Parametrized conditional log-specifications: proof theory and correctness

Conditional LOG-specifications extend standard conditional specifications in that the booleans are considered to be built-in. Formally, there is an initial constraint on booleans in every specification. It is shown that this allows to handle situations that could not be dealt within the standard approach. Moreover, it is shown that the usual techniques and results, including proof-theoretical characterizations, for usual parameterized specifications translate without problems to LOG-specifications, though the proofs are often quite different. To end, it must be said that in a previous paper it was proved that contextual rewriting provides a complete proof method for conditional LOG-specifications assuring the applicability of the approach