The Ackermann approach for modal logic, correspondence theory and second-order reduction

DOI10.1016/j.jal.2012.01.001zbMath1248.03039OpenAlexW2043056708MaRDI QIDQ420837

Renate A. Schmidt

Publication date: 23 May 2012

Published in: Journal of Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jal.2012.01.001

zbMATH Keywords

modal logiccorrespondence theoryAckermann lemmaaxiom and rule reductionssecond-order quantifier eliminationsubstitution method

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35) Quantifier elimination, model completeness, and related topics (03C10)

Related Items

Semantic forgetting in expressive description logics, Second-Order Quantifier Elimination on Relational Monadic Formulas – A Basic Method and Some Less Expected Applications, Predicate Elimination for Preprocessing in First-Order Theorem Proving

Uses Software

• SQEMA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Refutational theorem proving for hierarchic first-order theories
• Computing circumscription revisited: A reduction algorithm
• Elementary canonical formulae: extending Sahlqvist's theorem
• Improved Second-Order Quantifier Elimination in Modal Logic
• On the Correspondence Between Modal and Classical Logic: an Automated Approach
• The Monotonous Elimination of Predicate Variables
• Algorithmic correspondence and completeness in modal logic. I. The core algorithm SQEMA
• Relational and Kleene-Algebraic Methods in Computer Science