------------------------------------------- LOP-SYNTAX FOR THEOREM PROVING APPLICATIONS ------------------------------------------- This document originally described LOP for SETHEO. Some REMARKS have been added to point out differences to the E-LOP dialect used by E. Those are not complete. The syntax fragment of LOP relevant for theorem proving applications is inductively defined in a BNF-type format. We are using quasi-quotation technique with the following conventions. 1. `::=' is the definition symbol, and the `|' below `::=' is the logical `or' of the meta-language. 2. Strings of capital letters in the meta-language denote arbitrary strings of object-level symbols. 3. All other symbols in the definienda denote the respective object-level symbols. 4. Concatenation of strings `s1' and `s2' is expressed by writing `s1^s2'. Accordingly, the empty string in the object language is encoded with the symbol `^' in the meta-language. 5. An empty space in the meta-language between strings designates arbitrary many concatenations of empty spaces and comments in the object language, including the empty word; for the definition of comments see `COMMENT' below. Here, `\N' denotes `newline' and `\T' denotes `tabulator'. 6. The symbol `@' in the meta-language denotes an arbitrary string in the object language not containing `\', including the empty string. Definiens Definiendum CLAUSE ::= GOAL | AXIOM | QUERY | RULE GOAL ::= <- TAIL . | <- TAIL : CONSTRAINTS . REMARK: E-LOP does not support constraints! AXIOM ::= HEAD <- TAIL . | HEAD <- TAIL : CONSTRAINTS . | HEAD <- . | HEAD <- : CONSTRAINTS . REMARK: E-LOP does not distinguish GOALS and AXIOMS (although E by defaults treats all negative clauses as goals for heuristic search). QUERY ::= ?- TAIL . | ?- TAIL : CONSTRAINTS . RULE ::= LITERAL . | LITERAL : CONSTRAINTS . | LITERAL :- TAIL . | LITERAL :- TAIL : CONSTRAINTS . HEAD ::= LITERAL | LITERAL ; HEAD | LITERAL OR HEAD OR ::= | TAIL ::= SUBGOAL | SUBGOAL , TAIL | SUBGOAL AND TAIL AND ::= & LITERAL ::= ATOM | ~ ATOM SUBGOAL ::= LITERAL | BUILT_IN ATOM ::= CONSTANT | CONSTANT^TERMLIST CONSTRAINTS ::= CONSTRAINT | CONSTRAINTS , CONSTRAINT CONSTRAINT ::= [ CTERMS ] =/= [ CTERMS ] TERMLIST ::= ( TERMS ) TERMS ::= TERM | TERM , TERMS TERM ::= CONSTANT | VARIABLE | GLOBAL_VARIABLE | LIST | CONSTANT^TERMLIST CTERMLIST ::= ( CTERMS ) CTERMS ::= CTERM | CTERM , CTERMS CTERM ::= CONSTANT | VARIABLE | STRUCT_VARIABLE | LIST | CONSTANT^CTERMLIST LIST ::= [ ] | [ TERM | LIST ] | [ TERMS ] CONSTANT ::= SMALLCHARACTER^WORD | NAT | "^@^" VARIABLE ::= BIGCHARACTER^WORD | _^WORD STRUCT_VARIABLE ::= #^VARIABLE GLOBAL_VARIABLE ::= $^VARIABLE WORD ::= ^ | WORD^SMALLCHARACTER | WORD^BIGCHARACTER | WORD^CIPHER | WORD^_ SMALLCHARACTER ::= a | b | c | ... | x | y | z BIGCHARACTER ::= A | B | C | ... | X | Y | Z NAT ::= CIPHER | CIPHER^NAT CIPHER ::= 0 | 1 | 2 | ... | 7 | 8 | 9 COMMENT ::= /*^@^*/ | \N^#^@ | \T^%^@ Additionally LOP must fulfill the following consistencency condition which is different from Prolog: Each constant symbol can also occur as a function or a predicate symbol. It thus can have arity zero and, at the same time, arity n. In contrast to Prolog, however, it must never occur with more than one arity different from zero. REMARK: For E-LOP, every symbol can only occur in one of the roles (predicate symbols, function symbol, constant). GOALS are fanned and taken as top clauses. Their literals are reordered. AXIOMS are fanned but not taken as top clauses. Their literals are reordered. QUERIES are not fanned but taken as top clauses. They are not reordered. RULES are not fanned and not taken as top clauses. They are not reordered. REMARK: E only distinguishes QUERIES and other clauses if the option --sos-uses-input-types is set, in which case QUERIES are placed in the initial Set of Support. Under all other circumstances, the syntax of a clause is irrelevant. Semicolons ";" denote the logical "or". Commata "," denote the logical "and". The symbol "~" denotes the logical "not". The symbol "<-" denotes the logical "implication" (in backward direction). Definite and Indefinite Answers ******************************* QUERIES should be used to compute `definite answers'. GOALS must be used to obtain `indefinite answers'. To see the difference, consider the following example. Example 1: ^^^^^^^^^^ "<- p(X). p(a); p(b) <-." succeeds. The proof of the goal "<- p(X)" from the axiom "p(a); p(b) <-." needs two different instances of the goal. ~p(a) / \ p(a) p(b) | ~p(b). A collection of these instances determines the indefinite answer: X = a | X = b Setheo returns "SUCESS" Example 2: ^^^^^^^^^^ "?- p(X). p(a); p(b) <-." fails Since the query "?- p(X)" can be used only as a top clause, only one single instance of it can occur in each proof. Hence the tableau in example 1 cannot be derived any more. Setheo returns "TOTAL FAILURE" Example 3: ^^^^^^^^^^ "?- p(X). p(a); p(a) <-." succeeds. ~p(a) / \ p(a) p(a) The corresponding model elimination proof contains one extension and one reduction step. From the proof we read of the definite answer: X = a Setheo returns "SUCESS" Note: How definite and indefinite answers can be obtained as an output of proofs is described at the end of this manual, where we explain the BUILT-INS. Constraints *********** CONSTRAINTS are syntactical disequations of terms. They can be considered as additional subgoals of the clauses which are permanently checked. STRUCT_VARIABLES in constraints are treated as universally quantified variables in a precondition of the whole clause. The constraint [X] =/= [f(#Y)] is violated, when X is istantiated to a term of the form f(TERM). Fanning ******* In order to be complete for the Non-Horn case Setheo takes every literal of a clause as an entry literal of this clause. In the Horn case only the positive literals need to be taken into acount as entry literals. The clause p ; q <- r , s. is compiled into the following set of contrapositives. p :- ~q, r , s. q :- ~p, r , s. ~r :- ~p,~q , s. ~s :- ~p,~q , r. Subgoal reordering ****************** Axioms and goals are reordered, but rules and queries are not. Built-Ins are inserted before all other subgoals. More complex subgoals are inserted before less complex ones. Built-Ins ********* Built-ins are intended to be inserted as subgoals into the tail of procedural clauses (queries and rules). If they appear in the tail of declarative ones (goals and axioms), they are inherited to all contrapositives obtained by compiling the underlying axiom or goal. Note, that the procedural clauses are not reordered at all (they have been reordered in previous version of Setheo). The contrapositives of the declarative clauses are reordered, if subgaol reordering is not supressed. The Built-Ins of declarative clauses become the first subgoals in all contrapositives. Note: All built-ins except the destructive term assignment operations are strongly dependent from their positions in the tail. The built-ins are listed below. ------------------------------------- Assignment and destructive assignment ------------------------------------- *) Destructive term assignment to global variables BUILT_IN ::= GLOBAL_VARIABLE := TERM Example: The following program determines the minimum and the maximum element of a list. ?- minmax([17,1,5,23,3,19,7,11,13]),$write($Min),$write($Max). minmax([]). minmax([F|X]) :- $Min := F, $Max := F, minsearch(X). minsearch([]). minsearch([F|R]) :- setval(F), minsearch(R). setval(F) :- F > $Max, $Max := F. setval(F) :- F < $Min, $Min := F. setval(F). *) Destructive integer assignment to global variables: BUILT_IN ::= GLOBAL_VARIABLE :is ARITH_EXPR *) Non-destructive term assignment to logical variables: BUILT_IN ::= unify^( VARIABLE , TERM ) *) Non-destructive integer assignment to logical variables: BUILT_IN ::= VARIABLE is ARITH_EXPR Note: In contrast to global variables in some Prolog Systems for example Eclipse, destructive assignments to global variables in LOP are backtracked whenever the proof search fails at later subgoals. Note: In contrast to arithmetic assignments, term assignments can be inserted at any position in the tail. The right side of the assignment may become instantiated later. ------------------ Integer arithmetic ------------------ *) Arithmetical operations: ARITH_EXPR ::= VARIABLE | GLOBAL_VARIABLE | INTEGER | ARITH_EXPR * ARITH_EXPR | ARITH_EXPR / ARITH_EXPR | ARITH_EXPR + ARITH_EXPR | ARITH_EXPR - ARITH_EXPR | ( ARITH_EXPR ). INTEGER ::= NAT | -^NAT Note: Variables and global variables in arethmetical expressions must be instantiated by integers from the domain: [-32768..32768] Note: `*' and `/' have higher priority than `+' or `-' *) Arithmetical tests: BUILT_IN ::= ARITH_EXPR >= ARITHEXPR | ARITH_EXPR =< ARITHEXPR | ARITH_EXPR > ARITH_EXPR | ARITH_EXPR < ARITH_EXPR ---------------------------------- Unification and test for identity --------------------------------- *) Unification of terms: BUILT_IN ::= unify^( TERM , TERM ) *) Test whether two expressions are identical: BUILT_IN ::= eq^( TERM , TERM ) | TERM == TERM *) Test whether two expressions are not identical: BUILT_IN ::= neq^( TERM , TERM ) | TERM =/= TERM *) Equal predecessor check in the current tableau: BUILT_IN ::= eqpred^( NAT ) Comment: A built-in of this form fails, whenever the n-th literal in the current clause is preceeded by an identical one in the current tableau. Example: L1:- eqpred(1), /* eq pred check for the head literal L1. */ L3, eqpred(3), /* eq pred check for the literal ~L3. */ L5, eqpred(5), /* eq pred check for the literal ~L5. */ : : Note: All literals and built-ins in a clause have destinct positions in that clause. ---------------------- Metalogical predicates ----------------------- *) BUILT_IN ::= isvar^( VARIABLE ) Comment: succeeds if VARIABLE is unbound or bound to another variable *) BUILT_IN ::= isnonvar^( VARIABLE ) Comment: succeeds if VARIABLE is bound to a non-variable term *) BUILT_IN ::= isconst^( VARIABLE ) Comment: succeeds if VARIABLE is bound to a constant *) BUILT_IN ::= isnumber^( VARIABLE ) Comment: succeeds if VARIABLE is bound to an integer *) BUILT_IN ::= iscompl^( VARIABLE ) Comment: succeeds if VARIABLE is bound to a complex term *) BUILT_IN ::= isground^( VARIABLE ) Comment: succeeds if VARIABLE is bound to a ground term *) BUILT_IN ::= isunifyable^( TERM1 , TERM2 ) Comment: succeeds if TERM1 and TERM2 are unifiable *) BUILT_IN ::= isnotunifyable^( TERM1 , TERM2 ) Comment: succeeds if TERM1 and TERM2 are not unifiable !!!!!! under_scores sollten generell rein oder raus. !!!!!! fuer jedes built-in einen $. ------------------ Term manipulations ------------------ *) BUILT_IN ::= functor^( TERM ) Comment:?????????? *) BUILT_IN ::= arg^( TERM ) Comment:?????????? -------------------------------- Tests concerning term complexity -------------------------------- *) BUILT_IN ::= size^( TERM , VARIABLE ) Comment: Instantiates VARIABLE with the size of TERM. The size of a term is determined by the number of its variables, constants and function symbols (i.e. the number of destiinct positions in that term). *) BUILT_IN ::= size^( TERM , NAT ) Comment: Compares the size of TERM with the value of NAT. *) BUILT_IN ::= tdepth^( TERM , VARIABLE ) Comment: Instantiates VARIABLE with the depth of TERM. *) BUILT_IN ::= tdepth^( TERM , NAT ) Comment: Compares the depth of TERM with the value of NAT. --------------------------------------- Tests and bounds for tableau complexity --------------------------------------- *) BUILT_IN ::= getdepth^( VARIABLE ) Comment: Instantiates VARIABLE with the maximum tableau depth (allowed for a final tableau) minus current depth. *) BUILT_IN ::= getinf^( TERM ) Comment: Instantiates VARIABLE with the current number of inferences (i.e. the number of inferences needed to derive the current tableau). *) BUILT_IN ::= getmaxinf^( TERM ) Comment: Instantiates VARIABLE with the maximum number of inferences (allowed for a final tableau). *) BUILT_IN ::= setdepth^( NAT ) Comment: Set the current depth counter to the value of NAT *) BUILT_IN ::= setinf^( NAT ) Comment: Set the current inference counter to the value of NAT. *) BUILT_IN ::= setmaxinf^( NAT ) Comment: Set the maximum inference counter to the value of NAT. Note: The depth counter of Setheo is successively decremented from `maxdepth' downto `zero' when inferences are performed. The inference conter is incremented from `zero' up to `maxinf'. ------- Lemmata ------- *) BUILT_IN ::= genlemma Comment:?????????? *) BUILT_IN ::= uselemma Comment:?????????? ---------------------------------------- Other possibilities for explicit control ---------------------------------------- *) BUILT_IN ::= fail Comment: `fail' is an usolvable subgoal. *) BUILT_IN ::= stop Comment: `stop' is a subgoal letting the proof procedure halt. *) BUILT_IN ::= precut | cut Comment: If `precut' is inserted as the first subgoal of a procedural clause `cut' produces the same behaviour as the `cut' in Prolog. The Prolog clause p(X) :- q(X), !, r(X). is operationally equivalent to the LOP clause p(X) :- precut, q(X), cut, r(X). -------------------------------- Implementing Negation as Failure -------------------------------- The Prolog clause p(X) :- not q(X), r(X). is operationally equivalent to the LOP clauses p(X) :- not_q(X), r(X). not_q(X) :- precut, q(X), cut, fail. not_q(X) :- r(X). The transformation works for socalled normal programs. If you want to combine classical negation and negation as failure, you have several possibilities. Example: ^^^^^^^^ ?- p. p :- not ~p. is is usually transformed into: ?- p. p :- not_non_p. not_non_p :- precut, ~p, cut, fail. not_non_p. Setheo fails in this case, since the subgoal ~p succeeds by performing a reduction step into its tableau predecessor p. You can switch off reduction steps if you expect that p should succeed, since ~p is not provable (by ignoring its context). If you want to have reduction steps in other parts of your proofs, you should choose another transformation, where you exlicitly count the nestings of the `not's in your `proofs'. ?- p. p :- not ~p. is then transformed into: ?- p(X). p(X) :- not_non_p(s(X)). not_non_p(X) :- precut, ~p(X), cut, fail. not_non_p(X). Example: ^^^^^^^^ ?- p. p :- not p. is is usually transformed into: ?- p. p :- not_p. not_p :- precut, p, cut, fail. not_p. Setheo succeeds in this case, since the subgoal p fails by checking the regularity of the current tableau. If you don't want this behaviour either you can switch off the regularity check, or you can use again the above transformation. Then however, Setheo does not terminate any more. It runs into an infinite loop, except that you spend only finitely many resources for proofs. ------------------ Output statements ------------------ *) To open a file with filename STRING: BUILT_IN ::= tell^( "STRING" ) *) To close the file with filename STRING: BUILT_IN ::= told *) To write the value of variables into the file just opened or onto the screen: BUILT_IN ::= $write^( VARIABLE ) Note: The write statement is executed immediately whenever it is met during the search. Hence, in order to obtain the answer substitutions of a GOAL and in order to avoid that the write statements are executed permanently during the proof search, these write statements should be added as the last subgoal of an artifitial QUERY (and not of the GOAL). In order to output disjunctive answer substitutions global variables are needed: Example: Given the clauses p(a) ; p(b) <-. p(b) ; p(c) <-. the `disjunctive answers' for the GOAL <- p(X). are `X = a | X = b'. `X = b | X = c'. A program computing these answers needs a new `artificial query' containing a subgoal to enter the original goal. In this way, the goal is transformed into an axiom. The axiom however, is fanned into contrapositives. The program is given below. # In order to initialize list $L ?- $L := [], query, setdepth(1000), write_list($L). # In order to collect the answer substitutions in the list $L: query <- $L := [X|$L], p(X). # The disjunctive fact remains unchanged: p(a) ; p(b) <-. # In order to output the elements of $L: write_list([]) :- $write("."). write_list([H|T]) :- T == [], $write(H), $write(".").. write_list([H|[]]) :- T =/= [], $write(H), $write("|"), write_list(T). Note: It would be helpful if you try this program by your own with SETHEO and then have a closer look onto the proof tree using `xptree'. The subgoal "setdepth(1000)" is essential since we never want to fail during outputting an answer substituition. # In order to compute ALL POSSIBLE answer substitutions (say 100) ?- $L := [], query, setdepth(100), write_list($L), fail. Note: In this case SETHEO possibly loops for ever when it tries to compute more and more new answers.