daTac daTac - Déduction Automatique dans des Théories Associatives-Commutatives daTac

Pesto Group (former Cassis Group), LORIA (Nancy, France).

What is daTac?

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: 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.

daTac-0.93 is now available:

daTac without graphical interface: daTac with the graphical interface: For installing daTac, you need at least one compressed file containing binaries, and one of the compressed interface files.
For uncompressing files, use: A directory daTac-0.93 is created. A complete installation generates the following sub-directories: Five files are also copied in the directory daTac-0.93:


daTac has being used intensively in the CASSIS group for verifying cryptographic protocols. Its role is to find attacks in protocols, after they have been compiled by the CASRUL system.
This work is described in: daTac is also used with Anita Wasilewska (Stony Brook University, NY), for the study of non-classical logics modelled by rough sets. This theory of rough sets provides a methodological framework for studying classification problems with imprecise or incomplete information.
We have used daTac for discovering new theorems in two modal and two rough classes of algebras, and to examine the relationship between these classes.
Our main results have been published in the following papers:

Citing daTac:

If you want to cite daTac in a paper written in LaTeX, you can use the following definition:

\newcommand\DATAC{{\textsf{\setbox0\hbox{T}da\raise.1\wd0\hbox to.4\wd0{\hss T\hss}ac}}}

Just a simple example for your next paper: I have used \DATAC\ for proving that NP is equal to P; this was impossible with any other prover, except \DATAC. ;-)

daTac has received an IDDN (Inter Deposit Digital Number) certificate: IDDN.FR.001.140010.00.R.P.2000.000.10000
So feel free to use it and distribute it, provided you always mention its name in your publications.
Please send questions, remarks or bugs to the author.

Author of daTac : Laurent.Vigneron @
member of the Pesto Group, LORIA (Nancy, France)