Classical propositional decidability via Nuprl proof extraction

DOI10.1007/BFB0055132MaRDI QIDQ4247075zbMATH OpenFDO

Authors James Caldwell

Publication date 16 June 1999

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

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

zbMATH Keywords

classical propositional logicconstructive type theorydecidabilityNuprl systemproof development systemsequent calculus

Mathematics Subject Classification ID

Classical propositional logic (03B05) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70)

Recommendations

• Decision procedures for intuitionistic propositional logic by program extraction
• Intuitionistic tableau extracted
• Getting results from programs extracted from classical proofs
• scientific article; zbMATH DE number 895269

Cited in

(6)

• Search algorithms in type theory
• Formally verified tableau-based reasoners for a description logic
• Constructive membership predicates as index types
• Constructive Formalization of Hybrid Logic with Eventualities
• MUS Extraction Using Clausal Proofs
• Intuitionistic tableau extracted

Describes a project that uses

Uses Software

• Nuprl

This page was built for publication: Classical propositional decidability via Nuprl proof extraction

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