ACL2-AS-STANDALONE-PROGRAM

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 attempt.

(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))

(with-output :off :all (with-prover-time-limit 3 (thm ,@args)))

=== 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 acl2-init.lisp.)

(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.