CMU Artificial Intelligence Repository
LCF: Automated generic theorem prover
areas/reasonng/atp/systems/lcf/
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:
areas/reasonng/atp/systems/isabelle/
Origin:
ftp.cl.cam.ac.uk:/ml/ [128.232.0.56] (Univ. of Cambridge)
ftp.informatik.tu-muenchen.de:/lehrstuhl/nipkow/ [131.159.0.198]
(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
AI.Repository@cs.cmu.edu