##
**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.