LCF (theorem prover)

LCF (theorem prover)

LCF (Logic for Computable Functions) is an interactive automated theorem prover developed at the universities of Edinburgh and Stanford by Robin Milner and others. LCF introduced the general purpose programming language ML to allow users to write theorem proving tactics. Theorems in the system are propositions of a special "theorem" abstract datatype. The ML type system ensures that theorems are derived using only the inference rules given by the operations of the abstract type.

Successors include HOL and Isabelle.

References

* cite web
last = Gordon
first = Michael J. C.
authorlink = Michael J. C. Gordon
year=1996
title = From LCF to HOL: a short history
url = http://www.cl.cam.ac.uk/~mjcg/papers/HolHistory.html
accessdate = 2007-10-11


Wikimedia Foundation. 2010.

Игры ⚽ Поможем написать реферат

Look at other dictionaries:

  • Isabelle (theorem prover) — Infobox Software name = Isabelle caption = collapsible = author = developer = released = latest release version = latest release date = latest maintenance version = latest maintenance date = latest preview version = latest preview date =… …   Wikipedia

  • LCF — The term LCF may refer to:* Boeing 747 Large Cargo Freighter * Log control function * Longitudinal center of flotation * Launch control facility * Logic of Computable Functions * London College of Fashion * Low cycle fatigue * LCF theorem prover… …   Wikipedia

  • HOL theorem prover family — HOL (Higher Order Logic) denotes a family of interactive theorem proving systems sharingsimilar logics and implementation strategies. Systems in this family follow the LCF approach as they are implemented as a library in some programming language …   Wikipedia

  • Interactive theorem proving — is the field of computer science and mathematical logic concerned with tools to develop formal proofs by man machine collaboration. This involves some sort of proof assistant: an interactive proof editor, or other interface, with which a human… …   Wikipedia

  • Automated theorem proving — (ATP) or automated deduction, currently the most well developed subfield of automated reasoning (AR), is the proving of mathematical theorems by a computer program. Decidability of the problem Depending on the underlying logic, the problem of… …   Wikipedia

  • List of mathematical logic topics — Clicking on related changes shows a list of most recent edits of articles to which this page links. This page links to itself in order that recent changes to this page will also be included in related changes. This is a list of mathematical logic …   Wikipedia

  • ML (programming language) — ML Paradigm(s) multi paradigm: imperative, functional Appeared in 1973 Designed by Robin Milner others at the University of Edinburgh Typing discipline static, strong, inferred …   Wikipedia

  • Demostración automática de teoremas — Saltar a navegación, búsqueda Para otros usos de este término, véase Demostración. La demostración automática de teoremas (de siglas ATP, por el término en inglés …   Wikipedia Español

Share the article and excerpts

Direct link
… Do a right-click on the link above
and select “Copy Link”