| 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) HOL (Higher Order Logic) — семейство инструментов интерактивного доказательства теорем, при создании которых были использованы схожие подходы к построению доказательств, основанные на логике высшего порядка и схожие подходы к реализации. HOL развивает подход системы LCF. (ru) |
| dbo:designer |
dbr:Michael_J_C_Gordon |
| dbo:license |
dbr:BSD_licenses |
| dbo:wikiPageExternalLink |
http://hol-theorem-prover.org/ http://prdownloads.sourceforge.net/hol/kananaskis-3-description.pdf%3Fdownload http://proof-technologies.com/holzero/index.html http://www.lemma-one.com/ProofPower/specs/specs.html http://www.cl.cam.ac.uk/~mjcg/papers/HolHistory.html http://www.lemma-one.com/ProofPower/index/ https://web.archive.org/web/20051219153731/http:/vl.fmnet.info/hol/ |
| dbo:wikiPageID |
161888 (xsd:integer) |
| dbo:wikiPageLength |
6778 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID |
1116677452 (xsd:integer) |
| dbo:wikiPageWikiLink |
dbr:Power_ISA dbr:Proof_assistant dbc:Software_using_the_BSD_license dbr:Common_Lisp dbr:Moscow_ML dbr:Theorem dbr:Lisp_(programming_language) dbr:ML_(programming_language) dbr:Standard_ML dbr:BSD_licenses dbr:HOL_Light dbr:ARM_architecture dbr:Abstract_data_type dbr:Machine_code dbr:Isabelle_(proof_assistant) dbr:Coupling_(computer_programming) dbr:Michael_J_C_Gordon dbc:Logic_in_computer_science dbc:Proof_assistants dbr:Higher-order_logic dbr:Z_notation dbr:Poly/ML dbr:Classical_logic dbr:OCaml dbr:Semantics_(computer_science) dbr:Caml_Light dbr:LCF_(theorem_prover) dbr:Mike_Gordon_(computer_scientist) dbr:Inference_rule |
| dbp:designer |
dbr:Michael_J_C_Gordon |
| dbp:fileExt |
.sml (en) |
| dbp:license |
dbr:BSD_licenses |
| dbp:name |
HOL (en) |
| dbp:wikiPageUsesTemplate |
dbt:Cite_web dbt:Expand_section dbt:Infobox_programming_language dbt:Reflist dbt:Short_description dbt:Url |
| dct:subject |
dbc:Software_using_the_BSD_license dbc:Logic_in_computer_science dbc:Proof_assistants |
| rdf:type |
owl:Thing dbo:Language schema:Language wikidata:Q315 wikidata:Q9143 yago:Assistant109815790 yago:CausalAgent100007347 yago:LivingThing100004258 yago:Object100002684 yago:Organism100004475 yago:Person100007846 yago:PhysicalEntity100001930 yago:Worker109632518 yago:YagoLegalActor yago:YagoLegalActorGeo dbo:ProgrammingLanguage yago:Whole100003553 yago:WikicatProofAssistants |
| rdfs:comment |
HOL (Higher Order Logic) — семейство инструментов интерактивного доказательства теорем, при создании которых были использованы схожие подходы к построению доказательств, основанные на логике высшего порядка и схожие подходы к реализации. HOL развивает подход системы LCF. (ru) 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) HOL (ru) |
| owl:sameAs |
freebase:HOL (proof assistant) yago-res:HOL (proof assistant) wikidata:HOL (proof assistant) dbpedia-ru:HOL (proof assistant) https://global.dbpedia.org/id/fWc8 |
| prov:wasDerivedFrom |
wikipedia-en:HOL_(proof_assistant)?oldid=1116677452&ns=0 |
| foaf:isPrimaryTopicOf |
wikipedia-en:HOL_(proof_assistant) |
| foaf:name |
HOL (en) |
| is dbo:wikiPageDisambiguates of |
dbr:HOL |
| is dbo:wikiPageRedirects of |
dbr:HOL4 dbr:HOL_theorem_prover dbr:HOL_theorem_prover_family |
| is dbo:wikiPageWikiLink of |
dbr:Department_of_Computer_Science_and_Technology,_University_of_Cambridge dbr:Interactive_Theorem_Proving_(conference) dbr:Coq dbr:Separation_logic dbr:GNU_Common_Lisp dbr:Standard_ML dbr:Compiler_correctness dbr:Type_theory dbr:Logic_for_Computable_Functions dbr:Agda_(programming_language) dbr:HOL dbr:Isabelle_(proof_assistant) dbr:Higher-order_logic dbr:HOL4 dbr:HOL_theorem_prover dbr:HOL_theorem_prover_family |
| is foaf:primaryTopic of |
wikipedia-en:HOL_(proof_assistant) |