Skip to Main content Skip to Navigation

Déduction automatique avec contraintes symboliques dans les théories équationnelles

Abstract : 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.
Document type :
Complete list of metadata

Cited literature [86 references]  Display  Hide  Download
Contributor : Thèses UL Connect in order to contact the contributor
Submitted on : Thursday, March 29, 2018 - 11:43:20 AM
Last modification on : Thursday, March 31, 2022 - 8:41:04 AM
Long-term archiving on: : Friday, September 14, 2018 - 7:52:38 AM


Files produced by the author(s)


  • HAL Id : tel-01748621, version 1



Laurent Vigneron. Déduction automatique avec contraintes symboliques dans les théories équationnelles. Informatique [cs]. Université Henri Poincaré - Nancy 1, 1994. Français. ⟨NNT : 1994NAN10371⟩. ⟨tel-01748621⟩



Record views


Files downloads