[isabelle] FW: Cl-isabelle-users Digest, Vol 145, Issue 3
- To: <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] FW: Cl-isabelle-users Digest, Vol 145, Issue 3
- From: "Colin Rowat" <c.rowat at espero.org.uk>
- Date: Sat, 8 Jul 2017 11:21:11 +0100
- In-reply-to: <firstname.lastname@example.org>
- References: <email@example.com>
- Thread-index: AQJJ5+TKFTUIcyFf0H5mQDbuknr+daFb1rBA
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:
It looks at ways in which theorem provers might provide false assurances
(even in the absence of smuggled 'sorry' statements).
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>
<CADYF24fBE5-wFje-T9-z2c9Um4ZGf1y+ukaSiDi3EPa9uRBEaw at mail.gmail.com>
Content-Type: text/plain; charset="UTF-8"
Let's suppose I have some lemma
lemma ComplexProperty: "something interesting"
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and