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). 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 (ESCAR), Tallinn, Estonia, 2005.
