HW5 if you're using ACL2

[Sandip Ray]

Hi,

In case you want to use ACL2 for your homework, please follow these
instructions.

Please create a single lisp file with the definitions of functions
suggested and the theorems specified, in a sequence that is
processible by ACL2. We saw Matt Kaufmann produce such a file in
class interactively.

See the
http://www.cs.utexas.edu/users/moore/publications/tutorial/kaufmann-TPHOLs08/
for how such a file looks for Kaufmann's demos.

Please do not send multiple files for different homework questions.
You should send one file containing answers to _all_ the problems in
order. For the problems requiring you to define a function, there
should be an appropriate defun, and for the problems requiring you
to prove a theorem there must be a defthm. Please put a lisp
comment (a sequence of text lines each starting with ";") discussing
which definition is a solution to which problem.

Also, ACL2 must be able to successfully process the events in the
file sequentially. Thus, all auxiliary definitions must be present.
This means, for example, that you must write out a definition which
is already provided in the notes, if you are proving a theorem about
the function being defined. And if any auxiliary lemmas or
definitions are necessary then you need to state them as sppropriate
defthm and defun commands.

Please send the lisp file by email to both me and Warren.

For this homework, ACL2 will probably be able to prove all the
theorems automatically. But doing so will get you started on how to
interact with the system, which should be helpful in getting on with
your projects.

-- Sandip

[jdiamond]

It would be really cool after the homework is turned in to show us (if
possible) how to get ACL2 to prove #8. I think it's critical for the
project to figure out how to steer ACL2 to a larger proof.

[Sandip Ray]

Sure, I can show you. But as far as I can see ACL2 proves the theorem
automatically (with my definition of qvar-n). Did you just want to go
over the proof ACL2 did, or did you want something else?

-- Sandip

DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
d=googlegroups.com; s=beta;
h=domainkey-signature:received:received:x-sender:x-apparently-to
:mime-version:content-type:content-transfer-encoding:received:date
:in-reply-to:x-ip:references:user-agent:x-http-useragent:message-id
:subject:from:to:reply-to:sender:precedence:x-google-loop
:mailing-list:list-id:list-post:list-help:list-unsubscribe
:x-beenthere-env:x-beenthere;
bh=CznlNHYaU30ICwkXubEOqB5rufztp1Ggy93uJ/85xhU=;
b=Bq5Th3aLaZqCjDspDgNE7JStfN4uswHX4lykN59pEjF3UaGYH0PhrZSXL3Oxcv/lCl
EIqtfeIjpdIkGD6FbHS0RCeY7XSQM/zk42nRgDtuhWdlY7tO4rUhp7D1JB98N3YWPrMY
/9HnbcqX0MHVIwvg/b1SSig4HtC2QH1ULhRAc=
DomainKey-Signature: a=rsa-sha1; c=nofws;
d=googlegroups.com; s=beta;
h=x-sender:x-apparently-to:mime-version:content-type
:content-transfer-encoding:date:in-reply-to:x-ip:references
:user-agent:x-http-useragent:message-id:subject:from:to:reply-to
:sender:precedence:x-google-loop:mailing-list:list-id:list-post
:list-help:list-unsubscribe:x-beenthere-env:x-beenthere;
b=fDH1vgBdtyBbEPxPAjwT3subU+OILUUD65Ioj95FLNv5wO9rRrg8co7clOxWgKWVW7
DdUpDMp/+NB7l3/+BytjTFEQjkoEicq5+vehwysS7qkSVlat3jU7UXlvOJDMmGtEdDh+
IUTjqVmNpYdS9f2dmsZBYrBu28+HzcIq1uUvo=
X-Sender: jeffrey...@gmail.com
X-Apparently-To: utexas-cs38...@googlegroups.com
Date: Mon, 20 Oct 2008 08:44:16 -0700 (PDT)
X-IP: 32.97.110.57
X-HTTP-UserAgent: Mozilla/5.0 (Macintosh; U; Intel Mac OS X 10.5; en-US; rv:1.9.0.3) Gecko/2008092414 Firefox/3.0.3,gzip(gfe),gzip(gfe)
From: jdiamond <jeffrey...@gmail.com>
Reply-To: utexas-cs38...@googlegroups.com
Sender: utexas-cs38...@googlegroups.com
X-Google-Loop: groups
Mailing-List: list utexas-cs38...@googlegroups.com;
contact utexas-cs389r-...@googlegroups.com
X-BeenThere-Env: utexas-cs38...@googlegroups.com
X-SpamAssassin-Status: No, hits=0.6 required=5.0
X-UTCS-Spam-Status: No, hits=-130 required=165