ECS
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