Automated reasoning in higher-order logic. Set comprehension and extensionality in Church's type theory

zbMATH Open1206.03014MaRDI QIDQ3586992FDOQ3586992

Authors: Chad E. Brown 

Publication date: 1 September 2010

Recommendations

• Automated Deduction – CADE-20
• On sets, types, fixed points, and checkerboards
• Classical type theory
• scientific article; zbMATH DE number 47007
• The Clausal Theory of Types

zbMATH Keywords

type theoryautomated reasoninghigher-order logic

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Mechanization of proofs and logical operations (03B35)

Cited In (12)

• Title not available (Why is that?)
• Progress in the Development of Automated Theorem Proving for Higher-Order Logic
• Combining and automating classical and non-classical logics in classical higher-order logics
• Formalization of reliability block diagrams in higher-order logic
• Analytic tableaux for higher-order logic with choice
• Classical type theory
• Formal reliability and failure analysis of Ethernet based communication networks in a smart grid substation
• On sets, types, fixed points, and checkerboards
• Towards the formal reliability analysis of oil and gas pipelines
• Extended First-Order Logic
• Automated Deduction – CADE-20
• Proof search with set variable instantiation in the calculus of constructions

Uses Software

• Isabelle/ZF

This page was built for publication: Automated reasoning in higher-order logic. Set comprehension and extensionality in Church's type theory

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