A uniform procedure for converting matrix proofs into sequent-style systems

DOI10.1006/INCO.2000.2913zbMath1003.68147OpenAlexW2151355005MaRDI QIDQ1854382

Christoph Kreitz, Stephan Schmitt

Publication date: 14 January 2003

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/2c0c8d49cbc3c4af105a294b30743d67aca800eb

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35)

Related Items (3)

Innovations in computational type theory using Nuprl ⋮ Hintikka multiplicities in matrix decision methods for some propositional modal logics ⋮ Connection-based proof construction in linear logic

Uses Software

• Mathematica
• SETHEO
• Nuprl
• KoMeT

Cites Work

• More on the problem of finding a mapping between clause representation and natural-deduction representation
• Proof methods for modal and intuitionistic logics
• SETHEO: A high-performance theorem prover
• Untersuchungen über das logische Schliessen. I
• Mathematical thought. An introduction to the philosophy of mathematics
• On Matrices with Connections
• A resolution theorem prover for intuitionistic logic
• KoMeT
• Connection-based proof construction in linear logic
• A Machine-Oriented Logic Based on the Resolution Principle
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A uniform procedure for converting matrix proofs into sequent-style systems