An Evaluation-Driven Decision Procedure for G3i
From MaRDI portal
Publication:2946756
DOI10.1145/2660770zbMath1354.03083OpenAlexW2113939721MaRDI QIDQ2946756
Camillo Fiorentini, Guido Fiorino, Mauro Ferrari
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
Mechanization of proofs and logical operations (03B35) Proof theory in general (including proof-theoretic semantics) (03F03) Subsystems of classical logic (including intuitionistic logic) (03B20)
Related Items (3)
Proof-Search in Natural Deduction Calculus for Classical Propositional Logic ⋮ Linear depth deduction with subformula property for intuitionistic epistemic logic ⋮ Goal-oriented proof-search in natural deduction for intuitionistic propositional logic
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A formal framework for specifying sequent calculus proof systems
- Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models
- A Terminating Evaluation-Driven Variant of G3i
- Simplification Rules for Intuitionistic Propositional Tableaux
- A tableau calculus for Propositional Intuitionistic Logic with a refined treatment of nested implications
- Contraction-free sequent calculi for intuitionistic logic
- An O(n log n)-Space Decision Procedure for Intuitionistic Propositional Logic
- Avoiding duplications in tableau systems for intuitionistic logic and Kuroda logic
- Foundational Proof Certificates in First-Order Logic
- fCube: An Efficient Prover for Intuitionistic Propositional Logic
- An Intuitionistic Predicate Logic Theorem Prover
- Intuitionistic logic freed of all metarules
- Logical Approaches to Computational Barriers
- Goal-directed proof theory
This page was built for publication: An Evaluation-Driven Decision Procedure for G3i
