TY  - BOOK
AU  - Paulson,Lawrence C.
TI  - Logic and computation: interactive proof with cambridge LCF 
T2  - Cambridge tracts in theoretical computer science
SN  - 9780521395601
U1  - 005.1 23
PY  - 1990///
CY  - Cambridge
PB  - Cambridge University Press
KW  - Cambridge LCF (Computer system)
KW  - Computable functions
KW  - Data processing
N1  - Includes bibliographical references and index; 1. Survey and history of LCF--
2. Formal proof in first order logic--
3. A logic of computable functions--
4. Structural induction--
5. Syntactic operations for PP--
6. Theory structure--
7. Axioms and inference rules--
8. Tactics and tacticals--
9. Rewriting and simplification--
10. Sample proofs--
Bibliography--
Index
N2  - The book is based in part on the author's own research as well as on graduate teaching. Thus it can be used to accompany courses on hardware verification and as a resource for research workers
ER  -