scientific article; zbMATH DE number 1301852

MaRDI QIDQ4247075zbMATH OpenFDO

Authors James Caldwell

Publication date 16 June 1999

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

• scientific article; zbMATH DE number 1189111
• scientific article; zbMATH DE number 1341469
• 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
• scientific article; zbMATH DE number 1341469 (Why is no real title available?)

Describes a project that uses

Uses Software

• Nuprl

This page was built for publication:

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