HOL Zero's solutions for Pollack-inconsistency

DOI10.1007/978-3-319-43144-4_2MaRDI QIDQ2829240zbMATH OpenOpenAlexFDO

Authors Mark Adams

Publication date 27 October 2016

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-43144-4_2

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Pollack-inconsistency
• HOL Light: An Overview
• A consistent foundation for Isabelle/HOL
• A consistent foundation for Isabelle/HOL
• Comprehending Isabelle/HOL’s Consistency

Cites work

• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• A Brief Overview of HOL4
• A theory of type polymorphism in programming
• HOL Light: An Overview
• Isabelle/HOL. A proof assistant for higher-order logic
• Pollack-inconsistency
• The reflective Milawa theorem prover is sound (down to the machine code that runs it)

Cited in

(3)

• Isabelle's metalogic: formalization and proof checker
• Pollack-inconsistency
• A formalization and proof checker for Isabelle's metalogic

Describes a project that uses

Uses Software

• ML
• Isabelle/HOL
• HOL
• ProofPower
• HOL Light
• LCF
• Milawa
• Jitawa
• seL4
• HOL Zero
• kepler98

This page was built for publication: HOL Zero's solutions for Pollack-inconsistency

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