CMU Artificial Intelligence Repository
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.]
ftp.cl.cam.ac.uk:/ml/ [126.96.36.199] (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
University of Cambridge
Cambridge CB2 3QG
Institut f\"ur Informatik
Authors!Paulson, Automated Reasoning, Denotational Semantics,
Inference, LCF, Lazy Evaluation, ML!Code, Natural Deduction,
PPLAMBDA, Reasoning!Automated Reasoning, Simplifiers,
Theorem Proving, Univ. of Cambridge
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