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 (7)

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

This page was built for publication: Theorem Proving in Higher Order Logics