From cut-free calculi to automated deduction: the case of bounded contraction

DOI10.1016/j.entcs.2017.04.006zbMath1401.03034OpenAlexW2627866801WikidataQ57850656 ScholiaQ57850656MaRDI QIDQ1744444

Carlos Olarte, Björn Lellmann, Elaine Pimentel, Agata Ciabattoni

Publication date: 23 April 2018

Full work available at URL: https://doi.org/10.1016/j.entcs.2017.04.006

zbMATH Keywords

proof theorysubstructural logicsproof searchbounded contraction

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) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Complexity of proofs (03F20)

Related Items

From cut-free calculi to automated deduction: the case of bounded contraction

Uses Software

• Lolli

Cites Work

• Unnamed Item
• Disjunction property and complexity of substructural logics
• Linear logic
• Residuated lattices. An algebraic glimpse at substructural logics
• Logic programming in a fragment of intuitionistic linear logic
• Extending intuitionistic linear logic with knotted structural rules
• Efficient resource management for linear logic proof search
• From cut-free calculi to automated deduction: the case of bounded contraction
• Bounded contraction and Gentzen-style formulation of Łukasiewicz logics
• From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic
• Logic Programming with Focusing Proofs in Linear Logic
• Contraction-free sequent calculi for intuitionistic logic
• The finite model property for various fragments of intuitionistic linear logic
• Residuated frames with applications to decidability