Set theory, higher order logic or both?

DOI10.1007/BFB0105405MaRDI QIDQ6567712zbMATH OpenFDO

Authors Mike M. Gordon

Publication date 5 July 2024

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

Mathematics Subject Classification ID

Higher-order logic (03B16) Mechanization of proofs and logical operations (03B35) Set theory (03E99) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• On sets, types, fixed points, and checkerboards
• A mechanized translation from higher-order logic to set theory
• Set theory for verification. I: From foundations to functions
• STMM: A set theory for mechanized mathematics
• scientific article; zbMATH DE number 2080010

Cites work

• A formulation of the simple theory of types
• Exploring abstract algebra in constructive type theory
• scientific article; zbMATH DE number 2185680 (Why is no real title available?)
• scientific article; zbMATH DE number 46957 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• IMPS: An interactive mathematical proof system
• Isabelle. A generic theorem prover
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• The Alf proof editor and its proof engine

Cited in

(3)

• Hammering higher order set theory
• Mechanized HOL reasoning in set theory
• The Naproche-ZF theorem prover (short paper)

This page was built for publication: Set theory, higher order logic or both?

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