Tau (theorem prover)

Tau is a robust and general purpose, interactive (live on the web), user-configurable automated theorem prover for first-order predicate logic with equality. Tau proves both theorems and arguments expressed in unrestricted first-order notation in the KIF (knowledge interchange format) language. It combines rule-based problem rewriting with model elimination (both full and weak), uses Brand’s modification method to implement equality handling, and accepts user-configurable heuristic search to speed the search for proofs. Tau optionally implements mathematical induction (both strong and weak). Formulas are input and output in KIF or its own infix first-order syntax, and other syntactic forms can be added. Tau is operated from a Web interface or from a command-line interface. It is implemented entirely in Java.

Other features include tautology and subsumption deletion; depth-, breadth-, and modified-best-searching; use of unit lemmas; instantiation and generalization strategies; finite model checking; extensibility.

References

* Halcomb, Jay and Randall R. Schulz (2005). [http://hsinfosystems.com/taujay/doc/Workshop.pdf Tau: A Web-Deployed Hybrid Prover for First-Order Logic with Identity, with Optional Inductive Proof] . Proceedings of the CADE-20 Workshop on Empirically Successful Classical Automated Reasoning ( [http://www.cs.miami.edu/~geoff/Conferences/ESCAR/ ESCAR] ), Tallinn, Estonia, 2005.

External links

* [http://hsinfosystems.com/taujay/index.html Tau on the web]
* [http://64.142.14.4/mediawiki/index.php/Main_Page TauWiki documentation]