CMU Artificial Intelligence Repository
Home INFO Search FAQs Repository Root

LCF: Automated generic theorem prover

Cambridge LCF (Logic for Computable Functions) is an interactive theorem prover. Proofs are conducted in PPLAMBDA, a natural deduction logic based on the domain theory of Dana Scott. PPLAMBDA is particularly suitable for proofs involving denotational semantics, lazy evaluation, or higher-order functions. LCF provides a metalanguage (Standard ML), a functional programming language whose values include PPLAMBDA terms, formulas, and theorems. Theorem-proving primitives such as inference rules, subgoaling strategies (tactics), and simplifiers are implemented as ML functions. The user can extend LCF by programming in ML. [LCF is an obsolete system.]
See Also: 

Origin: [] (Univ. of Cambridge) []
   (University of Munich)

Version: 1.5 (25-AUG-92) Requires: Standard ML Updated: Thu Aug 11 20:56:23 1994 CD-ROM: Prime Time Freeware for AI, Issue 1-1 Author(s): Lawrence C Paulson Computer Laboratory University of Cambridge Pembroke Street Cambridge CB2 3QG England Tel: +44-223-334600 Fax: +44-223-334678 [Isabelle] Tobias Nipkow Institut f\"ur Informatik TU M\"unchen 80290 M\"unchen Germany Tel: +49-89-21052690 Fax: +49-89-21058183 [Isabelle] Keywords: Authors!Paulson, Automated Reasoning, Denotational Semantics, Inference, LCF, Lazy Evaluation, ML!Code, Natural Deduction, PPLAMBDA, Reasoning!Automated Reasoning, Simplifiers, Theorem Proving, Univ. of Cambridge References: See the book "Logic and Computation" by L. Paulson, Cambridge University Press, 1987, for details.
Last Web update on Mon Feb 13 10:27:32 1995