The Use of Machines to Assist in Rigorous Proof

R. Milner, R. S. Bird

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

A methodology for computer assisted proof is presented with an example. A central ingredient in the methods is the presentation of tactics (or strategies) in an algorithmic metalanguage. Further, the same language is also used to express combinators, by which simple elementary tactics -- which often correspond to the inference rules of the logic employed -- are combined into more complex tactics, which may even be strategies complete for a class of problems. However, the emphasis is not upon completeness but upon providing a metalogical framework within which a user may express his insight into proof methods and may delegate routine (but error-prone) work to the computer. This method of tactic composition is presented at the start of the paper in the form of an elementary theory of goal-seeking. A second ingredient of the methodology is the stratification of machine-assisted proof by an ancestry graph of applied theories, and the example illustrates this stratification. In the final section, some recent developments and applications of the method are cited.
Original languageEnglish
Pages (from-to)411-422
Number of pages12
JournalPhilosophical Transactions A: Mathematical, Physical and Engineering Sciences
Issue number1522
Publication statusPublished - Oct 1984


Dive into the research topics of 'The Use of Machines to Assist in Rigorous Proof'. Together they form a unique fingerprint.

Cite this