Automated deduction with symbolic constraints in equational theories
Déduction automatique avec contraintes symboliques dans les théories équationnelles
Résumé
In this document, we propose techniques of automated deduction for proving properties by refutation in first order logic, These proofs are done modulo a set of axioms forming a regular theory E.
The Inference systems defined are based on resolution and paramodulation rules, We propose several strategies for selecting clauses (ordered or positive) and for applying replacements (paramodulation or superposition). Our Inference rules avoid the combinatory of a direct use of axioms of E by a calculus of replacements contexts and an algorithm for unification modulo E. In addition to these inference rules, we define simplification rules which permit the deletion of redundant clauses. These systems are proved refutationally complete by an extension of the transfinite semantic trees technique. For associative and commutative theories, we show that we can avoid to solve unification problems. We only have a test the existence of a solution. Each unification problem is added to the deduced clause as a constraint, and each unsolved condition for applying the deduction is added as a constraint too. This constrained strategy simulates the basic strategy and generates only one clause deduction step, instead of as many as solutions of the unification problem. We describe the system DATAC, implementing the results presented in this document, for associative and commutative theories.
Nous proposons dans ce document des techniques de déduction automatique pour effectuer des preuves de propriétés par réfutation dans la logique du premier ordre. Ces preuves sont réalisées modulo un ensemble d'axiomes formant une théorie régulière e. Les systèmes d'inférence définis sont fondés sur les règles de résolution et de paramodulation. Nous proposons plusieurs stratégies de sélection de clauses (ordonnée ou positive), et de remplacement (paramodulation ou superposition). Nos règles d'inférence évitent la combinatoire de l'usage des axiomes de e, par un calcul de contextes de remplacements et un algorithme d'unification modulo e. En plus de ces règles d'inférence, nous définissons des règles de simplification permettant d'éliminer les clauses redondantes. Nous démontrons la complétude refutationnelle de ces systèmes grâce à une extension de la technique des arbres sémantiques transfinis. Pour le cas des théories associatives et commutatives, nous montrons que l'on peut éviter de résoudre les problèmes d'unification. Seul le test d'existence d'une solution est nécessaire. Ainsi, tout problème d'unification est ajouté à la clause déduite sous la forme d'une contrainte, de même que toute autre condition non résolue pour appliquer l'inférence. Cette stratégie contrainte simule la stratégie basique et n'engendre qu'une seule clause par étape d'inférence, au lieu d'autant de clauses que de solutions au problème d'unification rencontre. Nous décrivons le logiciel datac , implantant les résultats présentés dans ce document, pour le cas des théories associatives et commutatives.
Domaines
Informatique [cs]| Origine | Fichiers produits par l'(les) auteur(s) |
|---|
Loading...