Logic for Computable Functions: Difference between revisions

Revision as of 01:45, 27 December 2002

Revision as of 04:56, 29 December 2002

Line 1:

A '''theorem prover''' was developed at [[University of Edinburgh]] by [[Robin Milner]].

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

Theorems are proposition of special "theorem" type,

the ML type system ensures that theorems are derived using only sound

inference rules.

Successors include:

[[HOL theorem prover]], [[Isabelle theorem prover]].