DocumentCode
1996896
Title
Terms, proofs and refinement
Author
Burstall, Rod
Author_Institution
Dept. of Comput. Sci., Edinburgh Univ., UK
fYear
1994
fDate
4-7 Jul 1994
Firstpage
2
Lastpage
7
Abstract
We give a simple account of the connection between lambda terms and natural deduction proofs, showing how the terms can be rearranged into a form close to conventional proofs, and also to less conventional “top down” proofs. Creating proofs interactively by refinement can be seen as just keying in a lambda expression one symbol at a time in response to prompts from the machine. The aim is to convey some basic ideas to the uninitiated without technical or pragmatic detail
Keywords
formal logic; lambda calculus; theorem proving; lambda terms; natural deduction proofs; proofs; refinement; Calculus; Computer science; Logic; Mirrors; Time factors; Writing;
fLanguage
English
Publisher
ieee
Conference_Titel
Logic in Computer Science, 1994. LICS '94. Proceedings., Symposium on
Conference_Location
Paris
Print_ISBN
0-8186-6310-3
Type
conf
DOI
10.1109/LICS.1994.316092
Filename
316092
Link To Document