Converting non-classical matrix proofs into sequent-style systems

DOI10.1007/3-540-61511-3_104MaRDI QIDQ4647538zbMATH OpenOpenAlexFDO

Authors 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

intuitionistic logicmodal logicreduction rulerule applicationsequent calculus

Mathematics Subject Classification ID

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

Recommendations

• A uniform procedure for converting matrix proofs into sequent-style systems
• scientific article; zbMATH DE number 1748580
• scientific article; zbMATH DE number 1612558
• A proof-theoretic analysis of the classical propositional matrix method
• Automated Reasoning with Analytic Tableaux and Related Methods
• scientific article; zbMATH DE number 49746
• Studying sequent systems via non-deterministic multiple-valued matrices
• A formal framework for specifying sequent calculus proof systems
• scientific article; zbMATH DE number 1748578

Cites work

• \textsf{Ko\(_{\mathsf{M}}\)eT}
• A Machine-Oriented Logic Based on the Resolution Principle
• scientific article; zbMATH DE number 4164180 (Why is no real title available?)
• scientific article; zbMATH DE number 4055570 (Why is no real title available?)
• scientific article; zbMATH DE number 49746 (Why is no real title available?)
• scientific article; zbMATH DE number 194631 (Why is no real title available?)
• scientific article; zbMATH DE number 3300581 (Why is no real title available?)
• Integration of automated and interactive theorem proving in ILF
• On Matrices with Connections
• Proof methods for modal and intuitionistic logics
• SETHEO: A high-performance theorem prover
• T-string unification: unifying prefixes in non-classical proof methods
• The foundations of mathematics. A study in the philosophy of science

Cited in

(8)

• Representing scope in intuitionistic deductions
• Connection methods in linear logic and proof nets construction
• A uniform procedure for converting matrix proofs into sequent-style systems
• Proof reconstruction in classical and nonclassical logics (Diss., TU Darmstadt, 1999)
• Tableaux methods for access control in distributed systems
• Connection-based proof construction in linear logic
• A proof-theoretic analysis of the classical propositional matrix method
• Automated Reasoning with Analytic Tableaux and Related Methods

Describes a project that uses

Uses Software

• SETHEO
• KoMeT

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4647538)