Content deleted Content added
m <>cat |
No edit summary |
||
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 (Logic for Computable Functions) 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 [[datatype]].
The ML type system ensures that theorems are derived using only the inference rules given by the operations of the abstract type.
| |||