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

DOI10.1016/J.ENTCS.2017.04.006MaRDI QIDQ1744444zbMATH OpenOpenAlexWikidataFDO

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

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

Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Recommendations

• scientific article; zbMATH DE number 863013
• Automating and computing paraconsistent reasoning: contraction-free, resolution and type systems
• Contraction-free sequent calculi for intuitionistic logic
• Automatic decidability: a schematic calculus for theories with counting operators
• scientific article; zbMATH DE number 4072437
• Note on deduction theorems in contraction-free logics
• Axiomatizing proof tree concepts in bounded arithmetic
• Cut elimination in sequent calculi with implicit contraction, with a conjecture on the origin of Gentzen's altitude line construction
• Confluence of Cut-Elimination Procedures for the Intuitionistic Sequent Calculus
• A cut-free sequent calculus for the logic of constant domains with a limited amount of duplications

Cites work

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

Cited in

(1)

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

Describes a project that uses

Uses Software

• Lolli

This page was built for publication: From cut-free calculi to automated deduction: the case of bounded contraction

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