Narrowing, Abstraction and Constraints for Proving Properties of Reduction Relations

Isabelle Gnaedig 1, 2 Hélène Kirchner 1, 3
2 CARTE - Theoretical adverse computations, and safety
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
3 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We describe in this paper an inductive proof method for properties of reduction relations. The reduction trees are simulated with proof trees generated by narrowing and an abstraction mechanism. While narrowing simulates reduction, abstraction relies on the induction principle to replace subterms by variables representing specific reduced forms that trivially satisfy the property to be proved. The induction ordering is not given a priori, but defined with ordering constraints, incrementally set during the proof. Abstraction constraints are used to control the narrowing mechanism, well-known to easily diverge. The proof method is briefly illustrated on various examples of properties.
Type de document :
Communication dans un congrès
Hubert Comon and Claude Kirchner and Hélène Kirchner. Rewriting, Computation and Proof - Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday, Jun 2007, Paris, France. Springer, 4600, pp.44-67, 2007, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00182434
Contributeur : Isabelle Gnaedig <>
Soumis le : jeudi 25 octobre 2007 - 23:30:20
Dernière modification le : jeudi 11 janvier 2018 - 06:21:25

Identifiants

  • HAL Id : inria-00182434, version 1

Collections

Citation

Isabelle Gnaedig, Hélène Kirchner. Narrowing, Abstraction and Constraints for Proving Properties of Reduction Relations. Hubert Comon and Claude Kirchner and Hélène Kirchner. Rewriting, Computation and Proof - Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday, Jun 2007, Paris, France. Springer, 4600, pp.44-67, 2007, Lecture Notes in Computer Science. 〈inria-00182434〉

Partager

Métriques

Consultations de la notice

301