Narrowing, Abstraction and Constraints for Proving Properties of Reduction Relations - Archive ouverte HAL Access content directly
Conference Papers Year : 2007

Narrowing, Abstraction and Constraints for Proving Properties of Reduction Relations

(1, 2) , (1, 3)
1
2
3

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.
Not file

Dates and versions

inria-00182434 , version 1 (25-10-2007)

Identifiers

  • HAL Id : inria-00182434 , version 1

Cite

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⟩
123 View
0 Download

Share

Gmail Facebook Twitter LinkedIn More