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 (4)

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

This page was built for publication: Converting non-classical matrix proofs into sequent-style systems