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

DOI10.1098/RSTA.2014.0234zbMATH Open1353.68250OpenAlexW2077244951WikidataQ41871292 ScholiaQ41871292MaRDI QIDQ2955752FDOQ2955752

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)

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 theory of type polymorphism in programming
• An axiomatic basis for computer programming
• 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
• 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)

• ACKERMANN’S FUNCTION IN ITERATIVE FORM: A PROOF ASSISTANT EXPERIMENT
• From LCF to Isabelle/HOL
• Formalizing Ordinal Partition Relations Using 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)