The distinction between clauses and formulas is a frequent source of confusion for Prover9 (and Otter) users. When writing logical specifications for Prover9, we urge users to be careful, because clauses go in one kind of list, and formulas go into another. Here are the important points.
f( argument_1, ..., argument_n )Whitespace (spaces, tabs, newline, etc.) is accepted anywhere except within symbols.
Prover9 will accept any term, clause, or formula written prefix standard form. However, clauses, 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 clauses and formulas under the assumption of the built-in parsing properties. The general mechanism is described below in the section Infix, Prefix, and Postfix Declarations.
Prover9 recognizes several kinds of symbol.
Objects (terms, clauses, and formulas) are constructed from symbols, parentheses, and commas.
Prover9 is much more strict about overloading symbols than Otter is.
As a special case, Prolog-style list notation can be used to write terms that represent lists.
Term | Internal Representation | 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 |
clauses(sos). p| -q|r. a=b|c!=d. f(x)!=f(y)|x=y. end_of_list.
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)) |
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)).
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.
op( precedence, type, symbols(s) ). % declare parse type and precedence
The following table shows an example of each type of parsing property (and ignores precedence).
Type | Example | Standard Prefix | Comment |
---|---|---|---|
infix | a*(b*c) | *(a,*(b,c)) | |
infix_left | a*b*c | *(*(a,b),c) | |
infix_right | a*b*c | *(a,*(b,c)) | |
prefix | - -p | -(-(p)) | space required in - -p |
prefix_paren | -(-p) | -(-(p)) | |
postfix | a' ' | '('(a)) | space required in a' ' |
postfix_paren | (a')' | '('(a)) | |
clear | *(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 formulasThen the object 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.
The built-in parsing declarations can be overridden with ordinary "op" comands.
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.
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 "clear". The following example clears
the parse types for two symbols.
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.
No such rule is needed for variables in quantified formulas,
because all variables are explicitly quantified.
Changing prolog_style_variables after some clauses
have already been read file is allowed, but strongly
discouraged. In such situations, Prover9 can print a clause
P(A,A) in which the first A is a constant and
the second is a variable. Prover9 will (happily and correctly)
make deductions with clauses like that, but the user will go crazy.
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
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(400, prefix, - ). % logical negation in formulas or clauses, arithmetic minus in terms
op(300, postfix, ' ).
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)).
op(1, clear, [*,+]). % the precedence is irrelevant for type "clear"
op(400,infix_left,*). % assume left association for following clauses
clauses(sos).
P(a * b * c).
end_of_list.
op(400,infix_right,*). % assume right association for following clauses
clauses(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.
clauses(sos).
1 P((a * b) * c). [input].
2 Q(d * (e * f)). [input].
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.
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 '_'.