An evaluation-driven decision procedure for G3i

DOI10.1145/2660770MaRDI QIDQ2946756zbMATH OpenOpenAlexFDO

Authors Mauro Ferrari, Camillo Fiorentini, Guido Fiorino

Publication date 17 September 2015

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2660770

zbMATH Keywords

intuitionistic propositional logicproof-search proceduressequent calculi

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Mechanization of proofs and logical operations (03B35) Proof theory in general (including proof-theoretic semantics) (03F03)

Recommendations

• A Terminating Evaluation-Driven Variant of G3i
• Goal-oriented proof-search in natural deduction for intuitionistic propositional logic
• A proof-search procedure for intuitionistic propositional logic
• A semantical analysis of focusing and contraction in intuitionistic logic
• Intuitionistic logic freed of all metarules

Cites work

• A formal framework for specifying sequent calculus proof systems
• A tableau calculus for Propositional Intuitionistic Logic with a refined treatment of nested implications
• A Terminating Evaluation-Driven Variant of G3i
• An O(n log n)-Space Decision Procedure for Intuitionistic Propositional Logic
• An Intuitionistic Predicate Logic Theorem Prover
• Avoiding duplications in tableau systems for intuitionistic logic and Kuroda logic
• Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models
• Contraction-free sequent calculi for intuitionistic logic
• fCube: an efficient prover for intuitionistic propositional logic
• Foundational proof certificates in first-order logic
• Goal-directed proof theory
• scientific article; zbMATH DE number 1003731 (Why is no real title available?)
• scientific article; zbMATH DE number 1189106 (Why is no real title available?)
• scientific article; zbMATH DE number 1497485 (Why is no real title available?)
• scientific article; zbMATH DE number 895271 (Why is no real title available?)
• Intuitionistic logic freed of all metarules
• Logical Approaches to Computational Barriers
• Simplification Rules for Intuitionistic Propositional Tableaux

Cited in

(5)

• Goal-oriented proof-search in natural deduction for intuitionistic propositional logic
• A Terminating Evaluation-Driven Variant of G3i
• Proof-Search in Natural Deduction Calculus for Classical Propositional Logic
• Linear depth deduction with subformula property for intuitionistic epistemic logic
• A terminating sequent calculus for intuitionistic strong Löb logic with the subformula property

Describes a project that uses

Uses Software

• fCube

This page was built for publication: An evaluation-driven decision procedure for G3i

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