An Entity of Type: language, from Named Graph: http://dbpedia.org, within Data Space: dbpedia.org

HOL (Higher Order Logic) denotes a family of interactive theorem proving systems using similar (higher-order) logics and implementation strategies. Systems in this family follow the LCF approach as they are implemented as a library which defines an abstract data type of proven theorems such 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. As such, a large system can be built on top of a small trusted kernel.

Property Value
dbo:abstract
  • HOL (Higher Order Logic) denotes a family of interactive theorem proving systems using similar (higher-order) logics and implementation strategies. Systems in this family follow the LCF approach as they are implemented as a library which defines an abstract data type of proven theorems such 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. As such, a large system can be built on top of a small trusted kernel. Systems in the HOL family use ML or its successors. ML was originally developed along with LCF as a meta-language for theorem proving systems; in fact, the name stands for "Meta-Language". (en)
dbo:designer
dbo:license
dbo:wikiPageExternalLink
dbo:wikiPageID
  • 161888 (xsd:integer)
dbo:wikiPageLength
  • 6954 (xsd:nonNegativeInteger)
dbo:wikiPageRevisionID
  • 996632371 (xsd:integer)
dbo:wikiPageWikiLink
dbp:designer
dbp:fileExt
  • .sml (en)
dbp:license
dbp:name
  • HOL (en)
dbp:wikiPageUsesTemplate
dct:subject
rdf:type
rdfs:comment
  • HOL (Higher Order Logic) denotes a family of interactive theorem proving systems using similar (higher-order) logics and implementation strategies. Systems in this family follow the LCF approach as they are implemented as a library which defines an abstract data type of proven theorems such 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. As such, a large system can be built on top of a small trusted kernel. (en)
rdfs:label
  • HOL (proof assistant) (en)
owl:sameAs
prov:wasDerivedFrom
foaf:isPrimaryTopicOf
foaf:name
  • HOL (en)
is dbo:knownFor of
is dbo:wikiPageDisambiguates of
is dbo:wikiPageRedirects of
is dbo:wikiPageWikiLink of
is dbp:knownFor of
is foaf:primaryTopic of
Powered by OpenLink Virtuoso    This material is Open Knowledge     W3C Semantic Web Technology     This material is Open Knowledge    Valid XHTML + RDFa
This content was extracted from Wikipedia and is licensed under the Creative Commons Attribution-ShareAlike 3.0 Unported License