Non User
Index: > A B C D E F G H I J K L M N O P Q R S T U V W X Y Z	Business Non User Industries Finance Tax

Home > LCF theorem prover

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 the

Politics	Business	Finance

Topics: LCF Theorem Prover Abstract System Type Theorems Tactics...

---

LCFLog control function Longitudinal center of flotation Launch control facility Low cycle fatigue LCF theorem prover TLAs. LCF theorem proverAn interactive 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 propos LCFGLCFG stands for "Local ConFiGuration system". Developed at Edinburgh University beginning around 1993, it is "a system for automatically installing and managing the configuration of large numbers of computer systems. It is particularly suitable for sites