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 ) 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
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.