Skip to content


Subversion checkout URL

You can clone with
Download ZIP
Work with TPTP files, theorem provers, and model finders
Shell Perl Emacs Lisp
Latest commit 17ba8dd Jesse Alama A couple of new tasks.
Failed to load latest commit information.
emacs Rearrange files by editor kind.
subethaedit dump .DS_Store files
.gitignore Ignore .scpt files.
README.mkdn Typo: extra quote. New feature: sentries that watch the output of a prover. Don't count the conjecture as an unused formula. expand using tptp4X Script (and sentry) for paradox. New feature: sentries that watch the output of a prover. Better regexp. tab
reprove fix symlink Report which model finders report countersatisfiability. Say 'unknown' rather than 'possibly not needed'. Die if we're given more than one argument. Theory in work dir. Use the sentries. Wrong number of models. Script (and sentry) for paradox. default timeout of 30 seconds for prover9. cruft More documenation. strip vampire proof output from standard input check for presence of tptp4X and GetSymbols. A couple of new tasks. Several new scripts to facilitate exploration with TPTP files. Look for the Timeout SZS term. permit multiply-defined formulas. wrong parameter


tptp-el: Hack TPTP with emacs and SubEthaEdit

Do you work with formal proofs in plain first-order logic? In Emacs? If you said "yes" to both questions, this package is for you.



Currently, the TPTP Emacs Lisp package consists of a single Emacs Lisp file, namely this one, tptp.el. Simply put tptp.el in a directory (I recommend "~/share/emacs/site-lisp/tptp", but it doesn't really matter), and in your Emacs initialization file (generally the file called ".emacs" in your home directory), add the form

(add-to-list 'load-path <path to the directory in which you put tptp.el>)
(require 'tptp)

Make sure the path is double quoted, e.g., "/Users/jesse". For slightly better performance of the TPTP Emacs Lisp package, byte compile tptp.el.

To automatically load tptp-mode when editing files with a certain extension, add something like this to your Emacs initialization file:

(add-to-list 'auto-mode-alist '("\\.ax\\" . tptp-mode))

Doing this will set up files that have the ".ax" extension to automatically load tptp-mode. You can do this for multiple extensions (e.g., ".p", ".ax", etc).


There is currently only one prover supported for SubEthaEdit: vampire. To install SubEthaEdit support for vampire:

  1. Make a bin subdirectory of your home directory, if it doesn't already exist.
  2. Copy to ~/bin, and make the script executable.
  3. Copy run-vampire.applescript to ~/Library/Application Support/SubEthaEdit/Scripts.

Next time you start SubEthaEdit, you should see, in the Scripts menu, an item that says "Run Vampire". Try it out!


You can follow development by going to the source homepage at

There you can get the latest bleeding edge development version of the package, as well as download choice releases.


Ed Zalta provided the impetus for launching this package.


You're welcome to email me at Please do let me know about bug reports, and feel free to make feature requests.

Something went wrong with that request. Please try again.