Pollack-inconsistency

DOI10.1016/J.ENTCS.2012.06.008zbMATH Open1294.68130OpenAlexW2914101174WikidataQ113318097 ScholiaQ113318097MaRDI QIDQ5170237FDOQ5170237

Authors: 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

Recommendations

• HOL Zero's solutions for Pollack-inconsistency
• Proof by consistency
• Some considerations on the usability of interactive provers
• scientific article; zbMATH DE number 2185701
• scientific article; zbMATH DE number 2177623

zbMATH Keywords

consistencyinteractive theorem proverPollack consistency

Mathematics Subject Classification ID

Cites Work

• MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics
• Isabelle/HOL. A proof assistant for higher-order logic
• Mathematical knowledge management in MIZAR
• Towards Self-verification of HOL Light
• Mathematical Knowledge Management
• The HOL Light theory of Euclidean space
• TRX: a formally verified parser interpreter
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• The Four Colour Theorem: Engineering of a Formal Proof
• Spurious disambiguation errors and how to get rid of them
• Formalizing an analytic proof of the prime number theorem
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (4)

• Pollock and Sturgeon on defeaters
• 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

This page was built for publication: Pollack-inconsistency

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