[isabelle] FW: Cl-isabelle-users Digest, Vol 145, Issue 3



Dear Scott,

To address a broader question than the one you asked, you might like Mark
Adam's proof auditing paper, if you've not seen it:

http://www.proof-technologies.com/flyspeck/qed_paper.pdf

It looks at ways in which theorem provers might provide false assurances
(even in the absence of smuggled 'sorry' statements).

Best,

Colin

Date: Fri, 7 Jul 2017 09:37:14 -0700
From: scott constable <sdconsta at syr.edu>
Subject: [isabelle] Verify the legitimacy of a proof?
To: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>
Message-ID:
	<CADYF24fBE5-wFje-T9-z2c9Um4ZGf1y+ukaSiDi3EPa9uRBEaw at mail.gmail.com>
Content-Type: text/plain; charset="UTF-8"

Hi All,

Let's suppose I have some lemma

lemma ComplexProperty: "something interesting"
...
done

whose proof cites numerous other lemmas in other .thy files, possibly
written by other persons with malicious intentions. Is there a command in
Isabelle which I could use to determine the legitimacy of the entire proof
tree of ComplexProperty? That is, I want to ensure that no lemma in the
proof tree ended with "sorry", or if any axioms were used, I want to know
which ones, etc.

Thanks,

Scott Constable





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.