Prover9 Manual Version 2009-02A

Glossary

Under construction. (Send suggestions of terms to include.)

Terms, Clauses, Formulas, Interpretations

These definitions apply to first-order unsorted logic. See a book on first-order logic for more formal definitions of these concepts.
Term
A recursive definition of first-order unsorted terms.

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

Formula
When writing formulas for Prover9, many of the parentheses can be omitted; see the page Clauses and Formulas tor the parsing rules.

Free Variables
A free variable is a variable not bound by any quantifier. A closed formula has no free variables. An open formula has at least one free variable.

Prover9's default rule for distinguishing free variables from constants is that free varaibles start with (lower case) 'u' through 'z'.


Literal
A literal is either an atomic formula or the negation of an atomic formula.

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

Interpretation
An interpretation of a first-order language consists of
Given an interpretation, each term in the language evaluates to a member of the domain, and each clause or closed formula in the language evaluates to TRUE or to FALSE.

Types of Clause


Unit Clause
A unit clause has exactly one literal.

Positive Clause, Negative Clause, Mixed Clause
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.

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

Definite Clause
A definite clause has exactly one positive literal.


Logic Transformations


Negation Normal Form (NNF)
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.

Conjunctive Normal Form (CNF)
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
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
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.


Universal Closure
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


Knuth-Bendix Ordering (KBO)

Lexicographic Path Ordering (LPO)

Recursive Path Ordering (RPO)

Maximal Literal
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 greatest literals.


Inference and Simplification Rules


Completeness
An inference system is complete if it is capable (given enough time and memory) of proving any theorem (in the language of the inference system).

Binary Resolution
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.


Ordered Inference, Literal Selection
Ordered Inference is a restriction of resolution or paramdulation based on literal ordering. In some cases, inferences can be restricted to maximal literals.

Literal selection is a restriction of resolution or paramdulation. In each clause, some subset of the negative literals are marked as selected (the selection may be arbitrary), and in some cases inferences can be restricted to selected literals.


Factoring
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.


Hyperresolution
The hyperresolution inference rule (also called positive hyperresolution) 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.


UR-Resolution
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.


"From" and "Into" in Paramodulation
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.

Superposition is a restricted form of paramodulation in which substitution is not allowed into the lighter side of an equation.


Positive Paramodulation
Positive paramodulation is a restriction of paramodulation in which the "from" clause is positive, and if the "into" literal is positive, the "into" clause is also positive.

Demodulation, Back Demodulation
Demodulation (also called rewriting) 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, Back Unit Deletion
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.


Subsumption, Forward and Backward Subsumption
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.


Unit Conflict
Unit Conflict is an inference rule that derives a contradiction from unit clauses, for example, from P(a,b) and -P(x,b).


Prover9 Terminology


Given Clause
The given clause loop drives the inference process int Prover9. At each iteration of the loop, a given clause is selected from the sos list, moved the the usable list, and then inferences are made using the given clause and other clauses in the usable list.

Sos List, Assumptions List, Usable List
During the search, the usable list is the list of clauses that are available for making inferences with the given clause, and the sos list is the list of clauses that are waiting to be selected as given clauses. Clauses in the sos list are not available for making primary inferences, but they can be used to simplify inferred clauses by demodulation and unit deletion.

The assumptions list is identical to the sos list; that is, "assumptions" is a synonym for "sos".

Prover9 also accepts non-clausal formulas in lists named usable or sos. Such formulas are transformed to clauses which are placed in the clause list of the same name.

The name "sos" is used because it can be employed to achieve the set-of-support strategy, which requires that all lines of reasoning start with a subset of the input clauses called the set of support. The clauses or formulas in the initial set of support are placed the sos list, and the rest of the clauses or formulas are placed in the usable list.


Goal, Goals List
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.


Hint, Hints List
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.

Initial Clause
A clause is an initial clause if it exists at the time when the first given clause is selected. Initial clauses are not necessarily input clauses, because they may be created during preprocessing, for example, by rewriting or clausification.

Denial
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 Reduction
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.

Lex-Dependent Demodulator
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.

Depth of Term, Atom, Literal, Clause
For example, p(x) | -p(f(x)) has depth 2.

Relational Definition
A relational definition for an n-ary relation (say P with n=3) is a closed formula of the form (using Prover9 syntax)
all x all y all z (P(x,y,z) <-> f)
for some formula f that does not contain the symbol P.

Equational Definition
An equational definition for an n-ary function (say f with n=3) is an equation (using Prover9 syntax)
f(x,y,z) = t
for some term t that does not contain the symbol f and that does not contain free variables other than x, y, and z.

Next Section:
References