Pollack-inconsistency

DOI10.1016/j.entcs.2012.06.008zbMath1294.68130OpenAlexW2914101174WikidataQ113318097 ScholiaQ113318097MaRDI QIDQ5170237

Freek Wiedijk

Publication date: 22 July 2014

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2012.06.008

zbMATH Keywords

consistencyinteractive theorem proverPollack consistency

Mathematics Subject Classification ID

Related Items

The formal verification of the ctm approach to forcing, HOL Zero’s Solutions for Pollack-Inconsistency, Proof Auditing Formalised Mathematics

Uses Software

• ACL2
• Coq
• Isabelle/HOL
• MizarMode
• TRX
• Ivy
• Metamath
• seL4

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Spurious disambiguation errors and how to get rid of them
• MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics
• Isabelle/HOL. A proof assistant for higher-order logic
• The HOL Light theory of Euclidean space
• Formalizing an analytic proof of the prime number theorem
• TRX: A Formally Verified Parser Interpreter
• The Four Colour Theorem: Engineering of a Formal Proof
• Towards Self-verification of HOL Light
• Formal certification of a compiler back-end or
• Mathematical Knowledge Management