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 objects like a+b; that is, +(a,b), can be written without any whitespace around the +.

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.
The symbol | is used as a delimiter in the Prolog-style list notation as well as disjunction in clauses and formulas.

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

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.

Prolog-style list notation can be used to write terms that represent lists.

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 "lex" 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 symbol is |, and the negation 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, clear }.
symbol(s) is either a symbol or a list of symbols. Each multi-character special symbol must be enclosed in double quotes.

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))`
`infix_left`	`abc`	`((a,b),c)`
`infix_right`	`abc`	`(a,(b,c))`
`prefix`	`--p`	`-(-(p))`
`prefix_paren`	`-(-p)`	`-(-(p))`
`postfix`	`a''`	`'('(a))`
`postfix_paren`	`(a')'`	`'('(a))`
`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 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.

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,      "'" ).

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 state of the flag prolog_style_variables at the end of the input determines the rule that is used. 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.