Converting non-classical matrix proofs into sequent-style systems

DOI10.1007/3-540-61511-3_104zbMath1415.03031MaRDI 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 logic; sequent calculus; intuitionistic logic; reduction rule; rule application

Mathematics Subject Classification ID

03B45: Modal logic (including the logic of norms)

03B10: Classical first-order logic

03B35: Mechanization of proofs and logical operations

03B20: Subsystems of classical logic (including intuitionistic logic)

Related Items

Tableaux methods for access control in distributed systems, Connection-based proof construction in linear logic, Representing scope in intuitionistic deductions, 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