Automated deduction with associative commutative operators

Michaël Rusinowitch 1 Laurent Vigneron 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We propose a new inference system for automated deduction with equality and associative commutative operators. This system is an extension of the ordered paramodulation strategy. However, rather than using associativity and commutativity as the other axioms, they are handled by the AC-unification algorithm and the inference rules. Moreover, we prove the refutational completeness of this system without needing the functional reflexive axioms or AC-axioms. Such a result is obtained by semantic tree techniques. We also show that the inference system is compatible with simplification rules.
Type de document :
Rapport
[Research Report] RR-1896, INRIA. 1993, pp.34
Liste complète des métadonnées

https://hal.inria.fr/inria-00074775
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 16:17:12
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58
Document(s) archivé(s) le : mardi 12 avril 2011 - 19:19:45

Fichiers

Identifiants

  • HAL Id : inria-00074775, version 1

Collections

Citation

Michaël Rusinowitch, Laurent Vigneron. Automated deduction with associative commutative operators. [Research Report] RR-1896, INRIA. 1993, pp.34. 〈inria-00074775〉

Partager

Métriques

Consultations de la notice

229

Téléchargements de fichiers

65