Glossary

A recursive definition of first-order unsorted terms.

• A variable is a term,
• a constant is a term, and
• an n-ary function symbol applied to n terms is a term.

An n-ary predicate symbol applied to n terms is an atomic formula.

A clause is a formula consisting of a disjunction of literals. All variables in a clause are assumed to be universally quantified.

An interpretation of a first-order language consists of

• of a set of objects called the domain,
• an n-ary function over the domain into the domain for each n-ary function symbol in the language,
• an n-ary relation over the domain for each n-ary predicate symbol in the language.

Types of Clause

A unit clause has exactly one literal.

A positive clause has no negative literals. A negative clause has no positive literals. Note that the empty clause is both positive and negative. A mixed clause has at least one literal of each sign.

A Horn clause has at most one positive literal. A Horn set is a set of Horn clauses.

A definite clause has exactly one positive literal.

Logic Transformations

A formula is in negation normal form if the only logic connectives are negation, conjunction, disjunction, quantification (universal or existential), and if all negation operations are applied directly to atomic formulas.

This definition applies to quantifier-free formulas.

A formula is in conjunctive normal form if (1) the only logic connectives are negation, conjunction, and disjunction, (2) no negation is applied to a conjunction or a disjunction, and (3) no disjunction is applied to a conjunction.

Alternate definition: A formula is in CNF if it is a clause or a conjunction of clauses.

Skolemization is the process of replacing existentially quantified variables in a formula with new constants (called Skolem constants) or functions (called Skolem functions). If an existential quantifier is in the scope of some universal quantifiers, the new symbol is a function of the corresponding universally quantified variables. The result of Skolemization is not, strictly speaking, equivalent to the original formula, because new symbols may have been introduced, but the result is inconsistent iff the the original formula is inconsistent.

Clausification is the process of translating a formula into a conjunction of clauses. A standard way is NNF conversion, Skolemization, moving universal quantifiers to the top (renaming bound variables if necessary), CNF conversion, and finally removing universal quantifiers. The variables in each resulting clause are implicitly universally quantified.

Each step produces an equivalent formula, except for Skolemization, which produces an equiconsistent formula, so the result of Clausification is inconsistent iff the original formula is inconsistent.

The universal closure of a formula is constructed by universally quantifying, at the top of the formula, all free variables in the formula.

Term Ordering Terminology

A literal is maximal in a clause, with respect to some term ordering, if no literal in the clause is greater. The terms orderings used by Prover9 (LPO, KBO, RPO) are, in general, only partial, so clauses do not necessarily have maximum literals.

Inference and Simplification Rules

The inference rule binary resolution takes two clauses containing unifiable literals of opposite sign and produces a clause consisting of the remaining literals to which the most general unifying substitution has been applied. The rule can be viewed as a generalization of modus ponens.

Restrictions on Binary Resolution.

• Positive resolution: one of the parents is is a positive clause.
• Negative resolution: one of the parents is is a negative clause.
• Unit resolution: one of the parents is is a unit clause.

The inference rule factoring takes one clause containing two or more literals (of the same sign) that all unify. The most general unifying substitution is applied to the parent, and the unified literals become identical and are merged into one.

Factoring in Prover9 is binary, operating on two literals at a time.

The hyperresolution inference rule takes a non-positive clause (called the nucleus) and simultaneously resolves each of its negative literals with positive clauses (called the satellites), producing a positive clause. Hyperresolution can be viewed as a sequence of positive binary resolution steps ending with a positive clause.

Negative hyperresolution is similar to hyperresolution but with the signs reversed.

The UR-resolution (unit-resulting resolution) inference rule takes a nonunit clause (called the nucleus) and resolves all but one of its literals with unit clauses (called the satellites), producing a unit clause.

Positive UR-resolution is UR-resolution with the constraint that the result must be a positive unit clause.

Negative UR-resolution is UR-resolution with the constraint that the result must be a negative unit clause.

A paramodulation inference consists of two parents and a child. The parent containing the equality used for the replacement is the from parent or the from clause, the equality is the from literal, and the side of the equality that unifies with the term being replaced is the from term.

The replaced term is the into term, the literal containing the replaced term is the into literal, and the parent containing the replaced term is the into parent or into clause.

Demodulation is the process of using a set of oriented equations (demodulators) to rewrite (simplify, canonicalize) terms. If the demodulators have good properties, demodulation terminates.

Forward demodulation (or just demodulation) is the process of using a set of demodulators to rewrite newly generated clauses.

Back demodulation is the process of using a new demodulator to simplify previously stored clauses.

Unit deletion is analogous to demodulation. The difference is that unit clauses, rather than equations, are used for simplification.

Unit deletion is the process of using unit clauses to remove literals from newly generated clauses.

Back unit deletion is the process of using a new unit clause to remove literals from previously stored clauses.

Clause C subsumes clause D if the variables of C can be instantiated in such a way that it becomes a subclause of D. If C subsumes D, then D can be discarded, because it is weaker than or equivalent to C. (There are some proof procedures that require retention of subsumed clauses.)

Forward subsumption (or just subsumption) is the process of deleting a newly derived clause if it is subsumed by some previously stored clause.

Back subsumption is the process of deleting all previously stored clauses that are subsumed by a newly derived clause.

Prover9 Terminology

A goal is the conclusion of a conjecture, stated in positive form. Each goals is transformed to clauses by constructing its universal closure, negation, then clausification.

If there is more than one goal, Prover9 may impose restrictions on the structure of the goals.

Hints are clauses that are intended to guide Prover9 toward proofs. Hints are not part of the problem specification; that is, they are not used for making inferences. They are used only as a component of the weighting function for selecting given clauses.

In Prover9 terminology, a negative clause in a Horn set is called a denial, because such clauses usually come from the negation of a conclusion. (The term does not apply to non-Horn sets, because a proof of a non-Horn set may require more than one negative clause.)

FOF (First-Order Formula) reduction is a method of attempting to simplify a problem by reducing it to an equivalent set of independent subproblems. A trivial example is to reduce the conjecture A <-> B to the pair of problems A -> B and B -> A.

A lex-dependent demodulator is one that cannot be oriented by the primary term ordering (LPO or KBO). An example is commutativity of a binary operation. During demodulation, a lex-dependent demodulator is applied only if it produces a term that is smaller in the primary term ordering.