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
Previous | Index | Next An error occured whilst processing this directive