An improved refutation system for intuitionistic predicate logic

DOI10.1007/BF00881949zbMath0814.03005MaRDI QIDQ1344876

Pierangelo Miglioli, Ugo Moscato, Mario Ornaghi

Publication date: 22 February 1995

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

zbMATH Keywords

Kripke modelsintuitionistic logicnondeterminismduplicationsKuroda logicrefutation calculus

Mathematics Subject Classification ID

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

Related Items (8)

Tableaux for logic programming with strong negation ⋮ Generalized tableau systems for intermediate propositional logics ⋮ Almost duplication-free tableau calculi for prepositional lax logics ⋮ Combining many-valued and intuitionistic tableaux ⋮ Proof-search in intuitionistic logic based on constraint satisfaction ⋮ Optimization techniques for propositional intuitionistic logic and their implementation ⋮ Deciding intuitionistic propositional logic via translation into classical logic ⋮ Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models

Cites Work

• Semantical investigations in Heyting's intuitionistic logic
• Contraction-free sequent calculi for intuitionistic logic
• Unnamed Item
• Unnamed Item
• Unnamed Item

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