Generalized interpolation in CASL

In this paper we consider the partial many-sorted first-order logic and its extension to the subsorted partial many-sorted first-order logic that underly the Casl specification formalism. First we present counterexamples showing that the generalization of the Craig Interpolation Property does not hold for these logics in general (i.e., with respect to arbitrary signature morphisms). Then we formulate conditions under which the generalization of the Craig Interpolation Property holds for the first logic.

• Type: Journal
• Year: 2000
• Where: IPL
• Authors: Tomasz Borzyszkowski
• Keywords: Casl Specification Formalism, Craig Interpolation Property, IPL 2000, Many-sorted First-order Logic