ISSN:
1432-0525
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Notes:
Abstract In this paper we provide foundations to contextual rewriting. We present the class of LOG-specifications, which may be seen, essentially, as a variety of conditional specifications, which may be seen, essentially, as a of LOG-specifications are LOG-algebras, i.e. algebras satisfying that their boolean part coincides with the boolean algebra of two elements. With respect to this semantics, a proof-system called L is presented characterizing logical consequence proof-theoretically. Then, we show that, under adequate assumptions of confluence and finite termination, contextual rewriting is a complete method for this kind of specifications.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1007/BF01178578
Permalink