coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Measuring the size of proofs

From: mulhern <mulhern AT gmail.com>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Measuring the size of proofs
Date: Fri, 21 Oct 2005 22:02:23 -0500
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:message-id:date:from:to:subject:mime-version:content-type:content-transfer-encoding:content-disposition; b=g/I6U0jU2tUFYjuP+QmgOTzjFyVeblPIzXR9Vwt7ku0l5CTWICkGIn8W38+GNR6lTNQP40H+XCBNX6PlSmYaJtrPcbdcqjTr4/VpCIKvUzi1ZdgDHCDfJDfrAOWNhuvtVgSIv81pmWK0F9mgGw1Gc456rXbweNnQbqNZq6EtW7w=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi!

I'm interesting in measuring the size of proofs.

The idea is that I change the goal or some of the underlying
definitions slightly, then I rebuild the proof and measure how the
size of the proof changes.

So far, the simples idea I can come up with is to print the xml
version of the proof and measure the number of characters. If the
(number of XML markup characters / number of proof data characters)
ratio is a constant this should work well enough. I'm considering this
approach because it can be automated and because it has the
granularity I need, i.e., I can do measurements on the size of a
single proof.

Is there an obviously better way to go about this?

Thanks!

-mulhern

[Coq-Club] Measuring the size of proofs, mulhern
- Re: [Coq-Club] Measuring the size of proofs, Claudio Sacerdoti Coen