Deduction with symbolic constraints
Résumé
A framework for first-order constrained deduction is proposed in this paper. The syntax and semantics of symbolic constraints and constrained formulae are defined. Constrained deduction rules are given for equational logic and for first-order logic with equality. They are applied to clausal theorem proving, unfailing completion and completion modulo a set of axioms.