linTAP: A tableau prover for linear logic

DOI10.1007/3-540-48754-9_20MaRDI QIDQ4263017zbMATH OpenFDO

Authors Heiko Mantel, Jens Otten

Publication date 13 March 2000

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-48754-9_20

zbMATH Keywords

linear logicprefix unificationtableau prover

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47)

Recommendations

• \(\mathsf{ileanTAP}\): an intuitionistic theorem prover
• lean TAP revisited
• Connection-based proof construction in linear logic
• Decision problems for propositional linear logic

Cited in

(4)

• IeanCOP: lean connection-based theorem proving
• lean\(T^ AP\): Lean tableau-based deduction
• A tableau method for the Lambek calculus based on a matrix characterization
• A logical characterization of forward and backward chaining in the inverse method

Describes a project that uses

Uses Software

• leanTAP
• linTAP
• ModLeanTAP

This page was built for publication: linTAP: A tableau prover for linear logic

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