Logic for Computable Functions: Difference between revisions

Revision as of 04:46, 2 October 2003

Revision as of 17:31, 2 September 2004

Line 1:

An interactive '''theorem prover''' developed at the universities of [[University of Edinburgh|Edinburgh]] and [[Stanford University|Stanford]] by [[Robin Milner]] and others.

LCF introduced the general purpose [[programming language]] [[ML programming language|ML]] to allow users to write theorem proving tactics.

Theorems in the system are propositions of a special "theorem" abstract type[[datatype]].

The ML type system ensures that theorems are derived using only soundthe inference rules given by the operations of the abstract type.

inference rules.

Successors include the

[[HOL theorem prover|HOL]] and [[Isabelle theorem prover|Isabelle]] theorem provers.

[[Category:mathematical logic]]