TABLEAUX '98
Bernhard Beckert and Dov Gabbay
The methodology of fibring is a successful framework for combining
logical systems based on combining their semantics. In this paper, we
extend the fibring approach to calculi for logical systems: we describe
how to uniformly construct a sound and complete tableau calculus for the
combined logic from calculi for the component logics.
We consider semantic tableau calculi that satisfy certain conditions and
are therefore known to be "well-behaved" - such that fibring is
possible. The identification and formulation of conditions that are
neither too weak nor too strong is a main contribution of this paper.
As an example, we fibre tableau calculi for first order predicate logic
and for the modal logic K.