HOME > Detail View

Detail View

Logic and computation : interactive proof with Cambridge LCF 1st pbk. ed

Logic and computation : interactive proof with Cambridge LCF 1st pbk. ed (Loan 1 times)

Material type
단행본
Personal Author
Paulson, Lawrence C.
Title Statement
Logic and computation : interactive proof with Cambridge LCF / Lawrence C. Paulson.
판사항
1st pbk. ed.
Publication, Distribution, etc
Cambridge :   Cambridge University Press ,   1990, c1987.  
Physical Medium
xiii, 302 p. ; 25 cm.
Series Statement
Cambridge tracts in theoretical computer science ; 2
ISBN
0521395607 (pbk.) 9780521395601 (pbk.)
Bibliography, Etc. Note
Includes bibliographical references (p. [289]-295) and index.
Subject Added Entry-Topical Term
Cambridge LCF (Computer system) Computable functions -- Data processing.
000 00946namuu2200265 a 4500
001 000045453811
005 20080716094746
008 080711r19901987enk b 001 0 eng d
020 ▼a 0521395607 (pbk.)
020 ▼a 9780521395601 (pbk.)
040 ▼a 211009 ▼c 211009 ▼d 211009
050 4 ▼a QA9.59 ▼b .P38 1990
082 0 4 ▼a 005.1 ▼2 22
090 ▼a 005.1 ▼b P332L
100 1 ▼a Paulson, Lawrence C.
245 1 0 ▼a Logic and computation : ▼b interactive proof with Cambridge LCF / ▼c Lawrence C. Paulson.
250 ▼a 1st pbk. ed.
260 ▼a Cambridge : ▼b Cambridge University Press , ▼c 1990, c1987.
300 ▼a xiii, 302 p. ; ▼c 25 cm.
440 0 ▼a Cambridge tracts in theoretical computer science ; ▼v 2
504 ▼a Includes bibliographical references (p. [289]-295) and index.
650 0 ▼a Cambridge LCF (Computer system)
650 0 ▼a Computable functions ▼x Data processing.
945 ▼a KINS

Holdings Information

No. Location Call Number Accession No. Availability Due Date Make a Reservation Service
No. 1 Location Science & Engineering Library/Sci-Info(Stacks2)/ Call Number 005.1 P332L Accession No. 121173263 Availability Available Due Date Make a Reservation Service B M

Contents information

Table of Contents

Part I. Preliminaries: 1. Survey and history of LCF; 2. Formal proof in first order logic; 3. A logic of computable functions; 4. Structural induction; Part II. Cambridge LCF: 5. Syntactic operators for PPL; 6. Theory structure; 7. Axioms and interference rules; 8. Tactics and tacticals; 9. Rewriting and simplification; 10. Sample proofs; Bibliography; Index.


Information Provided By: : Aladin

New Arrivals Books in Related Fields

Anson, Steve (2022)
한국. 행정안전부 (2022)
한국. 행정안전부 (2022)
황기태 (2021)