Detecting Loops During Proof Search in Propositional Affine Logic

DOI10.1093/LOGCOM/EXI072MaRDI QIDQ5488611zbMATH OpenOpenAlexFDO

Authors Tatjana Lutovac, James Harland

Publication date 22 September 2006

Published in Journal Of Logic And Computation (Search for Journal in Brave)

Full work available at URL https://semanticscholar.org/paper/3cf9ffe0fa5d24e94b8e1a4870842d1d9dada5c9

zbMATH Keywords

sequent calculusproof searchloop detectionaffine logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Recommendations

• Efficient loop-check for backward proof search in some non-classical propositional logics
• Decidability of linear affine logic
• Two loop detection mechanisms: a comparison
• scientific article; zbMATH DE number 517070
• Termination of derivations for minimal tense logic

Cited in

(5)

• Loop Elimination, a Sound Optimisation Technique for PTTP Related Theorem Proving
• scientific article; zbMATH DE number 1098500 (Why is no real title available?)
• Detection and analysis of some redundancies in linear logic sequent proofs
• Two loop detection mechanisms: a comparison
• Efficient loop-check for backward proof search in some non-classical propositional logics

This page was built for publication: Detecting Loops During Proof Search in Propositional Affine Logic

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