Deriving Theory Superposition Calculi from Convergent Term Rewriting Systems

Jürgen Stuber 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We show how to derive refutationally complete ground superposition calculi systematically from convergent term rewriting systems for equational theories, in order to make automated theorem proving in these theories more effective. In particular we consider abelian groups and commutative rings. These are difficult for automated theorem provers, since their axioms of associativity, commutativity, distributivity and the inverse law can generate many variations of the same equation. For these theories ordering restrictions can be strengthened so that inferences apply only to maximal summands, and superpositions into the inverse law that move summands from one side of an equation to the other can be replaced by an isolation rule that isolates the maximal terms on one side. Additional inferences arise from superpositions of extended clauses, but we can show that most of these are redundant. In particular, none are needed in the case of abelian groups, and at most one for any pair of ground clauses in the case of commutative rings.
Type de document :
Communication dans un congrès
Leo Bachmair. International Conference on Rewriting Techniques & Applications - RTA'2000, 2000, Norwich, UK, Springer-Verlarg, 1833, pp.229-245, 2000, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00099187
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 08:51:38
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58

Identifiants

  • HAL Id : inria-00099187, version 1

Collections

Citation

Jürgen Stuber. Deriving Theory Superposition Calculi from Convergent Term Rewriting Systems. Leo Bachmair. International Conference on Rewriting Techniques & Applications - RTA'2000, 2000, Norwich, UK, Springer-Verlarg, 1833, pp.229-245, 2000, Lecture Notes in Computer Science. 〈inria-00099187〉

Partager

Métriques

Consultations de la notice

125