Major Section: ACL2-TUTORIAL
ACL2 is intended for interactive use. It is generally unrealistic to expect it to prove theorems fully automatically; see the-method, and see introduction-to-the-theorem-prover for a more detailed tutorial.
Nevertheless, here we describe an approach for how to call the ACL2 theorem prover noninteractively. These steps can of course be modified according to your needs. Here, we illustrate how to call ACL2 from another Lisp program (or an arbitrary program) to attempt to prove an arithmetic theorem.
=== STEP 1: ===
Build a suitable ACL2 image by starting ACL2 and then executing the following
forms. In particular, these define a macro,
try-thm, that causes ACL2 to
exit with with an exit status indicating success or failure of a proof
(include-book "arithmetic-5/top" :dir :system) (defmacro try-thm (&rest args) `(mv-let (erp val state) (with-prover-time-limit 3 (thm ,@args)) (declare (ignore val)) (prog2$ (if erp (exit 1) (exit 0)) state)))) (reset-prehistory) ; optional :q (save-exec "arith-acl2" "Included arithmetic-4/top")
If you prefer, above you can replace 3 by some other number of seconds as a time limit for the prover. Also, you can replace
(with-prover-time-limit 3 (thm ,@args))by
(with-output :off :all (with-prover-time-limit 3 (thm ,@args)))if you want to turn off output. It may be best to leave the output on, instead eliminating it in the calling program (see Step 3 below).
=== STEP 2: ===
Try a little test. In that same directory try this:
echo '(try-thm (equal x x))' | ./arith-acl2 echo $?
The exit status should be 0, indicating success. Now try this:
echo '(try-thm (not (equal x x)))' | ./arith-acl2 echo $?
The exit status should be 1, indicating failure.
=== STEP 3: ===
Create a shell script that automates Step 2, for example:
#!/bin/sh (echo "(try-thm $1)" | ./arith-acl2) >& /dev/null exit $?
=== STEP 4: ===
Try your script from a Lisp program, if you like. Here is how you can do it
in SBCL, for example. (Different Lisps have different ways to do this, as
summarized in function
system-call in ACL2 source file
(defun provable? (x) (let ((status (process-exit-code (sb-ext:run-program "./try-thm.sh" (list (format nil "~s" x)) :output t :search t)))) (eql status 0)))
Then here is a log:
* (provable? '(equal x y)) NIL * (provable? '(equal x x)) T *
Certainly refinements are possible -- for example the above doesn't distinguish between unprovable and ill-formed input. But it's a start.