Skip to Main content Skip to Navigation
Theses

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 :
Theses
Complete list of metadata

Cited literature [86 references]  Display  Hide  Download

https://hal.univ-lorraine.fr/tel-01748621
Contributor : Thèses Ul <>
Submitted on : Thursday, March 29, 2018 - 11:43:20 AM
Last modification on : Friday, February 26, 2021 - 3:26:01 PM
Long-term archiving on: : Friday, September 14, 2018 - 7:52:38 AM

File

SCD_T_1994_0371_VIGNERON.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : tel-01748621, version 1

Collections

Citation

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

Share

Metrics

Record views

71

Files downloads

93