Constructive decision via redundancy-free proof-search

DOI10.1007/S10817-020-09555-YzbMATH Open1468.03015OpenAlexW4205994606MaRDI QIDQ5919012FDOQ5919012

Authors: Dominique Larchey-Wendling 

Publication date: 2 November 2020

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-020-09555-y

Recommendations

• Constructive decision via redundancy-free proof-search
• The complexity of decision procedures in relevance logic II
• scientific article; zbMATH DE number 1189111
• Decision procedure of some relevant logics: a constructive perspective
• scientific article; zbMATH DE number 1342215

zbMATH Keywords

sequent calculirelevance logiccontraction rulealmost full relationsconstructive decidabilitymechanization in Coqredundancy-free search

Mathematics Subject Classification ID

Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Proof theory in general (including proof-theoretic semantics) (03F03) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Formalization of mathematics in connection with theorem provers (68V20)

Cites Work

• The decidability of the intensional fragment of classical linear logic
• A completeness theorem in modal logic
• The semantics of BI and resource tableaux
• The undecidability of entailment and relevant implication
• On the decidability of implicational ticket entailment
• Ticket Entailment is decidable
• Constructive topology and combinatorics
• Stop when you are almost-full. Adventures in constructive termination
• A uniform semantic proof for cut-elimination and completeness of various first and higher order logics.
• A direct proof of the equivalence between Brouwer's fan theorem and König's lemma with a uniqueness hypothesis
• Ramsey's Theorem and the Pigeonhole Principle in Intuitionistic Mathematics
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Decision procedure of some relevant logics: a constructive perspective
• Issues in machine-checking the decidability of implicational ticket entailment
• On the decision problem for MELL
• Implicational relevance logic is 2-\textsc{ExpTime}-complete
• The covering and boundedness problems for branching vector addition systems
• Polynomial-space completeness of reachability for succinct branching VASS in dimension one
• Title not available (Why is that?)
• Constructive decision via redundancy-free proof-search

Cited In (3)

• A formally verified cut-elimination procedure for linear nested sequents for tense logic
• Decision procedure of some relevant logics: a constructive perspective
• Constructive decision via redundancy-free proof-search

Uses Software

• Coq

This page was built for publication: Constructive decision via redundancy-free proof-search

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