Laboratory of Informatics of Grenoble


An equational constraint solver

ECS is a system for solving equational constraints in the empty theory. We consider first-order formulae (with conjunction, disjunctions, negations, universal and existential quantifiers) which contain only the equality predicate "=". Equality is interpreted as syntactic identity between terms, and  variables range over the set of ground (finite) terms built on a given signature. 
These constraints have many application in automated deduction (model building, inductive reasoning etc.), in artificial intelligence and in computer science (program verification, handling of negation in logic programming...).

ECS is based on the quantifier elimination algorithm developed by  H. Comon et P. Lescanne (1989). Every formula can be reduced to either "false" (no solution) or to a disjunction of formulae in solved from, called "definition with constraints" which are defined by a substitution (a "most general solution") and a set of inequations imposing additional conditions on the free variables.

It has been developed by  Nicolas Peltier as a part of the ATINF project. It is implemented in C.

This program is provided without any warrantie. See here for details.
Laboratory of Informatics of Grenoble, CAPP Team