Optimization techniques for propositional intuitionistic logic and their implementation

DOI10.1016/j.tcs.2008.08.013zbMath1157.68060OpenAlexW1971769584MaRDI QIDQ959821

Alessandro Avellone, Guido Fiorino, Ugo Moscato

Publication date: 12 December 2008

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2008.08.013

zbMATH Keywords

tableauxintuitionistic logicautomated theorem proving

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items (4)

KALC: a constructive semantics for ALC ⋮ Intuitionistic Decision Procedures Since Gentzen ⋮ Fast decision procedure for propositional Dummett logic based on a multiple premise tableau calculus ⋮ A tableau calculus for Propositional Intuitionistic Logic with a refined treatment of nested implications

Uses Software

• Coq
• ILTP
• Nuprl
• PITP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• The ILTP problem library for intuitionistic logic
• A constructivism based on classical truth
• Intuitionistic propositional logic is polynomial-space complete
• Abstract parametric classes and abstract data types defined by classical and constructive logical methods
• An improved refutation system for intuitionistic predicate logic
• Contraction-free sequent calculi for intuitionistic logic
• An O(n log n)-Space Decision Procedure for Intuitionistic Propositional Logic
• The Taming of the Cut. Classical Refutations with Analytic Cut
• Avoiding duplications in tableau systems for intuitionistic logic and Kuroda logic
• Space-efficient Decision Procedures for Three Interpolable Propositional Intermediate Logics
• An Intuitionistic Predicate Logic Theorem Prover
• Computer Science Logic
• Improvements to the Tableau Prover PITP

This page was built for publication: Optimization techniques for propositional intuitionistic logic and their implementation