TU Vienna logic.at Theory and Logic Group (E185-2)

## LKDe

LKDe is an exstension of LK. Besides the rules of LK, LKDe contains definition- and equality rules.

• The definition rules directly correspond to the extension principle (see [2]) in predicate logic. It simply consists in introducing new predicate- and function symbols as abbreviations for formulas and terms. Mathematically this corresponds to the introduction of new concepts in theories. Let be a first-order formula with the free variables (denoted by ) and be a unique -ary predicate symbol corresponding to the formula . Then the rules are:

for arbitrary sequences of terms . There are also definition introduction rules for new function symbols which are of similar type.

• The equality rules are:

for inference on the left and

on the right, where denotes a set of positions of subterms where replacement of by has to be performed. We call (or ) the active equation of the rules. Note that, on atomic sequents, the rules coincide with paramodulation -- under previous application of the most general unifier.