HOL Zero’s Solutions for Pollack-Inconsistency

DOI10.1007/978-3-319-43144-4_2zbMath1478.68433OpenAlexW2480255341MaRDI QIDQ2829240

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)

Related Items (2)

Isabelle's metalogic: formalization and proof checker ⋮ A formalization and proof checker for Isabelle's metalogic

Uses Software

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

Cites Work

• Unnamed Item
• The reflective Milawa theorem prover is sound (down to the machine code that runs it)
• A theory of type polymorphism in programming
• Isabelle/HOL. A proof assistant for higher-order logic
• HOL Light: An Overview
• A Brief Overview of HOL4
• Pollack-inconsistency

This page was built for publication: HOL Zero’s Solutions for Pollack-Inconsistency