THORN: A Theorem-Prover that compiles first-order Logic into LISP

Mark Tarver

Abstract: Backwards-chaining theorem-prover for first-order predicate logic with identity. Based on the Prolog Technology Theorem-Prover of Mark Stickel, THORN receives UNIX text files containing wffs and compiles them down to LISP functions. Proofs automatically generated. Franz LISP only; for use on the VAX family of machines. has been withdrawn


Previous | Index | Next