DL extends the structural language of ordinary sequents in a natural way by introducing abstract operations on structures.
Antecedent (succedent) parts of a sequent s can be displayed as the entire antecedent (succedent) of a sequent s′ structurally equivalent to s.
The introduction rules for the logical operations exploit a certain duality between the antecedent and the succedent position of the sequent arrow. In particular, the introduction rules for the normal modal and tense logical operators rely on the ideas of residuation and Galois connection.
There may be more than just one family of structural operations.
KeywordsNormal Form Logical Operation Structure Connective Structural Rule Residuated Pair
Unable to display preview. Download preview PDF.