daTac

daTac - Déduction Automatique dans des Théories Associatives-Commutatives. The aim of the system daTac is to do automated deduction in first-order logic with equality. Its speciality is to apply deductions modulo some equational properties of operators, such as commutativity or associativity-commutativity (AC). The deduction techniques implemented, based on resolution, paramodulation and term rewriting, have been proved refutationally complete in [RV95]. Several strategies are available: Selection of Deduction Steps: two strategies for selecting terms, literals and clauses are proposed, the ordering and positive-ordering strategies. Both are based on an ordering for comparing objects [Vig95]. Symbolic Constraints: the basic strategy is implemented in daTac [Vig94]. Elimination of Redundant Information: several strategies for eliminating redundant information have been implemented, such as demodulation, subsumption (forward and backward), tautology elimination, clausal simplification. daTac is written in Objective Caml 3.04 (22000 lines), a functional language of the ML family. Its interface is written in Tcl/Tk (8000 lines). It runs on Linux and Solaris workstations.