Theorem provers for substructural logics

DOI10.2298/PIM0796055IMaRDI QIDQ3510441zbMATH OpenOpenAlexFDO

Authors Mirjana Isaković-Ilić

Publication date 2 July 2008

Published in Publications de l'Institut Math?matique (Belgrade) (Search for Journal in Brave)

Full work available at URL https://eudml.org/doc/117041

IPFS File on IPFS (Hint: this is only the Hash - if you get a timeout, this file is not available on our server.)

zbMATH Keywords

BCK logicclassical logiccut eliminationintuitionistic logicrelevant logicsequent systemtableau system

Mathematics Subject Classification ID

Classical propositional logic (03B05) Subsystems of classical logic (including intuitionistic logic) (03B20) Mechanization of proofs and logical operations (03B35) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Cut-elimination and normal-form theorems (03F05)

Recommendations

• scientific article; zbMATH DE number 2099386
• Towards structurally-free theorem proving
• Algorithmic structural completeness and a retrieval system for proving theorems in algorithmic theories
• Proof finding algorithms for implicational logics
• Relational proof system for linear and other substructural logics

Cited in

(12)

• Algorithmic structural completeness and a retrieval system for proving theorems in algorithmic theories
• Skolemization for Substructural Logics
• Some Remarks on Theorem Proving Systems and Mazurkiewicz Algorithms Associated with them
• scientific article; zbMATH DE number 1222430 (Why is no real title available?)
• Towards structurally-free theorem proving
• scientific article; zbMATH DE number 1989651 (Why is no real title available?)
• scientific article; zbMATH DE number 1770113 (Why is no real title available?)
• scientific article; zbMATH DE number 2099386 (Why is no real title available?)
• A Sahlqvist theorem for substructural logic
• Theorems of Alternatives for Substructural Logics
• Substructural logic and partial correctness
• Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic

This page was built for publication: Theorem provers for substructural logics

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