From cut-free calculi to automated deduction: the case of bounded contraction
DOI10.1016/J.ENTCS.2017.04.006zbMATH Open1401.03034OpenAlexW2627866801WikidataQ57850656 ScholiaQ57850656MaRDI QIDQ1744444FDOQ1744444
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
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
- 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
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)
Cites Work
- Linear logic
- Residuated frames with applications to decidability
- Residuated lattices. An algebraic glimpse at substructural logics
- Logic programming in a fragment of intuitionistic linear logic
- The finite model property for various fragments of intuitionistic linear logic
- Logic Programming with Focusing Proofs in Linear Logic
- Extending intuitionistic linear logic with knotted structural rules
- From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic
- Disjunction property and complexity of substructural logics
- Contraction-free sequent calculi for intuitionistic logic
- Bounded contraction and Gentzen-style formulation of Łukasiewicz logics
- Efficient resource management for linear logic proof search
- From cut-free calculi to automated deduction: the case of bounded contraction
- Title not available (Why is that?)
Cited In (1)
Uses Software
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)
