#========================= HEURISTICP ================================== HEURISTICP contains the nial implementation of a heuristic theorem prover based on an AO* algorithm. The theorem prover is utilized by executing the PROVE transformer. PROVE takes three operations as arguments: quit_cond : decides when a proof has finished. Takes a list of results as its argument. Can be used to specify finding all solutions, only one one solution, or it can be used to interact with the user to decide whether to continue looking for solutions. process_result: does the evaluation of the variables in the goal after the proof completes. This allows for the varaibles to be printed in an interactive proof, or to be just returned in the case that the prover is being used without any side effects. node_eval : heuristically evaluates a list of literals representing a subgoal in a graph node. Returns the literals ordered as specified by the operation. This can be used to reorder the literals in the most likely to fail order. graph_eval : heuristically evaluates a graph consisting of the list of nodes holding goal and clause information. It returns one of the nodes as the next node to be expanded and the list of all the other nodes. # PROVE results in an operation that takes 4 arguments : Goals: - a list of goals to be proved stored in the form produced by build_logic. Clauseinfo: - a list of clauses to be used in the proof organized with a predicated table that gives indices and sizes of clauses with the same predicate in the head. These are also built by build_logic. D : Represents the maximum depth of the search for a solution. Any subgoal occuring below this depth bound will not be generated into a graph entry. D can be used in the heuristic function to evaluate a node. Currently D is utilized within build_graph. M0 : Represents the maximum size of a local search graph. Once the graph surpasses this size PROVE will recurse down a level. Thus, if M0 is 1 a depth first PROLOG style theorem prover will be represented. # Algorithmic notes. The resolve operation used in PROVE is very similar to that used in depthfirst, except that CUT and FAIL are not recognized as special predicates. The build_graph routine builds a node for each rule that the predicate name of the subgoal occurs in. The rule numbers are found from the Predtable data structure that is built by build_logic and is part of the Clauseinfo data structure. The main body of rprove is a WHILE loop that chooses a node of the graph and expands it using resolve. If the result is not an empty Resolvent then the Resolvent is used to add new Nodes to the graph. If the graph is larger than M0, then a recursive call is made to isolate a new local area for the search. Weightf Depthf Sindex Subgoal := tell 4; PROVE IS TRANSFORMER quit_cond process_result node_eval graph_eval OPERATION Goals Clauseinfo M0 D { LOCAL Predtable Clauses Success Result Quit I; resolve IS OPERATION Subgoal Rule { Goal Bndev Refev := Subgoal; CASE Goal@@[0,1,1,0] FROM "DO : Newbndev Newrefev Newgllits Unifiable Semlist := do_pred ( first Goal ) Bndev Refev ; END "PUT : Newbndev Newrefev Newgllits Unifiable Semlist := put_pred_value (first Goal ) Bndev Refev ; END ELSE % organize the terms to be unified; Ofsneglit Neglit := first Goal ; Ofsposlit Poslit := ( tally Bndev ) ( second Rule ) ; Numnewvars := first Rule ; Newbndev := link Bndev ( Numnewvars reshape [ Null ] ) ; Newrefev := link Refev ( Numnewvars reshape [ -1 ] ) ; % do the unification step; Newbndev Newrefev Unifiable Semlist := eqnstest cycletest bindterms Ofsneglit Neglit Ofsposlit Poslit Newbndev Newrefev l Null; IF not isfault Unifiable THEN Newgllits := third Rule ; ENDIF ; ENDCASE ; IF not isfault Unifiable THEN % set up the resolvent and return; (link (flip ((tally Newgllits) reshape [ Ofsposlit ]) Newgllits) (rest Goal)) Newbndev NewRefev l ELSE ??nores Bndev Refev o ENDIF }; build_graph IS OP D Depth Subgoal Bndev Refev Predtable { IF D > Depth THEN Predname := Subgoal@@[0,1,1,0]; IF Predname in "PUT "DO THEN % generate one node with no Rulenumber; [ [0,Depth,??isexecutable,Subgoal Bndev Refev] ] ELSE Test Pos := Predname seek Predtable@0; IF Test THEN Rulepairs := Pos pick Predtable@1; EACH (OP Rulenum Tallyp ( [Tallyp,Depth,Rulenum,Subgoal Bndev Refev])) Rulepairs ELSE Null ENDIF ENDIF ELSE Null ENDIF }; rprove IS OPERATION Goal Bndev Refev Orgvars Varnames Result Success M0 D { Graph := build_graph D 0 Goal Bndev Refev Predtable; Quit := o; WHILE not ((empty Graph) or Quit) DO Node Graph := graph_eval Graph; Resolvent Newbnd NewRefev Unifiable := resolve (Node@[Subgoal]) (Clauses@[Node@[Sindex]]); IF Unifiable THEN IF empty Resolvent THEN Result := Result append process_result Orgvars Varnames Newbnd; Quit := Quit_cond Result; Success := l; ELSE Graph := (build_graph D (1 + Node@[Depthf]) (node_eval Resolvent) Newbnd NewRefev Predtable) link Graph; WHILE tally Graph > M0 and not Quit DO NewNode Graph := graph_eval Graph; Result Success Quit := rprove (NewNode@@[Subgoal] link (Orgvars Varnames Result Success M0 D)); ENDWHILE; ENDIF; ENDIF; ENDWHILE ; Result Success Quit }; prove_goal is OP Goal { rprove Goal@@[0,1] Goal@1 Goal@2 Goal@3 Goal@@[0,2] [] o M0 D }; Predtable := 1 pick Clauseinfo; Clauses := each second (0 pick Clauseinfo); Success := o; I := 0; % loop through the goals until one succeeds; WHILE not Success and (I < tally Goals) DO Result Success Quit := prove_goal Goals@I; I := I + 1; ENDWHILE; Result Success }