- Claus-Peter Wirth,
- On Notions of Inductive Validity for First-Order Equational Clauses
- 12th CADE 1994, LNAI 814, pp. 162-176, Springer.
- We define and discuss various conceivable notions of inductive validity for first-order
equational clauses. This is done within the framework of constructor-based positive/negative
conditional equational specifications which permits to treat negation and incomplete function
definitions in an adequate and natural fashion. Moreover, we show that under some reasonable
assumptions all these notions are monotonic w.r.t. consistent extension, in contrast to the case of
inductive validity for initial semantics (of unconditional or positive conditional equations). In
particular from a practical point of view, this monotonicity property is crucial since it allows for an
incremental construction process of complex specifications where consistent extensions of
specifications cannot destroy the validity of (already proved) inductive properties. Finally we show
how various notions of inductive validity in the literature fit in or are related to our classification.
- Full paper
- .2 Mbytes
- .1 Mbytes
The fonts of this version differ from the original,
some originally identical fonts are different in this version,
but the whole file can be searched!
- .2 Mbytes