TY - JOUR
T1 - Can theorem proving keep the planes flying
AU - Bundy, Alan
PY - 1993/7
Y1 - 1993/7
N2 - Alan Bundy is Professor of Automated Reasoning in the Department of Artificial Intelligence at the University of Edinburgh. His Mathematical Reasoning Group is applying mathematics to the development of computer programs. The synthesis, verification and transformation of computer software is done by proving mathematical theorems using an automated theorem prover. A major technical problem to be overcome is how to guide the search for a proof so the theorem prover does not become bogged down in the possibilities. To solve this problem, the Edinburgh group have developed proof planning. their automated theorem prover first constructs an outline of the desired proof and then fills in the details of this outline.
AB - Alan Bundy is Professor of Automated Reasoning in the Department of Artificial Intelligence at the University of Edinburgh. His Mathematical Reasoning Group is applying mathematics to the development of computer programs. The synthesis, verification and transformation of computer software is done by proving mathematical theorems using an automated theorem prover. A major technical problem to be overcome is how to guide the search for a proof so the theorem prover does not become bogged down in the possibilities. To solve this problem, the Edinburgh group have developed proof planning. their automated theorem prover first constructs an outline of the desired proof and then fills in the details of this outline.
M3 - Article
VL - 5
JO - SERC Bulletin
JF - SERC Bulletin
IS - 1
ER -