Metamathematics, Machines and Gödel's Proof

DOI10.1017/CBO9780511569883zbMath0813.68150OpenAlexW1968376266MaRDI QIDQ4296962

Natarajan Shankar

Publication date: 23 June 1994

Full work available at URL: https://doi.org/10.1017/cbo9780511569883

zbMATH Keywords

lambda calculusBoyer-Moore theorem proverLisp programming

Mathematics Subject Classification ID

Related Items (23)

A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle ⋮ The reflective Milawa theorem prover is sound (down to the machine code that runs it) ⋮ Computing and the cultures of proving ⋮ More Church-Rosser proofs (in Isabelle/HOL) ⋮ A verified SAT solver framework with learn, forget, restart, and incrementality ⋮ Formalization of the resolution calculus for first-order logic ⋮ Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Computer theorem proving in mathematics ⋮ The Mechanical Verification of a DPLL-Based Satisfiability Solver ⋮ Automated search for Gödel's proofs ⋮ Matching and alpha-equivalence check for nominal terms ⋮ Towards the animation of proofs -- testing proofs by examples ⋮ Formalizing Bachmair and Ganzinger's ordered resolution prover ⋮ Distilling the requirements of Gödel's incompleteness theorems with a proof assistant ⋮ A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality ⋮ Mechanised Computability Theory ⋮ A formally verified abstract account of Gödel's incompleteness theorems ⋮ A Formalisation of Weak Normalisation (with Respect to Permutations) of Sequent Calculus Proofs ⋮ A Completeness Proof for Bisimulation in the pi-calculus Using Isabelle ⋮ On the desirability of mechanizing calculational proofs ⋮ Reflection in conditional rewriting logic

This page was built for publication: Metamathematics, Machines and Gödel's Proof