On the Correspondence Between Modal and Classical Logic: an Automated Approach

DOI10.1093/logcom/3.6.605zbMath0802.03009OpenAlexW1989151171MaRDI QIDQ4286209

Andrzej Szałas

Publication date: 15 December 1994

Published in: Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/11858/00-001M-0000-0014-B1BE-5

zbMATH Keywords

modal logicfirst-order logicautomated translationelimination of second-order quantification

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35)

Related Items

Towards automating duality ⋮ Converse-PDL with regular inclusion axioms: a framework for MAS logics ⋮ Algebraic modal correspondence: Sahlqvist and beyond ⋮ On an automated translation of modal proof rules into formulas of the classical logic ⋮ Unnamed Item ⋮ The Ackermann approach for modal logic, correspondence theory and second-order reduction ⋮ Discrete dualities for \(n\)-potent MTL-algebras and 2-potent BL-algebras ⋮ General domain circumscription and its first-order reduction ⋮ Second-order quantifier elimination in higher-order contexts with applications to the semantical analysis of conditionals ⋮ First-Order Resolution Methods for Modal Logics ⋮ Annotation theories over finite graphs ⋮ Towards incorporating background theories into quantifier elimination ⋮ Completeness and Correspondence in Hybrid Logic via an Extension of SQEMA ⋮ On the strength and scope of DLS ⋮ Second-order reasoning in description logics ⋮ Approximate databases: a support tool for approximate reasoning ⋮ 2005 Summer Meeting of the Association for Symbolic Logic. Logic Colloquium '05