Tactics for mechanized reasoning: a commentary on Milner (1984) ‘The use of machines to assist in rigorous proof’
From MaRDI portal
Publication:2955752
DOI10.1098/rsta.2014.0234zbMath1353.68250OpenAlexW2077244951WikidataQ41871292 ScholiaQ41871292MaRDI QIDQ2955752
Publication date: 13 January 2017
Published in: Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1098/rsta.2014.0234
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (4)
ACKERMANN’S FUNCTION IN ITERATIVE FORM: A PROOF ASSISTANT EXPERIMENT ⋮ Computational logic: its origins and applications ⋮ Formalizing Ordinal Partition Relations Using Isabelle/HOL ⋮ From LCF to Isabelle/HOL
Cites Work
- The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4
- A theory of type polymorphism in programming
- A MACHINE-ASSISTED PROOF OF GÖDEL’S INCOMPLETENESS THEOREMS FOR THE THEORY OF HEREDITARILY FINITE SETS
- The use of machines to assist in rigorous proof
- Proving Theorems about LISP Functions
- A Machine-Oriented Logic Based on the Resolution Principle
- The next 700 programming languages
- An axiomatic basis for computer programming
This page was built for publication: Tactics for mechanized reasoning: a commentary on Milner (1984) ‘The use of machines to assist in rigorous proof’
