HOL Zero's solutions for Pollack-inconsistency

DOI10.1007/978-3-319-43144-4_2zbMATH Open1478.68433OpenAlexW2480255341MaRDI QIDQ2829240FDOQ2829240

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

Recommendations

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

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (3)

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

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)