Theorem Proving in Higher Order Logics

DOI10.1007/11541868zbMath1152.03315OpenAlexW2484880499MaRDI QIDQ5477659

Russell O'Connor

Publication date: 6 July 2006

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

Full work available at URL: https://doi.org/10.1007/11541868

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) First-order arithmetic and fragments (03F30)

Related Items

A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle, Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Extended version, Quantitative continuity and Computable Analysis in Coq, Formalizing Bachmair and Ganzinger's ordered resolution prover, Distilling the requirements of Gödel's incompleteness theorems with a proof assistant, Mechanised Computability Theory, A formally verified abstract account of Gödel's incompleteness theorems

Uses Software

• Coq
• Nuprl