Zobrazeno 1 - 2
of 2
pro vyhledávání: '"opentheory"'
Autor:
Mario M Carneiro
Publikováno v:
Journal of Formalized Reasoning, Vol 9, Iss 1, Pp 187-200 (2016)
We present an algorithm for converting proofs from the OpenTheory interchange format, which can be translated to and from any of the HOL family of proof languages (HOL4, HOL Light, ProofPower, and Isabelle), into the ZFC-based Metamath language. This
Externí odkaz:
https://doaj.org/article/55ce068158ab4dc4a2e77a7e0ce40d8f
Autor:
Thiré, François
Today, we observe a large diversity of proof systems. This diversity has the negative consequence that a lot of theorems are proved many times. Unlike programming languages, it is difficult for these systems to cooperate because they do not implement
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::6c7f972d62fd7937816241e290e49c21
https://hal.inria.fr/hal-01668250/document
https://hal.inria.fr/hal-01668250/document
