Pollack-inconsistency

DOI10.1016/J.ENTCS.2012.06.008MaRDI QIDQ5170237zbMATH OpenOpenAlexWikidataFDO

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

zbMATH Keywords

consistencyinteractive theorem proverPollack consistency

Mathematics Subject Classification ID

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

Cites work

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

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

Describes a project that uses

Uses Software

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

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)