DETERMINISTIC SQEMA AND APPLICATION FOR PRE-CONTACT LOGIC - T. Georgiev, Dimiter (Ann. Sofia Univ. Fac. Math. and Inf., 2016)
SQEMA is a set of rules for finding first-order correspondents of modal formulas, and can be used for proving axiomatic completeness. SQEMA succeeds for the Sahlqvist and Inductive formulas. A deterministic, terminating, but sometimes failing algorithm based on SQEMA for a modal language with nominals, reversed modalities and the universal modality - ML(T,U) - is presented. Deterministic SQEMA finds first-order correspondents, and it can be used to prove di-persistence. It succeeds for the Sahlqvist and Inductive formulas. The axiomatic system for ML(T,U) is shown and its strong completeness is proven. It is shown that adding di-persistent formulas as axioms preserves strong completeness. Deterministic SQEMA is extended for the language of pre-contact logics using a modified translation into ML(T,U). Deterministic SQEMA succeeds for the Sahlqvist class of pre-contact formulas.