| Prover9 Manual |
| Version 2009-02A |
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.
When writing formulas for Prover9, many of the parentheses can be omitted; see the page Clauses and Formulas tor the parsing rules.
- An atomic formula is a formula,
- if F and G are formulas, then the following are formulas.
- (-F)
- (F | G)
- (F & G)
- (F -> G)
- (F <-> G)
- if F is a formula and x is a variable, then the following are formulas.
- (all x F)
- (exists x F)
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'.
A literal is either an atomic formula or the negation of 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 ofGiven 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.
- 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.
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.
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.
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.
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).
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.
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.
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 (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.
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.
Superposition is a restricted form of paramodulation in which substitution is not allowed into the lighter side of an equation.
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 (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 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.
Unit Conflict is an inference rule that derives a contradiction from unit clauses, for example, from P(a,b) and -P(x,b).
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.
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.
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.
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.
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.
For example, p(x) | -p(f(x)) has depth 2.
- depth of variable, constant, or propositional atom: 0;
- depth of term or atom with arguments: one more than the maximum argument depth;
- depth of literal: depth of its atom (negation signs don't count);
- depth of clause: maximum of depths of literals;
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.
An equational definition for an n-ary function (say f with n=3) is an equation (using Prover9 syntax)f(x,y,z) = tfor some term t that does not contain the symbol f and that does not contain free variables other than x, y, and z.