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:
![\begin{displaymath}
\infer[{\rm def}_{P}\colon l]{P(t_1,\ldots,t_k)^+, \Gamma \v...
...\ldots,t_k)^+}
{\Gamma \vdash \Delta,A(t_1,\ldots,t_k)^\star}
\end{displaymath}](method-img42.png)
for arbitrary sequences of terms
. There are also
definition introduction rules for new function symbols which are
of similar type.
- The equality rules are:
![\begin{displaymath}
\infer[=\colon l1]{A[t]^\star_\Sigma, \Gamma, \Pi \vdash
\D...
... \vdash \Delta, t=s^+
&
A[s]^+_\Sigma, \Pi \vdash \Lambda
}
\end{displaymath}](method-img44.png)
for inference on the left and
![\begin{displaymath}
\infer[=\colon r1]{\Gamma, \Pi \vdash \Delta, \Lambda,
A[t]^...
... \vdash \Delta, t=s^+
&
\Pi \vdash \Lambda, A[s]^+_\Sigma
}
\end{displaymath}](method-img45.png)
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.