scientific article; zbMATH DE number 1507179

MaRDI QIDQ4503899zbMATH OpenFDO

Authors Gilles Dowek

Publication date 14 September 2000

zbMATH Keywords

first-order presentations of simple type theoryhigher-order logichigher-order resolutionhigher-order theorem provingset theory

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• First-order automated reasoning with theories: when deduction modulo theory meets practice
• Automated reasoning in higher-order logic. Set comprehension and extensionality in Church's type theory
• scientific article; zbMATH DE number 46359
• Completeness theorems for first-order logic analysed in constructive type theory
• Automating theories in intuitionistic logic
• Completeness theorems for first-order logic analysed in constructive type theory
• On the proof-theory of two formalisations of modal first-order logic
• An automated prover for Zermelo-Fraenkel set theory in Theorema
• Proof theory and automated deduction
• scientific article; zbMATH DE number 1088206

Cited in

(8)

• Modularity of proof-nets. Generating the type of a module.
• Automated proof construction in type theory using resolution
• First-order automated reasoning with theories: when deduction modulo theory meets practice
• scientific article; zbMATH DE number 1614692 (Why is no real title available?)
• Combining Type Theory and Untyped Set Theory
• On sets, types, fixed points, and checkerboards
• Automated Deduction – CADE-20
• Proof-term synthesis on dependent-type systems via explicit substitutions

Describes a project that uses

Uses Software

• ETPS

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 Q4503899)