Paramodulation and Theorem-Proving in First-Order Theories with Equality

Abstract

A term is an individual constant or variable or an n-adic function letter followed by n terms. An atomic formula is an n-adic predicate letter followed by n terms. A literal is an atomic formula or the negation thereof. A clause is a set of literals and is thought of as representing the universally-quantified disjunction of its members. It will sometimes be notationally convenient¹ to distinguish between the empty clause □, viewed as a clause, and ‘other’ empty sets such as the empty set of clauses, even though all these empty sets are the same set-theoretic object ø. A ground clause (term, literal) is one with no variables. A clause C’ (literal, term) is an instance of another clause C (literal, term) if there is a uniform replacement of the variables in C by terms that transform C into C’.