Decision procedures for intuitionistic propositional logic by program extraction

DOI10.1007/3-540-69778-0_29MaRDI QIDQ3838821zbMATH OpenFDO

Authors Klaus Weich

Publication date 5 January 1999

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

Full work available at URL https://doi.org/10.1007/3-540-69778-0_29

zbMATH Keywords

construction of derivationsconstructive proofscounter-modeldecidabilitydecision proceduresintuitionistic logicintuitionistic propositional logicprogram correctnessverification

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) Cut-elimination and normal-form theorems (03F05) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Intuitionistic tableau extracted
• scientific article; zbMATH DE number 1753197
• An O(n log n)-Space Decision Procedure for Intuitionistic Propositional Logic
• Intuitionistic Decision Procedures Since Gentzen
• On sequent calculi for intuitionistic propositional logic.

Cited in

(13)

• A unified procedure for provability and counter-model generation in minimal implicational logic
• Controlling Program Extraction in Light Logics
• Intuitionistic Decision Procedures Since Gentzen
• On sequent calculi for intuitionistic propositional logic.
• Bidirectional Decision Procedures for the Intuitionistic Propositional Modal Logic IS4
• Extraction of a program from deduction and its regularity. I
• Classical propositional decidability via Nuprl proof extraction
• Intuitionistic tableau extracted
• scientific article; zbMATH DE number 1753197 (Why is no real title available?)
• The decidability of dependency in intuitionistic propositional logic
• Deciding intuitionistic propositional logic via translation into classical logic
• Constructive decision via redundancy-free proof-search
• Optimization techniques for propositional intuitionistic logic and their implementation

This page was built for publication: Decision procedures for intuitionistic propositional logic by program extraction

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