LCF theorem prover

E230806

interactive theorem prover proof assistant software system

The LCF theorem prover is an early interactive proof system that pioneered the use of higher-order logic and the LCF-style architecture, forming the conceptual basis for later provers like HOL and Isabelle.

Try in SPARQL Jump to: Surface forms Statements Referenced by

All labels observed (2)

Label	Occurrences
LCF theorem prover canonical	5
Logic for Computable Functions theorem prover	1

Statements (43)

Predicate	Object
instanceOf	interactive theorem prover ⓘ proof assistant ⓘ software system ⓘ
basedOn	higher-order logic ⓘ
category	computer-assisted proof system ⓘ
conceptualBasisFor	HOL theorem prover ⓘ surface form: HOL theorem prover family Isabelle logical framework ⓘ
contributedTo	development of ML ⓘ
designedBy	Robin Milner ⓘ
developedAt	University of Edinburgh ⓘ
ensures	soundness via abstract data types ⓘ
era	1970s ⓘ
field	automated reasoning ⓘ formal methods ⓘ mathematical logic ⓘ
fullName	LCF theorem prover self-linksurface differs ⓘ surface form: Logic for Computable Functions theorem prover
hasAbbreviation	LCF ⓘ
hasArchitectureStyle	LCF-style architecture ⓘ
hasCoreComponent	logical inference kernel ⓘ tactic mechanism ⓘ theorem abstract type ⓘ
hasDesignGoal	machine-assisted formal proof ⓘ reliable proof checking ⓘ
hasDesignPrinciple	separation of logic kernel and tactics ⓘ soundness by construction ⓘ
hasKeyConcept	abstract data types for theorems ⓘ small trusted kernel ⓘ user-level proof tactics ⓘ
implementedIn	ML ⓘ
influenced	HOL theorem prover ⓘ surface form: HOL theorem provers Isabelle proof assistant ⓘ surface form: Isabelle theorem prover ML programming language design ⓘ
isEarlyExampleOf	interactive proof system ⓘ
notableFor	inspiring later LCF-style provers ⓘ introduction of tactic-based proof construction ⓘ pioneering higher-order logic in interactive provers ⓘ
pioneered	LCF-style architecture ⓘ
relatedTo	HOL Light ⓘ HOL4 ⓘ Isabelle proof assistant ⓘ surface form: Isabelle/HOL
supports	interactive proof development ⓘ user-defined proof strategies ⓘ
usesLogic	higher-order logic ⓘ

Referenced by (6)

Full triples — surface form annotated when it differs from this entity's canonical label.

Robin Milner → knownFor → LCF theorem prover ⓘ

ML → originatedInContextOf → LCF theorem prover ⓘ

Arthur John Robin Gorell Milner → notableWork → LCF theorem prover ⓘ

Arthur John Robin Gorell Milner → developed → LCF theorem prover ⓘ

LCF theorem prover → fullName → LCF theorem prover self-linksurface differs ⓘ

this entity surface form: Logic for Computable Functions theorem prover

Arthur → notableWork → LCF theorem prover ⓘ

subject surface form: Arthur John Robin Gorell Milner