• People
• Events
• Research

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

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

ECS-LFCS-89-74