Towards mechanical metamathematics
From MaRDI portal
Publication:1821563
DOI10.1007/BF00244278zbMath0616.68075MaRDI QIDQ1821563
Publication date: 1985
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
mathematical logicautomatic theorem provingBoyer-Moore theorem proverMetamathematicsproof-checking programtautology theorem
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (7)
Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL ⋮ Mechanising Gödel-Löb provability logic in HOL light ⋮ An automatic proof of Gödel's incompleteness theorem ⋮ A mechanical verification of the stressing algorithm for negative cost cycle detection in networks ⋮ The Mechanical Verification of a DPLL-Based Satisfiability Solver ⋮ Formalizing Bachmair and Ganzinger's ordered resolution prover ⋮ Formally verified tableau-based reasoners for a description logic
This page was built for publication: Towards mechanical metamathematics
