Skip to content
Open global navigation

Cambridge University Press

AcademicLocation selectorSearch toggleMain navigation toggle
Cart
Register Sign in Wishlist
Logic and Computation

Logic and Computation
Interactive Proof with Cambridge LCF

$69.00

Part of Cambridge Tracts in Theoretical Computer Science

  • Date Published: July 1990
  • availability: Available
  • format: Paperback
  • isbn: 9780521395601

$69.00
Paperback

Add to cart Add to wishlist

Other available formats:
Hardback, eBook


Looking for an examination copy?

If you are interested in the title for your course we can consider offering an examination copy. To register your interest please contact collegesales@cambridge.org providing details of the course you are teaching.

Description
Product filter button
Description
Contents
Resources
About the Authors
  • Logic and Computation is concerned with techniques for formal theorem-proving, with particular reference to Cambridge LCF (Logic for Computable Functions). Cambridge LCF is a computer program for reasoning about computation. It combines methods of mathematical logic with domain theory, the basis of the denotational approach to specifying the meaning of statements in a programming language. This book consists of two parts. Part I outlines the mathematical preliminaries: elementary logic and domain theory. They are explained at an intuitive level, giving references to more advanced reading. Part II provides enough detail to serve as a reference manual for Cambridge LCF. It will also be a useful guide for implementors of other programs based on the LCF approach.

    Reviews & endorsements

    "This book is well-written: it is a good text for any reader who wants to become familiar with Cambridge LCF, or, in general, with machine assisted (formal) proof construction." Mathematical Reviews

    Customer reviews

    Not yet reviewed

    Be the first to review

    Review was not posted due to profanity

    ×

    , create a review

    (If you're not , sign out)

    Please enter the right captcha value
    Please enter a star rating.
    Your review must be a minimum of 12 words.

    How do you rate this item?

    ×

    Product details

    • Date Published: July 1990
    • format: Paperback
    • isbn: 9780521395601
    • length: 320 pages
    • dimensions: 246 x 189 x 17 mm
    • weight: 0.58kg
    • availability: Available
  • 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.

  • Author

    Lawrence C. Paulson, University of Cambridge

Sign In

Please sign in to access your account

Cancel

Not already registered? Create an account now. ×

You are now leaving the Cambridge University Press website, your eBook purchase and download will be completed by our partner www.ebooks.com. Please see the permission section of the www.ebooks.com catalogue page for details of the print & copy limits on our eBooks.

Continue ×

Continue ×

Find content that relates to you

© Cambridge University Press 2014

Back to top

Are you sure you want to delete your account?

This cannot be undone.

Cancel Delete

Thank you for your feedback which will help us improve our service.

If you requested a response, we will make sure to get back to you shortly.

×
Please fill in the required fields in your feedback submission.
×