W3C home > Mailing lists > Public > www-archive@w3.org > September 2002

[www-archive] <none>

From: Sandro Hawke <sandro@w3.org>
Date: Fri, 6 Sep 2002 12:40:51 -0400
Message-Id: <200209061640.g86GepP24255@wadimousa.hawke.org>
To: www-archive@w3.org
EXCERPT FROM:     http://www-unix.mcs.anl.gov/AR/otter/


		     Otter 3.0 Reference Manual and Guide
			      William W. McCune

	Otter  (Organized Techniques for Theorem-proving and Effective
	Research) is a resolution-style	 theorem-proving  program  for
	first-order logic with equality.  Otter includes the inference
	rules binary resolution, hyperresolution,  UR-resolution,  and
	binary	paramodulation.	  Some of its other abilities and fea-
	tures are conversion from  first-order	formulas  to  clauses,
	forward	 and  back  subsumption,  factoring, weighting, answer
	literals, term ordering, forward and back demodulation, evalu-
	able  functions	 and  predicates, and Knuth-Bendix completion.
	Otter is coded in C, is free, and is portable to many  differ-
	ent kinds of computer.

				 January 1994
			   (Revision A, August 1995)

    This work was supported by the Office of Scientific Computing, U.S.
    Department of Energy, under Contract W-31-109-Eng-38.

CHAPTER 4, "SYNTAX"

    4.  Syntax

    Otter recognizes two basic types of statement: clauses and formulas.
    Clauses are simple disjunctions whose variables are implicitly univer-
    sally quantified.  Otter's searches for proofs operate on clauses.
    Formulas are first-order statements without free variables---all vari-
    ables are explicitly quantified.  When formulas are input, Otter imme-
    diately translates them to clauses.

    Function symbols and predicate symbols are sometimes referred to as
    functors when the distinction is not important.


    4.1.  Comments

    Comments can be placed in the input file by using the symbol %.  All
    characters from the first % on a line to the end of the line are
    ignored.  Comments can occur within terms.	Comments are not echoed to
    the output file.


    4.2.  Names for Variables, Constants, Functions, and Predicates

    Three kinds of character string, collectively referred to as names,
    can be used for variables, constants, function symbols, and predicate
    symbols:

      +	 An ordinary name is a string of alphanumerics, $, and _.

      +	 A special name is a string of characters in the set
	 *+-/<>=`~:?@&!;# (and sometimes |).

      +	 A quoted name is any string enclosed in two quotation marks of
	 the same type, either " or '.	We have no trick for including a
	 quotation mark of the same type in a quoted name.

    (The reason for separating ordinary and special names has to do with
    infix, prefix, and postfix operators; see Sec. [ops].)  Although out
    of place here, for completeness we list the meanings of the remaining
    printable characters.

	. (period)  --- terminates input expressions.

	%  --- starts a comment (which ends with the end of the line).

	,()[] (and sometimes |) --- are punctuation and grouping symbols.

    Variables.

    Determining whether a simple term is a constant or a variable depends
    on the context of the term.	 If it occurs in a clause, the symbol
    determines the type: the default rule is that a simple term is a vari-
    able if it starts with u, v, w, x, y, or z.	 If the flag pro-
    log_style_variables is set, a simple term is a variable if and only if
    it starts with an upper-case letter or with _.  (Therefore, variables
    in clauses must be ordinary names.)	 A simple term in a formula is a
    variable if and only if it is bound by a quantifier.


    Reserved and Built-in Names.

    Names that start with $ are reserved for special purposes, including
    evaluable functions and predicates (Sec. [eval]), answer literals and
    terms (Sec. [answer]), and some internal system names.  The name = and
    any name that starts with eq, EQ, or Eq, when used as a binary predi-
    cate symbol, is recognized as an equality predicate by the demodula-
    tion and paramodulation processes.	And some names, when they occur in
    clauses or formulas, are recognized as logic symbols.


    Overloaded Symbols.

    The user can use a name for more than one purpose, for example as a
    constant and as a 5-ary predicate symbol.  When the flag check_arity
    is set (the default), the user is warned about such uses.  Some built-
    in names are also overloaded; for example, | is used both for disjunc-
    tion and as Prolog-style list punctuation, and although - is built in
    as logical negation, it is generally used for both unary and binary
    minus as well.


    4.3.  Terms and Atoms

    Recall that, when interpreted, terms are evaluated as objects in some
    domain, and atoms are evaluated as truth values.  Constants and vari-
    ables are terms.  An n-ary function symbol applied to n terms is also
    a term.  An n-ary predicate symbol applied to n terms is an atom. A
    nullary predicate symbol (also referred to as a propositional vari-
    able) is also an atom.

    The pure way of writing complex terms and atoms is with standard
    application: the function or predicate symbol, opening parenthesis,
    arguments separated by commas, then closing parenthesis, for example,
    f(a,b,c) and =(f(x,e),x).  If all subterms of a term are written with
    standard application, the term is in pure prefix form.  Whitespace
    (spaces, tabs, newlines, and comments) can appear in standard applica-
    tion terms anywhere except between a function or predicate symbol and
    its opening parenthesis.  If the flag display_terms is set, Otter will
    output terms in pure prefix form.


    Infix Equality.	infix form; the most important is =.  In addition, a
    negated equality, -(a=b) can be abbreviated a!=b.


    List Notation.   to write terms that represent lists.  Table 1 gives
    some example terms in list notation and the corresponding pure prefix
    form.

			    Table 1: List Notation

	    []		 $nil
	    [x|y]	 $cons(x,y)
	    [x,y]	 $cons(x,cons(y,nil))
	    [a,b,c,d]	 $cons(a,cons(b,cons(c,cons(d,nil))))
	    [a,b,c|x]	 $cons(a,cons(b,cons(c,x)))


    Of course, lists can contain complex terms, including other lists.


    4.4.  Literals and Clauses

    A literal is either an atom or the negation of an atom.  A clause is a
    disjunction of literals.  The built-in symbols for negation and dis-
    junction are - and |, respectively.	 Although clauses can be written
    in pure prefix form, with - as a unary symbol and | as a binary sym-
    bol, they are rarely written that way.  Instead, they are almost
    always written in infix form, without parentheses.	For example, the
    following is a clause in both forms.


	 Pure prefix:		    |(-(a),|(=(b1,b2),-(=(c1,c2))))
	 Infix (abbreviated):	    -a | b1=b2 | c1!=c2


    Otter accepts both forms.  (Clauses are parsed by the general term-
    parsing mechanism presented in Sec. [ops]).


    4.5.  Formulas

    Table 2. lists the built-in logic symbols for constructing formulas.

			    Table 2: Logic Symbols

	negation			   -
	disjunction			   |
	conjunction			   &
	implication			   ->
	equivalence			   <->
	existential quantification	   exists
	universal quantification	   all



    Formulas in Pure Prefix Form.

    Although the practice is rarely done, formulas can be written in pure
    prefix form.  Quantification is the only tricky part: there is a spe-
    cial variable-arity functor, $Quantified, for quantified formulas.
    For example, all x y exists z (P(x,y,z) | Q(x,z)) is represented by

	$Quantified(all,x,y,exists,z,|(P(x,y,z),Q(x,z))).

    If the flag display_terms is set, the formulas (and everything else)
    will be displayed in pure prefix form.


    Abbreviated Formulas.

    Formulas are usually abbreviated in a natural way.	The associativity
    and precedence rules for abbreviating formulas and the mechanism for
    parsing formulas are presented in Sec. [ops].  Here are some examples.

	standard usage			     Otter syntax (abbreviated)
	all x P(x)			     all x P(x)
	all x y exists z (P(x,y,z) v Q(x,z))
					     all x y exists z (P(x,y,z) | Q(x,z))
	all x (P(x) & Q(x) & R(x) -> S(x))
					     all x (P(x) & Q(x) & R(x) -> S(x))

    Note that if a formula has a string of identical quantifiers, all but
    the first can be dropped.  For example, all x all y all z p(x,y,z) can
    be shortened to all x y z p(x,y,z).	 In expressions involving the
    associative operations & and |, extra parentheses can be dropped.
    Moreover, a default precedence on the logic symbols allows us to drop
    more parentheses: <-> has the same precedence as ->, and the rest in
    decreasing order are ->, |, &, -.  Greater precedence means closer to
    the root of the term (i.e., larger scope).	For example, p | -q & r ->
    -s | t represents (p | (-(q) & r)) -> (-(s) | t), or in pure prefix
    form, ->(|(p,&(-(q),r)),|(-(s),t)).

    When in doubt about how a particular string will be parsed, one can
    simply add additional parentheses and/or test the string by having
    Otter read it and then display it in pure prefix form.  The following
    input file can be used to test the preceding example.

	assign(stats_level, 0).
	set(display_terms).
	formula_list(usable).
	p| -q&r-> -s|t.	      % This formula has minimum whitespace.
	end_of_list.

    In general, whitespace is required around all and exists and to the
    left of -; otherwise, whitespace around the logic symbols can be
    removed.  See Sec. [ops] for the rules.


    4.6.  Infix, Prefix, and Postfix Expressions

    Many Prolog systems (for example Quintus and Sicstus) have a feature
    that allows users to declare that particular function or predicate
    symbols are infix, prefix, or postfix and to specify a precedence and
    associativity so that parentheses can sometimes be dropped.	 Otter has
    a similar feature.	In fact, the clause and formula parsing routines
    use the feature.   Users who use only the predeclared logic operators
    for clauses and formulas and the predeclared infix equality = can skip
    the rest of this section.

    Prolog users who are familiar with the declaration mechanism should
    note the following differences between the Quintus/Sicstus mechanism
    and Otter's.

      +	 The predeclared operators are different.  See Table 3.

      +	 Otter does not treat comma as an operator; in particular, a,b,c
	 cannot be a term, as in a,b,c -> d,e,f.

      +	 Otter treats the quantifiers all and exists as special cases,
	 because they don't seem to fit neatly into the standard Prolog
	 mechanism.

      +	 Otter requires whitespace in some cases where the Prologs do not.

    Functors to be treated in this special way are given a type and a
    precedence.	 Either Otter predeclares the functor's properties, or the
    user gives Otter a command of one of the forms
    op( precedence ,  type ,  functor ).
    op( precedence ,  type ,  list-of-functors ).
    The precedence is an integer i, 0<i<1000, and type is one of the fol-
    lowing: xfx, xfy, yfx (infix), fx, fy (prefix), xf, yf (postfix).  See
    Table 3 for the commands corresponding to the predeclared functors.

			Table 3: Predeclared Functors

	    op(800, xfx, ->).	     op(700, xfx, @<).
	    op(800, xfx, <->).	     op(700, xfx, @>).
	    op(790, xfy, |).	     op(700, xfx, @<=).
	    op(780, xfy,  ).	     op(700, xfx, @>=).

	    op(700, xfx, =).	     op(500, xfy, +).
	    op(700, xfx, !=).	     op(500, xfx, -).

	    op(700, xfx, <).	     op(500, fx, +).
	    op(700, xfx, >).	     op(500, fx, -).
	    op(700, xfx, <=).
	    op(700, xfx, >=).	     op(400, xfy, *).
	    op(700, xfx, ==).	     op(400, xfx, /).
	    op(700, xfx, =/=).	     op(300, xfx, mod).


    Given an expression that looks like it might be associated in a number
    of ways, the relative precedence of the operators determines, in part,
    how it is associated.  A functor with higher precedence is more domi-
    nant (closer to the root of the term), and one with lower precedence
    binds more tightly.	 For example, the functors ->, |, &, and - have
    decreasing precedence; therefore the expression p & - q | r -> s is
    understood as ((p & (-q)) | r) -> s.

    In each of the types, f represents the functor, and x and y, which
    represent the expressions to which the functor applies, specify how
    terms are associated.  Given an expression involving functors of the
    same precedence, the types of the functors determines, in part, the
    association.  See Table 4.

			    Table 4: Functor Types

	    xfx	  infix (binary)    don't associate
	    xfy	  infix (binary)    associate right
	    yfx	  infix (binary)    associate left
	    fx	  prefix (unary)    don't associate
	    fy	  prefix (unary)    associate
	    xf	  postfix (unary)   don't associate
	    yx	  postfix (unary)   associate


    The following are examples of associativity:

      +	 If + has type xfy, then a+b+c+d is understood as a+(b+(c+d)).

      +	 If -> has type xfx, then a->b->c is not well formed.

      +	 If - has type fy, then - - -p is understood as -(-(-(p))).  (The
	 spaces are necessary; otherwise, --- will be parsed as single
	 name.)

      +	 If - has type fx, then - - -p is not well formed.

     Caution: The associativity specifications in the infix functor decla-
    rations say nothing about the logical associativity of the operation,
    e.g., whether (a+b)+c is the same object as as a+(b+c).  The specifi-
    cations are only about parsing ambiguous expressions.  In most cases,
    when an operator is xfy or yfx, it is also logically associative, but
    the logical associativity is handled separately; it is built-in in the
    case of the logic symbols | and & in Otter clauses and formulas, and
    it must be axiomatized in other cases.


    Details of the Functor Declarations.   (This paragraph can be skipped
    by most users.)  The precedence of functors extends to the precedence
    of expressions in the following way.  The precedence of an atomic,
    parenthesized, or standard application expression is 0.  Respective
    examples are p, (x+y), and p(a+b,c,d).  The precedence of a (well-
    formed) nonparenthesized nonatomic expression is the same as the
    precedence of the root functor.  For example, a&b has the precedence
    of &, and a&b|c has the precedence of the greater functor.	In the
    type specifications, x represents an expression of lower precedence
    than the functor, and y represents an expression with precedence less
    than or equal to the functor.  Consider a+b+c, where + has type xfy;
    if association is to the left, then the second occurrence of + does
    not fit the type, because a+b, which corresponds to x, does not have a
    lower precedence than +; if association is to the right, then all is
    well.  If we extend the example, under the declarations op(700, xfx,
    =) and op(500, xfy, +), the expression a+b+c=d+e must be understood as
    (a+ (b+c))= (d+e).


    4.7.  Whitespace in Expressions

    The reason for separating ordinary names from special names (Sec.
    [names]) is so that some whitespace (spaces, tabs, newline, and com-
    ments) can be removed.  We can write a+b+c (instead of having to write
    a + b + c), because "a+b+c" cannot be a name, that is, it must be
    parsed into five names.

    Caution.  There is a deficiency in Otter's parser having to do with
    whitespace between a name and opening parenthesis.	The rule to use
    is:	 Insert some white space if and only if it is not a standard
    application.  For example, the two pieces of white space in (a+
    (b+c))= (d+e) are required, and no white space is allowed after f or g
    in f(x,g(x)).


    4.8.  Bugs, etc., in Input and Output of Expressions


      +	 The symbol | is either Prolog-style list punctuation or part of a
	 special name.	With the built-in declaration of | as infix, the
	 term [a|b] is ambiguous, with possible interpretations
	 t_1=$cons(a,b) and t_2=$cons(|(a,b),$nil).  Otter recognizes
	 [a|b] as t_1.	 The term t_2 can be written [(a|b)].	The bug is
	 that t_2 will be output without the parentheses.  This is the
	 only case I know in which Otter cannot correctly read a term it
	 has written.

      +	 A term consisting of a unary + or - applied to a nonnegative
	 integer is always translated to a constant.

      +	 Parsing large terms without parentheses, say a1+a2+a3+...+a1000,
	 can be very slow if the operator is left associative (yfx).  If
	 you intend to parse such terms, make the operator right associa-
	 tive (xyf).

      +	 Quoted strings cannot contain a quotation mark of the same type.

      +	 The flag check_arity sometimes issues warnings when it should
	 not.

      +	 Braces () can be used to group input expressions, but Otter
	 always uses ordinary parentheses on output.

    4.9.  Examples of Operator Declarations

    Group Theory.  Suppose we like to see group theory expressions in the
    form (ab^-1c^-1-1)^-1, in which right association is assumed.
    We can approximate this for Otter with (a*b^ *c^ ^)^.
    (We have to make the group operator explicit; -1 is not a legal
    Otter name; the whitespace shown is required.)  The declarations
    op(400, xfy, *) and op(350, yf, ^) suffice.	 Other examples of expres-
    sions (with minimum whitespace) using these declarations are
    (x*y)*z=x*y*z and (y*x)^ =x^ *y^.

    Otter Options.  Options are normally input as in the following examples.

	set(prolog_style_variables).
	clear(print_kept).
	assign(max_given, 300).

    If, however, we make the declarations (the precedences are irrelevant)

	op(100, fx, set).
	op(100, fx, clear).
	op(100, xfx, assign).

    then we may write

	set prolog_style_variables.
	clear print_kept.
	max_given assign 300.

================================================================

---- With Permission ----

To: Sandro Hawke <sandro@w3.org>
Subject: Re: Is the otter manual on the web? Can I put it there? 
Date: Thu, 05 Sep 2002 11:03:40 -0500
From: William McCune <mccune@mcs.anl.gov>
Message-Id: <200209051603.g85G3fn11253@theorem.mcs.anl.gov>


You're most welcome to put any parts of the Otter manual on the web.

  Bill

---- Why? ----

Because I want to refer people to this syntax in web documents.

  - sandro
Received on Friday, 6 September 2002 12:43:14 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Wednesday, 7 November 2012 14:17:22 GMT