Tactics for mechanized reasoning: a commentary on Milner (1984) ‘The use of machines to assist in rigorous proof’

DOI10.1098/RSTA.2014.0234MaRDI QIDQ2955752zbMATH OpenOpenAlexWikidataFDO

Authors Michael J. C. Gordon

Publication date 13 January 2017

Published in Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1098/rsta.2014.0234

Mathematics Subject Classification ID

History of mathematics in the 20th century (01A60) History of computer science (68-03)

Cites work

• A Machine-Oriented Logic Based on the Resolution Principle
• A machine-assisted proof of Gödel's incompleteness theorems for the theory of hereditarily finite sets
• A theory of type polymorphism in programming
• An axiomatic basis for computer programming
• Proving Theorems about LISP Functions
• The next 700 programming languages
• The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4
• The use of machines to assist in rigorous proof

Cited in

(4)

• Formalizing ordinal partition relations using Isabelle/HOL
• ACKERMANN’S FUNCTION IN ITERATIVE FORM: A PROOF ASSISTANT EXPERIMENT
• From LCF to Isabelle/HOL
• Computational logic: its origins and applications

This page was built for publication: Tactics for mechanized reasoning: a commentary on Milner (1984) ‘The use of machines to assist in rigorous proof’

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2955752)