Paramodulation-based theorem proving (Q2751359)

The aim of this chapter is to review the fundamental techniques in paramodulation-based theorem proving and presenting them in a uniform framework. It starts with easier subcases and progressively the different extensions are included. Since the objective is to obtain a concise overview of the current state of the art, some of the historical developments that are not essential for the current results are omitted.NEWLINENEWLINENEWLINEIn the first section, the main concepts are introduced in an informal way, with emphasis on their intuitive background. This is done to facilitate the reading of subsequent sections, where all these notions are formally defined and explained in detail, and some of the main results are proved.NEWLINENEWLINEFor the entire collection see [Zbl 0964.00020].