Intuitionistic Decision Procedures Since Gentzen

DOI10.1007/978-3-319-29198-7_6zbMath1439.03096OpenAlexW2402087943MaRDI QIDQ3305556

Roy Dyckhoff

Publication date: 7 August 2020

Published in: Advances in Proof Theory (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/10023/8824

zbMATH Keywords

sequent calculusproof theoryintuitionistic logicproof assistantinitial sequent

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items (2)

Abductive Reasoning in Intuitionistic Propositional Logic via Theorem Synthesis ⋮ Maehara-style modal nested calculi

Uses Software

• Coq
• ILTP
• STRIP
• LoTREC
• ileanCoP
• Imogen
• TABLEAUX
• IntHistGC

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Saved from the cellar. Gerhard Gentzen's shorthand notes on logic and foundations of mathematics
• Proof analysis in intermediate logics
• Complexity of subclasses of the intuitionistic propositional calculus
• The foundations of mathematics. A study in the philosophy of science
• The ILTP problem library for intuitionistic logic
• Cut-free sequent systems for temporal logic
• Optimization techniques for propositional intuitionistic logic and their implementation
• Proof methods for modal and intuitionistic logics
• The modal logic of provability. The sequential approach
• TABLEAUX: A general theorem prover for modal logics
• Bounds for cut elimination in intuitionistic propositional logic
• Linearizing intuitionistic implication
• Intuitionistic propositional logic is polynomial-space complete
• Proofs and countermodels in non-classical logics
• Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models
• Decision methods for linearly ordered Heyting algebras
• Admissibility of structural rules for contraction-free systems of intuitionistic logic
• GEOMETRISATION OF FIRST-ORDER LOGIC
• Simplification Rules for Intuitionistic Propositional Tableaux
• Countermodels from Sequent Calculi in Multi-Modal Logics
• A History-Based Theorem Prover for Intuitionistic Propositional Logic Using Global Caching: IntHistGC System Description
• SEMANTIC POLLUTION AND SYNTACTIC PURITY
• A Labelled System for IPL with Variable Splitting
• Strong Cut-Elimination Systems for Hudelmaier’s Depth-Bounded Sequent Calculus for Implicational Logic
• A Note on Gentzen's Decision Procedure for Intuitionistic Propositional Logic
• Contraction-free sequent calculi for intuitionistic logic
• An O(n log n)-Space Decision Procedure for Intuitionistic Propositional Logic
• Two loop detection mechanisms: A comparison
• Efficient loop-check for backward proof search in some non-classical propositional logics
• A resolution theorem prover for intuitionistic logic
• Space-efficient Decision Procedures for Three Interpolable Propositional Intermediate Logics
• Automated Reasoning with Analytic Tableaux and Related Methods
• An Intuitionistic Predicate Logic Theorem Prover
• Automating Coherent Logic
• Intuitionistic logic freed of all metarules
• Automated Reasoning with Analytic Tableaux and Related Methods
• Automated Reasoning with Analytic Tableaux and Related Methods
• Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic
• A new algorithm for derivability in the constructive propositional calculus
• Mechanizing Mathematical Reasoning
• Eine Darstellung der Intuitionistischen Logik in der Klassischen
• Automated Synthesis of Tableau Calculi
• Logical Approaches to Computational Barriers

This page was built for publication: Intuitionistic Decision Procedures Since Gentzen