Simplification Rules for Intuitionistic Propositional Tableaux

DOI10.1145/2159531.2159536zbMath1352.03015OpenAlexW2019841519MaRDI QIDQ2946662

Guido Fiorino, Mauro Ferrari, Camillo Fiorentini

Publication date: 17 September 2015

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

Full work available at URL: http://hdl.handle.net/2434/204038

zbMATH Keywords

intuitionistic logictableau calculidecision proceduressimplification rules

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items (5)

An Evaluation-Driven Decision Procedure for G3i ⋮ Goal-oriented proof-search in natural deduction for intuitionistic propositional logic ⋮ A non-clausal tableau calculus for \textsc{MinSat} ⋮ Intuitionistic Decision Procedures Since Gentzen ⋮ Efficient SAT-based proof search in intuitionistic propositional logic

This page was built for publication: Simplification Rules for Intuitionistic Propositional Tableaux