Intuitionistic tableau extracted

DOI10.1007/3-540-48754-9_11MaRDI QIDQ4263008zbMATH OpenFDO

Authors James Caldwell

Publication date 13 March 2000

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-48754-9_11

zbMATH Keywords

correct-by-construction programdecidabilityformalization of a sequent presentation of intuitionistic propositional logicKripke counter-modelNuprl systemtableau

Mathematics Subject Classification ID

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

Recommendations

• Decision procedures for intuitionistic propositional logic by program extraction
• Classical propositional decidability via Nuprl proof extraction
• An O(n log n)-Space Decision Procedure for Intuitionistic Propositional Logic
• scientific article; zbMATH DE number 1753197

Cited in

(3)

• Decision procedures for intuitionistic propositional logic by program extraction
• Classical propositional decidability via Nuprl proof extraction
• Deciding intuitionistic propositional logic via translation into classical logic

Describes a project that uses

Uses Software

• Nuprl

This page was built for publication: Intuitionistic tableau extracted

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