An improved refutation system for intuitionistic predicate logic

DOI10.1007/BF00881949MaRDI QIDQ1344876zbMATH OpenFDO

Authors Pierangelo Miglioli, Ugo Moscato, Mario Ornaghi

Publication date 22 February 1995

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BF00881949

zbMATH Keywords

duplicationsintuitionistic logicKripke modelsKuroda logicnondeterminismrefutation calculus

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20)

Recommendations

• Avoiding duplications in tableau systems for intuitionistic logic and Kuroda logic
• An Intuitionistic Predicate Logic Theorem Prover
• scientific article; zbMATH DE number 1941685
• Refutation calculi for certain intermediate propositional logics
• scientific article; zbMATH DE number 1922478

Cites work

• Contraction-free sequent calculi for intuitionistic logic
• scientific article; zbMATH DE number 3739532 (Why is no real title available?)
• scientific article; zbMATH DE number 3222098 (Why is no real title available?)
• scientific article; zbMATH DE number 3300581 (Why is no real title available?)
• Semantical investigations in Heyting's intuitionistic logic

Cited in

(13)

• Intuitionistic logic according to Dijkstra's calculus of equational deduction
• Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models
• Avoiding duplications in tableau systems for intuitionistic logic and Kuroda logic
• scientific article; zbMATH DE number 1941685 (Why is no real title available?)
• scientific article; zbMATH DE number 1922478 (Why is no real title available?)
• Tableaux for logic programming with strong negation
• Generalized tableau systems for intermediate propositional logics
• Almost duplication-free tableau calculi for propositional lax logics
• Combining many-valued and intuitionistic tableaux
• Proof-search in intuitionistic logic based on constraint satisfaction
• scientific article; zbMATH DE number 1390272 (Why is no real title available?)
• Deciding intuitionistic propositional logic via translation into classical logic
• Optimization techniques for propositional intuitionistic logic and their implementation

This page was built for publication: An improved refutation system for intuitionistic predicate logic

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