Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/inria-00182434
Contributor : Isabelle Gnaedig <>
Submitted on : Thursday, October 25, 2007 - 11:30:20 PM
Last modification on : Tuesday, December 18, 2018 - 4:48:02 PM

Identifiers

  • HAL Id : inria-00182434, version 1

Collections

Citation

Isabelle Gnaedig, Hélène Kirchner. Narrowing, Abstraction and Constraints for Proving Properties of Reduction Relations. Rewriting, Computation and Proof - Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday, Jun 2007, Paris, France. pp.44-67. ⟨inria-00182434⟩

Share

Metrics

Record views

377