daTac

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

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:

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.

daTac-0.93 is now available:

daTac without graphical interface:

daTac-0.93.linux.tar.gz (358 Kb): Binary files for Linux PCs (Red Hat 6.2), manual, examples.
daTac-0.93.sol.tar.gz (518 Kb): Binary files for Sun workstations (Solaris, i.e. SunOS 5.*), manual, examples.

daTac with the graphical interface:

daTac-0.93.interf.misc.tar.gz (158 Kb): Common files for the graphical interface (lib, src, help, examples).

daTac-0.93.interf.linux.tar.gz (972 Kb): Binary files for Linux PCs (Red Hat 6.2), and libraries.
daTac-0.93.interf.sol.tar.gz (1252 Kb): Binary files for Sun workstations (Solaris, i.e. SunOS 5.*), and libraries.

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:

bin

examples

help

lib

src

Five files are also copied in the directory daTac-0.93:

README

CHANGES

INSTALL

daTac

rdaTac

Applications:

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:

[LPAR] Compiling and Verifying Security Protocols. In M. Parigot and A. Voronkov, editors, Seventh International Conference on Logic for Programming and Automated Reasoning, LPAR 2000, volume 1955 of Lecture Notes in Computer Science, pages 131-160, St Gilles (Reunion, France), November 2000. Springer-Verlag.

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:

[RSKD] A. Walislewska and L. Vigneron. Rough Algebras and Automated Deduction. In L. Polkowski and A. Skowron, editors, Rough Sets in Knowledge Discovery 1. Springer Verlag, 1998.
[FI] L. Vigneron. Automated Deduction Techniques for Studying Rough Algebras. Fundamenta Informaticae, 33(1):85-103, February 1998.
[CESA] L. Vigneron and A. Walislewska. Rough and Modal Algebras. In P. Borne, editor, Proceedings of the IMACS/IEEE CESA'96 International Multiconference (Computational Engineering in Systems Applications), Symposium on Modelling, Analysis and Simulation, Lille (France), pages 1107-1112, July 1996.

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 @ loria.fr
https://members.loria.fr/lvigneron/
member of the Pesto Group, LORIA (Nancy, France)