HOL (Higher Order Logic) denotes a family of interactive theorem proving systems sharing similar logics and implementation strategies. Systems in this family follow the LCF approach as they are implemented as a library in some programming language. This library implements an abstract data type of proven theorems so that new objects of this type can only be created using the functions in the library which correspond to inference rules in higher-order logic.

PropertyValue
dbpprop:abstract
  • HOL (Higher Order Logic) denotes a family of interactive theorem proving systems sharing similar logics and implementation strategies. Systems in this family follow the LCF approach as they are implemented as a library in some programming language. This library implements an abstract data type of proven theorems so that new objects of this type can only be created using the functions in the library which correspond to inference rules in higher-order logic. As long as these functions are correctly implemented, all theorems proven in the system must be valid. In this way, a large system can be built on top of a small trusted kernel. Systems in the HOL family use the ML programming language or its successors. ML was originally developed along with LCF to serve the purpose of a meta-language for theorem proving systems; in fact, the name stands for "Meta-Language".
dbpprop:hasPhotoCollection
dbpprop:reference
rdfs:comment
  • HOL (Higher Order Logic) denotes a family of interactive theorem proving systems sharing similar logics and implementation strategies. Systems in this family follow the LCF approach as they are implemented as a library in some programming language. This library implements an abstract data type of proven theorems so that new objects of this type can only be created using the functions in the library which correspond to inference rules in higher-order logic.
rdfs:label
  • HOL theorem prover family
owl:sameAs
skos:subject
foaf:page
is dbpprop:redirect of