Linear Paramodulation modulo Equality

摘要: We propose to use E-paramodulation, i.e. linear paramodulation modulo equality, compute with generalized equational programs consisting of a conditional theory and program. Simple examples from deduction systems motivate our approach. formally define the calculus for which is based on inference rules E-paramodulation E-reflection. This proven be sound complete by using fixpoint theory. Finally, we discuss why functional reflexive axioms have used ensure these results.