Title :
Terms, proofs and refinement
Author_Institution :
Dept. of Comput. Sci., Edinburgh Univ., UK
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;
Conference_Titel :
Logic in Computer Science, 1994. LICS '94. Proceedings., Symposium on
Conference_Location :
Paris
Print_ISBN :
0-8186-6310-3
DOI :
10.1109/LICS.1994.316092
