Converting non-classical matrix proofs into sequent-style systems

DOI10.1007/3-540-61511-3_104zbMath1415.03031OpenAlexW2103614325MaRDI QIDQ4647538

Stephan Schmitt, Christoph Kreitz

Publication date: 15 January 2019

Published in: Automated Deduction — Cade-13 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61511-3_104

zbMATH Keywords

modal logicsequent calculusintuitionistic logicreduction rulerule application

Mathematics Subject Classification ID

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

Related Items

Tableaux methods for access control in distributed systems, Representing scope in intuitionistic deductions, Connection-based proof construction in linear logic, Connection methods in linear logic and proof nets construction

Uses Software

• SETHEO
• KoMeT

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The foundations of mathematics. A study in the philosophy of science
• Proof methods for modal and intuitionistic logics
• SETHEO: A high-performance theorem prover
• On Matrices with Connections
• T-string unification: Unifying prefixes in non-classical proof methods
• KoMeT
• Integration of automated and interactive theorem proving in ILF
• A Machine-Oriented Logic Based on the Resolution Principle