<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On 7 August 2015 at 00:30, Günter Rote <span dir="ltr"><<a href="mailto:rote@inf.fu-berlin.de" target="_blank">rote@inf.fu-berlin.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I am trying to write an article reader in python, mainly to<br>
get an understanding how the steps of a formal proof in HOL look like.<br></blockquote><div><br></div><div>Sounds like a good idea.<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

My question concerns the definition of *defineTypeOp*<br>
in the article file format<br>
<a href="http://www.gilith.com/research/opentheory/article.html" rel="noreferrer" target="_blank">http://www.gilith.com/research/opentheory/article.html</a><br>
<br>
Since the new constants *abs* and *rep*<br>
appear in a term like "(⊦ (λa. abs (rep a)) = λa. a)",<br>
they must have some type:<br>
<br>
I guess the new type operator op with name n has<br>
type parameters α1 ... αk in this order, and<br>
the types of rep and abs are<br>
 rep:: n α1 ... αk -> b<br>
 abs:: b -> n α1 ... αk (using prefix notation for the type-operator)<br>
where b is the type of t<br>
Is that true?<br></blockquote><div><br></div><div>That is correct.<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

In the definition of *opType*, is it required that<br>
the length n of the list equals the k with which<br>
the type-operator "op" has been defined?<br></blockquote><div><br></div><div>Kind of true, but not really. Type operators can be constructed by the virtual machine even if they have not previously been defined in the same article. In that case, the type operator will be one of the "external type operators" (i.e., an input) to the resulting theory. (N.B. if you use *typeOp* to create a type operator with the same name as one created by *defineTypeOp*, they won't alias each other; i.e., if you want to use the type defined by *defineTypeOp* you have to use the TypeOp object that it returns. Some related previous mails on this point: <a href="http://www.gilith.com/opentheory/mailing-list/2011-January/000080.html">http://www.gilith.com/opentheory/mailing-list/2011-January/000080.html</a>.)<br><br></div><div>However, I think if you are using a type operator whose definition is known and supply the wrong number of arguments, article processing will fail. Joe can probably confirm and clarify this.<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

(Maybe my question is based on a basic misunderstanding:<br>
Can opentheory be used as a proof verifier?<br>
I.e. If an article file goes through opentheory without<br>
errors, does it mean that the listed "theorems" can be<br>
derived from the "assumptions" (using the OpenTheory derivation rules)?<br></blockquote><div><br></div><div>Yes. The opentheory tool can be used to verify that articles obey the derivation rules of (OpenTheory's variant of) HOL.<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

(I have seen talks about proof verification by transforming opentheory to<br>
dedukti (or rather HOL via opentheory to dedukti) and then verifying the<br>
proof in dedukti. What would be the point of this if this<br>
verification is also fine in opentheory?)<br></blockquote><div><br></div><div>There are at least two points to make here:<br></div><div><br>1. Dedukti verifies proofs in a different logical system, lambda pi modulo rewriting, in which HOL (e.g., OpenTheory) can be embedded. The idea is that it could be a place where theories from different logics could be combined. Thus it makes sense to import into Dedukti, even if you trust the opentheory-checked version is correct, to allow the connection with other things in Dedukti.<br><br></div><div>2. It's always good to have multiple implementations of a proof checker, since proof checkers can contain bugs but the chances of two very different implementations having the same bugs are low. (To be clear, proof checkers don't typically have many bugs, but it's possible.) The opentheory tool wasn't designed primarily as a proof checker (it has other design goals too), so it's not the smallest and simplest piece of code doing that job, hence maybe you would prefer to trust an independent, purpose-built checker. (I don't think Dedukti is that either though.) The CakeML project (of which I'm a developer) takes the idea of reducing the need to trust the proof checker to an extreme: we are working on a proof checker whose machine-code implementation is itself verified to only accept theories that are true in all (standard) models of higher-order logic. (Verified in the sense of having a proof in OpenTheory deriving that fact.)<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<span class="HOEnZb"><font color="#888888"><br>
--<br>
G"unter Rote (Germany=49)30-838-75150 (office)<br>
Freie Universit"at Berlin<br>
Institut f"ur Informatik<br>
<br>
</font></span><br>_______________________________________________<br>
opentheory-users mailing list<br>
<a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a><br>
<a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
<br></blockquote></div><br></div></div>