Prover9 Manual

Version 2009-02A

Clauses and Formulas

The Glossary Page contains definitions of term, atomic formula, literal, clause, and formula from a logical point of view. This page contains descriptions of how those kinds of things are parsed and printed, and we refer to them collectively as objects.

In Otter and in earlier versions of Prover9, "clauses" and "formulas" were distinct types of object, and "formulas" could not have free variables. Now, clauses are a subset of formulas.

Here are the important points about clauses and formulas.

Clauses are a subset of formulas. All input formulas, including clauses, appear in a list headed by formulas(list_name).
There is a rule for distinguishing variables from constants, because clauses and other formulas can have free variables (variables not bound by quantifiers). The default rule is that variables start with (lower case) u through z. For example, in the formula P(a,x), the term a is a constant, and x is a variable. (See also the flag prolog_style_variables.)
Free variables in clauses and formulas are assumed to be universally quantified at the outermost level.
Prover9's inference rules operate on clauses. If non-clausal formulas are input, Prover9 immediately translates them clauses by NNF, Skolemization, and CNF conversions.

Parsing and Printing Objects

The prefix standard form of an object with an n-ary symbol, say f, at the root is

f( argument_1, ..., argument_n )

Whitespace (spaces, tabs, newline, etc.) is accepted anywhere except within symbols.

Prover9 will accept any term or formula written prefix standard form. However formulas and many terms can be written in more convenient ways, for example, "a=b | a!=c'" instead of "|(=(a,b),-(=(a,'(c))))".

Prover9 uses a general mechanism in which binary and unary symbols can have special parsing properties such as "infix", "infix-right-associated", "postfix". In addition, each of those symbols has a precedence so that many parentheses can be omitted. (The mechanism is similar to those used by most Prolog systems.)

Many symbols have built-in parsing properties (see the table below), and the user can declare parsing properties for other symbols with the "op" command.

Clauses and formulas make extensive use of the built-in parsing properties for the equality relation and the logic connectives. Instead of first presenting the general mechanism, we will present the syntax for formulas under the assumption of the built-in parsing properties. The general mechanism is described below in the section Infix, Prefix, and Postfix Declarations.

Symbols

Symbols include variables, constants, function symbols, predicate symbols, logic connectives. Symbols do not include parentheses or commas.

Prover9 recognizes several kinds of symbol.

An ordinary symbol is a (maximal) string made from the characters a-z, A-Z, 0-9, $, and _.
A special symbol is a (maximal) string made from the special characters: {+-*/\^<>=`~?@&|!#';}.
A quoted symbol is any string enclosed in double quotes.
The empty list symbol is []. This is a special case.

The reason for separating ordinary and special symbols is so that strings like a+b; that is, +(a,b), can be written without any whitespace around the +.

A symbol cannot have both ordinary and special characters, for example R+ (unless it is a quoted symbol).

Objects (terms or formulas) are constructed from symbols, parentheses, and commas.

Overloaded Symbols

In most cases, symbol overloading is not allowed. For example a symbol cannot be both a function symbol and a predicate symbol, or both a constant and a binary function symbol. There are a few exceptions.

The logic connectives can also be used as function or predicate symbols of the same arity. For example, - is typically used as unary arithmetic minus well as for logical negation.

Prover9 is much more strict about overloading symbols than Otter is.

Symbols With Meaning

Several symbols have built-in meaning. These are the equality symbols (=, !=) and logic connectives (-, |, &, ->, <-, <->, all, exists). These symbols can be changed as described in the section Redeclaring Built-in Symbols. (Parentheses, comma, period, and the list construction symbols cannot be redeclared.)

Terms

Any term can be written in prefix standard form, for example, f(g(x),y) and *('(x),y). If symbols in the term have parsing/printing properties (either built-in) or declared with the op command), the term can be written in infix/prefix/postfix form with assumed precedence, for example, x'*y, which represents *('(x),y) under the built-in parsing/printing properties.

A list notation similar to Prolog's can be used to write terms that represent lists. Note that the "cons" operator is ":", instead of "|" as in Prolog.

Term	Standard Prefix Form	What it Is
`[]`	`$nil`	the empty list
`[a,b,c]`	`$cons(a,$cons(b,$cons(c,$nil)))`	list of three objects
`[a:b]`	`$cons(a,b)`	first, rest
`[a,b:c]`	`$cons(a,$cons(b,c))`	first, second, rest

Lists are frequently used in Prover9 commands such as the function_order command, and they are sometimes also used in clauses and formulas.

Atomic Formulas

Equality is a built-in special case. The binary predicate symbol = is usually written as an infix relation. The binary symbol != is an abbreviation for "not equal"; that is, the formula a!=b stands for -(a=b), or more precisely, -(=(a,b)). From the semantics point of view, the binary predicate symbol = is the one and only equality symbol for the inference rules that use equality.

Clauses

The disjunction (OR) symbol is |, and the negation (NOT) symbol is -. The disjunction symbol has higher precedence than the equality symbol, so equations in clauses do not need parentheses. Every clause ends with a period. Examples of clauses follow (Prover9 adds some extra space when printing clauses).

formulas(sos).
    p|-q|r.
    a=b|c!=d.
    f(x)!=f(y)|x=y.
end_of_list.

Formulas

Meaning	Connective	Example
negation	`-`	`(-p)`
disjunction	`\|`	`(p \| q \| r)`
conjunction	`&`	`(p & q & r)`
implication	`->`	`(p -> q)`
backward implication	`<-`	`(p <- q)`
equivalence	`<->`	`(p <-> q)`
universal quantification	`all`	`(all x all y p(x,y))`
existential quantification	`exists`	`(exists x exists y p(x,y))`

When writing formulas, the built-in parsing declarations allow many parentheses to be omitted. For example, the following two formulas are really the same formula.

formulas(sos).
 all x  all y (p <->   -q  |  r &  -s)     .
(all x (all y (p <-> ((-q) | (r & (-s)))))).
end_of_list.

For Prover9 formulas, each quantified variable must have its own quantifier; Otter allows quantifiers to be omitted in a sequence of quantified variables with the same quantifier. For example, Otter allows (all x y z p(x,y,z)), and Prover9 requires (all x all y all z p(x,y,z)).

Infix, Prefix, and Postfix Declarations

Several symbols are understood by Prover9 as having special parsing properties that determine how terms involving those symbols can be arranged. In addition, the user can declare additional symbols to have special parsing properties.

Parsing Declarations

The "op" command is used to declare parse types and precedences.

op( precedence, type, symbols(s) ).  % declare parse type and precedence

1 ≤ precedence ≤ 998.
type is one of { infix, infix_left, infix_right, prefix, prefix_paren, postfix, postfix_paren, ordinary }.
symbol(s) is either a symbol or a list of symbols. Each multi-character special symbol must be enclosed in double quotes.

Prover9 does not allow different symbol types with the same precedence, for example,
op(325, postfix, ').
op(325, prefix, ~).
This restriction prevents ambiguous strings such as ~x'.

The following table shows an example of each type of parsing property (and ignores precedence).

Type	Example	Standard Prefix	Comment
`infix`	`a(bc)`	`(a,(b,c))`	like Prolog's `xfx`
`infix_left`	`abc`	`((a,b),c)`	like Prolog's `yfx`
`infix_right`	`abc`	`(a,(b,c))`	like Prolog's `xfy`
`prefix`	`--p`	`-(-(p))`	like Prolog's `fy`
`prefix_paren`	`-(-p)`	`-(-(p))`	like Prolog's `fx`
`postfix`	`a''`	`'('(a))`	like Prolog's `yf`
`postfix_paren`	`(a')'`	`'('(a))`	like Prolog's `xf`
`ordinary`	`*(a,b)`	`*(a,b)`	takes away parsing properties

Higher precedence means closer to the root of the object, and lower precedence means the the symbol binds more closely. For example, assume that the following declarations are in effect.

op(790, infix_right,  "|" ).  % disjunction in formulas or clauses
op(780, infix_right,  "&" ).  % conjunction in formulas

Then the string a & b | c is an abbreviation for (a & b) | c.

The built-in parsing declarations are shown in the following box. The ones with comments have built-in meanings; the others are for general use as function or predicate symbols.

op(810, infix_right,  "#" ).  % for attaching attributes to clauses
	    
op(800, infix,      "<->" ).  % equivalence in formulas
op(800, infix,       "->" ).  % implication in formulas
op(800, infix,       "<-" ).  % backward implication in formulas
op(790, infix_right,  "|" ).  % disjunction in formulas or clauses
op(780, infix_right,  "&" ).  % conjunction in formulas

% Quantifiers (a special case) have precedence 750.
	    
op(700, infix,        "=" ).  % equal in atomic formulas
op(700, infix,       "!=" ).  % not equal in atomic formulas
op(700, infix,       "==" ).  
op(700, infix,        "<" ).
op(700, infix,       "<=" ).
op(700, infix,        ">" ).
op(700, infix,       ">=" ).
	    
op(500, infix,        "+" ).
op(500, infix,        "*" ).
op(500, infix,        "@" ).
op(500, infix,        "/" ).
op(500, infix,        "\" ).
op(500, infix,        "^" ).
op(500, infix,        "v" ).

op(350, prefix,       "-" ).  % logical negation in formulas or clauses
op(300, postfix,      "'" ).

The built-in parsing declarations can be overridden with ordinary "op" commands. Be careful, however, when overriding parsing declarations for symbols with built-in meanings. For example, say you wish to use "#" as an infix function symbol and give the following the declaration.

op(500, infix, "#").

Then clauses with attributes might have be written with more parentheses, for example, as

(p(a) | q(a)) # (label(a) # label(b)).

If you wish to use one of the symbols with built-in parsing declarations as an ordinary prefix symbol, you can undo the declaration by giving an "op" command with type "ordinary". The following example clears the parse types for two symbols.

op(ordinary, ["*","+"]).   % there is no precedence argument for type "ordinary"

Finally, the following example shows that parsing declarations can be changed anywhere in the input, with immediate effect. This can be useful for example, if lists of clauses come from different sources.

op(400,infix_left,"*").  % assume left association for following clauses

formulas(sos).
  P(a * b * c).
end_of_list.

op(400,infix_right,"*"). % assume right association for following clauses

formulas(sos).
  Q(d * e * f).
end_of_list.

op(400,infix,"*").  % from here on, include all parentheses (input and output)

An excerpt from the output of the preceding example shows how the clauses are printed after the last "op" command.

formulas(sos).
P((a * b) * c).  [assumption].
Q(d * (e * f)).  [assumption].
end_of_list.

Prolog-Style Variables

set(prolog_style_variables).
clear(prolog_style_variables).    % default clear

A rule is needed for distinguishing variables from constants in clauses and formulas with free variables. If this flag is clear, variables in clauses start with (lower case) 'u' through 'z'. If this flag is set, variables in clauses start with (upper case) 'A' through 'Z' or '_'.
Prover9 decides whether symbols are constants or variables after it has read all of its input, so the state of the flag prolog_style_variables at the end of the input determines the rule that is used for all formulas. For example, in the following input,
formulas(sos).
  p(x,A).
end_of_list.

set(prolog_style_variables).

formulas(sos).
  q(y,B).
end_of_list.
the term x is a constant, and A is a variable.

Redeclaring Built-in Symbols

NOTE: Keep in mind the difference between semantic properties of symbols (e.g., logic connectives) and parsing/printing properties of symbols (e.g., infix with high precedence). Those two kinds of property are independent (by default, many symbols have both).

Most of the symbols with built-in meaning can be changed to other symbols. The symbols that can be changed are shown in the following table.

Operation	Default Symbol
true	`$T`
false	`$F`
negation	`-`
disjunction	`\|`
conjunction	`&`
implication	`->`
backward_implication	`<-`
equivalence	`<->`
universal_quantification	`all`
existential_quantification	`exists`
equality	`=`
negated_equality	`!=`
attribute	`#`

To change the symbol associated with an operation, one uses the following command.

redeclare( operation, symbol ).  % associate a different symbol with an operation

For example, the following command says that "AND" will be used for conjunction.

redeclare(conjunction, AND).  % change the conjunction symbol to AND.

As with the "op" command, if the new symbol is a multicharacter special symbol, it must be enclosed in double quotes, as in the following example.

redeclare(conjunction, "&&").  % change the conjunction symbol to &&.

When in doubt, quote the symbol, because unnecessary quotes are ignored in the "redeclare" and "op" commands.

Parsing/Printing Properties and Redeclarations

Many of the default symbols for the built-in operations have default printing/parsing properties, for example, the default properties for default conjunction symbol are

op(780, infix_right,  "&" ).  % conjunction in formulas

When a redeclaration for such an operation occurs, the parsing/printing properties are copied from the old symbol to the new symbol. For example, when conjunction is changed to AND, the following is automatically applied.

op(780, infix_right,  AND ).

If the user wishes some other printing/parsing properties for the new symbol, the appropriate "op" command can be placed after the "redeclare" command.

Redeclaration Example

The following example shows redeclarations of many of the operations.

prover9 -f redeclare.in > redeclare.out

Location of Redeclare Commands

Most of the operations can be redeclared repeatedly throughout the input. The declarations in effect when a formula is read will be used, ane the ones in effect at the end of the input will be used for all subsequent output.

An exception: If the operations "equality" or "negated_equality" are redeclared, it must be done before any formulas containing those symbols are read.

Next Section: Auto Modes