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

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. - sandroReceived 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
*