The Proof Planners of Ωmega: A Technical Description

Andreas Meier DFKI Gmbh, 66041 Saarbrücken, Germany

                               E-mail: ameier@dfki.de
                     WWW: http://www.ags.uni-sb.de/~ameier/

SEKI Report SR–2004–03

SEKI-REPORT ISSN 1437-4447  UNIVERSITÄT DES SAARLANDES FACHRICHTUNG INFORMATIK D–66123 SAARBRÜCKEN GERMANY WWW: http://www.ags.uni-sb.de/

This SEKI Report was internally reviewed by: Erica Melis DFKI GmbH, 66041 Saarbrücken, Germany

E-mail: melis@dfki.de
WWW: http://www.ags.uni-sb.de/~melis/

Editor of SEKI series: Claus-Peter Wirth FR Informatik, Universität des Saarlandes, D–66123 Saarbrücken, Germany

E-mail: cp@ags.uni-sb.de
WWW: http://www.ags.uni-sb.de/~cp/welcome.html

The Proof Planners of Ωmega: A Technical Description

Andreas Meier DFKI Gmbh, 66041 Saarbrücken, Germany

                     E-mail: ameier@dfki.de
           WWW: http://www.ags.uni-sb.de/~ameier/

August 25, 2004

Abstract

The Ωmega proof development system employs proof planning for automated proof construction at the abstract level of methods. In this report we discuss the technical concepts underlying proof planning in Ωmega and give detailed descriptions of the algorithms of the two proof planners of the Ωmega system: PLAN which performs simple proof planning with methods and Multi which performs multiple-strategy proof planning.

1 Introduction

Proof planning was originally conceived as an extension of tactical theorem proving to enable automated theorem proving at the abstract level of tactics. Bundy’s key idea in [9] is to augment individual tactics with pre- and postconditions. This results in planning operators, so-called methods. Thus, proof planning integrates both, elements from tactical theorem proving and elements from Artificial Intelligence (AI) planning. In the Ωmega [56] system the traditional proof planning approach is enriched by incorporating mathematical knowledge into the planning process (see [45]) and the introduction of the additional hierarchical level of strategies (see [44]).

Domain-specific knowledge can be encoded in methods, in control rules, and in external systems such as computer algebra systems or constraint solvers. Methods can encode not only general proving steps but also steps particular to a mathematical domain. Control rules enable meta-level reasoning about the current proof planning state as well as about the entire history of the proof planning process in order to guide the search.

The simple proof planner of the Ωmega system, which is called PLAN, searches at the level of methods, i.e., it searches for applicable methods and applies the instantiated methods. Case-studies revealed the drawbacks of the simple planner: It combines the application of methods, the instantiation of variables, and backtracking in a pre-defined way. Moreover, the functionalities of these subcomponents are very restricted. The hard-coded combination of operations with restricted functionalities prohibits the use of mathematical knowledge of certain proof constructions and their combination. As a result, the planner fails on problems for which more flexibility and knowledge is needed in the proof planning process (see [44, 34]).

These observations motivated the development of proof planning with multiple strategies. Proof planning with multiple strategies decomposes the previous monolithic proof planning process and replaces it by separate but collaborating operations, so-called strategies, which can realize different plan refinements and modifications, e.g., different kinds of step (i.e., instantiated method) computation and selection, different kinds of backtracking, different kinds of variable instantiation etc. Moreover, the decision on when to apply a strategy is not encoded once and forever into a fixed control procedure but rather is determined by meta-level reasoning using heuristic control knowledge of strategies and their combination. As compared with the previous proof planning, strategies and their heuristic control introduce another hierarchical level and can encode further (mathematical) domain knowledge. We realized proof planning with multiple strategies in the Multi planner.

In this technical report, we describe the technical concepts underlying proof planning in Ωmega and give detailed descriptions of the algorithms of both planners of Ωmega. The structure of the report is as follows: We first describe the basics of knowledge-based proof planning in section 2, in particular, methods and control rules and the incorporation of external systems. In the subsequent section, we give a detailed description of PLAN including the discussion of a sample application. Section 4 introduces proof planning with multiple-strategies and gives a conceptual description of Multi, which is complemented by a detailed technical description in section 5.

2 Basics of Proof Planning in Ωmega

Proof planning in Ωmega considers mathematical theorems as planning problems and combines tactical theorem proving and AI planning techniques. Hence, we start with a brief account of how theorem proving can be seen as an AI-planning problem comprising brief discussions of the background proof development in Ωmega and AI-planning. Next, we discuss tasks and the PDS, which represent the current status during a proof planning process. Afterwards, we introduce Ωmega’s method and control rule languages, describe the instantiations of methods, which are called actions, and briefly discuss the incorporation of external systems into proof planning.

Notation Functions that are part of the descriptions of methods, control rules, and algorithms are denoted with a special font (e.g., term-at-position). Since the core of Ωmega is implemented in LISP these functions are LISP functions in the implementation. For clarity, we write the application of the function func to the arguments arg_{1}, …, arg_{2} not in LISP syntax, i.e., (func arg_{1} … arg_{n}), but in prefix notation, i.e., func(arg_{1}, …, arg_{n}).

Notation We denote a set of items it_{1}, …, it_{n} with {it_{1}, …, it_{n}}. A list or sequence of items (i.e., ordered set of items) it_{1}, …, it_{n} we write as [it_{1}, …, it_{n}]. [] denotes the empty list. On sets the operations ∪, ∩, − are defined as usual. On lists ∪ denotes the concatenation of lists. The result of list_{1} − list_{2} is list_{1} without all elements that are in list_{2}. The operations first, last, rest, and reverse are defined on lists. The function first returns the first element of a list whereas the function last returns the last element of a list. The function rest returns the list that results from the deletion of the first element from the initial list. The function reverse returns a list whose elements are in the reverse order of the elements of the input list.

The set of all items it that satisfy a certain property P (it) is written as {it|P (it)}. The analogous list is written as [it|P (it)]. The elements of such a list are ordered arbitrarily, if no order is explicitly specified.

Sets are denoted with symbols in calligraphic style (e.g., M for a set of methods and C for a set of control rules). Lists are denoted with symbols that are marked with an arrow as superscript (e.g., A⃗ for a sequence of actions).

2.1 From Theorem Proving to AI-Planning

Proof Development in Ωmega

The basic logic of the proof development system Ωmega is a higher-order variant of Gentzen’s natural deduction (ND) calculus [23]. Similar to many interactive systems (c.f., Nuprl [14], Isabelle [51], Hol [25], coq [15], QuodLibet [30]) Ωmega employs tactics for the construction of complex and more abstract proofs. The idea in tactical theorem proving [48] is that repeatedly occurring sequences of inference steps are encapsulated into macro steps, so-called tactics, which enable interactive proof construction at a higher level of abstraction.

Since tactic applications can be expanded to Ωmega’s basic ND-calculus and can be combined with the application of ND-rules Ωmega needs a hierarchical proof data structure that represents a (partial) proof attempt at different levels of abstraction. This data structure is called the proof plan data structure PDS [12]. We will present the proof objects stored in a PDS in a linearized style with proof lines as introduced in [2]. A proof line is of the form L. Δ⊢F (R), where L is a unique label, Δ⊢F a sequent denoting that the formula F can be derived from the set of hypotheses Δ, and (R) is a justification expressing how the line was derived. Lines that are not yet derived from other lines are called open lines and have an open justification. A line that is not open is called a closed line.

For instance, the initial PDS for the proof problem with theorem T hm and assumptions Ass_{1}, …, Ass_{n} is:

L_{Ass_{1}}.  L_{Ass_{1}}  ⊢ Ass_{1}  (Hyp)
⋮
L_{Ass_{n}}.  L_{Assn}  ⊢ Ass_{n}  (Hyp)
L_{T hm}.  L_{Ass_{1}} , …, L_{Assn}  ⊢ T hm  (Open)

AI-Planning

An AI-planning problem^{1} consists of

1. a description of the initial state of the world in some formal language,

2. a description of the agent’s goals in some formal language, and

3. a description of the possible operations that the agent can performs in some formal language.

An AI-planner is an algorithm that is applied to a planning problem and returns a sequence of actions, i.e., instantiated operations, which will achieve the goal, when executed in any world satisfying the initial state description. Such a sequence of actions is also called a solution plan.

A very simple, yet very influential language is the Strips representation.^{2} Strips describes the initial state of the world with a complete set of ground literals. It restricts the type of goals that may be specified to conjunctions of positive literals. Operations are represented in the Strips language as operators (also called operator schemata) with preconditions and effects. The preconditions of each operator have the same restriction as the problem’s goals: they are a conjunction of positive literals. An operator’s effects are a conjunction that may includes both, positive and negative literals. All the positive literals in the operator’s effects are called the add-list of the operator, while all the negative literals are called the delete-list of the operator.

The classical approach to solve planning problems is precondition achievement planning [17]. Precondition achievement planning goes back to the General Problem Solver, GPS [50]. Strips focused and distilled the technique to the form used in planning: During the planning process, first an unsatisfied precondition is chosen (this condition is not true and but it should be). Then, the available operators are checked whether their add list contains an effect to achieve this precondition. One operator is chosen, appropriately instantiated (bind the variables of the operator to elements of the plan), and the resulting action is inserted into the plan under development. Then, the preconditions of the introduced action become new unsatisfied preconditions of the plan whereas the initially unsatisfied precondition is satisfied by an effect of the introduced action.

Theorem Proving as AI-Planning Problem

The initial state of a proof planning problem consists of the proof assumptions and the goal description consists of the theorem. Methods are the operators of proof planning, where methods are tactics known from tactical theorem proving augmented with pre- and postconditions in order to derive operators for AI-planning. Simple proof planning searches for a solution plan, i.e., a sequence of instantiated methods that transforms the initial state into a state in which the theorem holds. In order to find a solution plan, it searches for applicable methods and applies the instantiated methods. Similar to AI-planning we call the instantiation of a method (i.e., the instantiation of a proof planning operator) an action.

1See [64, 54] for introductions to AI-planning.

2The acronym “STRIPS” stands for “STanford Research Institute Problem Solver’, a very famous and influential planner build in the 1970s to control an unstable mobile robot known as “Shakey” [21, 20].

2.2 Tasks and the PDS

Central during the proof planning process in Ωmega are so-called tasks, which express the logical dependencies between goals and assumptions, and a PDS, which represents the partial proof plan constructed so far. We shall now first explain the role of these two fundamental structures.

In AI-planning, an unsatisfied precondition in a plan under construction can be satisfied with a matching effect of any other action in the plan. In proof planning, however, this is not the case because of the logical context of open lines. Thus, Ωmega’s proof planning uses so-called tasks to express which proof lines (closed and open) can be used to construct a subplan for an open line. A task is a pair (L_{open}, SUPPS_{L_{open}}) where L_{open} is an open line and SUPPS_{L_{open}} is a set of lines. The first element of a task is called the task line or the goal of the task and the second element is called the support lines or supports. The formula of the goal is also called task formula. A task with goal L_{open} and supports SUPPS_{L_{open}} is written as L_{open} ◀ SUPPS_{L_{open}}. During the planning process a list of all current tasks is stored in a so-called agenda. For a problem with theorem T hm and assumptions Ass_{1}, …, Ass_{n} the initial agenda consists of the task L_{T hm} ◀ {L_{Ass_{1}}, …, L_{Ass_{n}}} where L_{Ass_{i}} and L_{T hm} are the proof lines of the initial PDS of the problem.

As example for the necessity to maintain a separate set of supports for each goal consider the introduction of a case-split. Let a goal F [x] have the support line x > 0 ∨ x ≤ 0.^{3} The introduction of a case-split results in two branches with: subtask F [x] ◀ {x > 0, …} and F [x] ◀ {x ≤ 0, …}. It would be incorrect, if the second subtask used the first assumption or vice versa. Moreover, actions can remove support lines of a task such that afterwards the planner cannot use these lines anymore. This is sensible, for instance, when an action simplifies a given support line with formula x + 0 > 0 to the new support with formula x > 0. Likely, the old support will not be needed anymore.

The proof plan under construction is represented in a PDS. The initial PDS consists of the lines L_{T hm} and L_{Ass_{1}}, …, L_{Ass_{n}}. The effects and the preconditions of actions in Ωmega’s proof planning are proof lines. When a new action is added, then the new lines derived by this action are added into the PDS. Moreover, all effect lines of the action are justified by an application of the method of the action to the premises of the action. For instance, if an action of method M has the premise lines L_{1} and L_{2} and the effect line L_{3}, then L_{3} becomes justified in the PDS by (M L_{1} L_{2}).

The justifications of the proof lines in the constructed PDS comprise the same information as causal links known from partial-order planning (see [64, 54]): which preconditions of an action are satisfied by which effects of other actions and – vice versa – which effects of an action are used to satisfy which preconditions of other actions. Thus, the PDS stores information such as which lines are used by actions and which lines depend on which other lines. Moreover, it keeps track of all proof lines created so far. Thereby, open lines in the PDS represent unsatisfied preconditions of actions (initially, the theorem) whereas closed lines are effects of actions (initially, the proof assumptions).

During a proof planning process, tasks in the agenda do always correspond to open lines in the PDS, that is, for an open line in the current PDS there exists a task in the current agenda with this line as goal and vice versa. Thus, with respect to the agenda and the constructed PDS, we can state the aim of the proof planning process as follows: Compute a sequence of actions, which derives, starting from the initial agenda and the initial PDS, an empty agenda and a closed PDS, that is, a PDS without open lines. The solution proof plan is a record of this sequence of actions. The simultaneous achievement of an empty agenda and a closed PDS mirrors the two roots of proof planning: From the AI-planning point of view the aim is to compute a sequence of actions that satisfy all goals, that is, to reach an empty agenda. From the tactical theorem proving point of view the aim is to apply a sequence of tactics, which result in a closed PDS.

3To simplify this example, we just write the formulas of the goal and the support line instead of the whole proof lines.

The proof planners PLAN and Multi essentially work on an agenda and its tasks. First, they compute applicable actions for the current tasks. Then, they select one action and apply it. This results in new tasks. Technically, the simultaneous maintenance of a PDS during the proof planning process is not necessary for the two planners. In particular, if needed, a closed PDS could be constructed from the computed set of actions later on. However, historically proof planning in Ωmega did construct a PDS and an agenda was only introduced as a bookkeeping mechanism for the open proof lines. Practically, the PDS is important because of two reasons: First, Ωmega’s tools for user interaction (e.g., its graphical user interface) are based on the PDS as the central data structure. During the proof planning process the constructed PDS is presented to the user as the current state of progress. When describing sample applications of PLAN and Multi in section 3.5 and 4.5 we shall also use PDSs as a means to display and discuss the constructed proof plans. Second, the PDS is a representation of the current proof plan, i.e., the current sequence of actions, and explicitly stores information that is important for the control rules (e.g., which lines depend on which other lines etc.). Although this information could be computed from the current sequence of actions each time it is needed, it is more convenient to use the PDS as a bookkeeper.

2.3 Methods

Methods encode the knowledge of the relevant proof steps of mathematical domains. Technically, a method in Ωmega is a frame data structure with the slots declarations, parameters, application conditions, premises, conclusions, outline computations, expansion computations, and proof schema.

The premises and conclusions of a method specify the preconditions and the effects of the method.^{4} The conclusions should be logically inferable from the premises. The union of conclusions and premises is called the outline of a method. Declarative descriptions of the formulas of the outline can be given in the proof schema, which also provides the schematic or procedural expansion information (see below).

Premises and conclusions may be annotated with ⊕ and ⊖. The annotations are needed to indicate whether a method is used for forward or backward search. As opposed to AIplanning, where operators typically can be applied for both forward search and backward search, a method in Ωmega is either used in forward search or in backward search. This is because methods typically comprise complex computations that are reasonable either in one direction or in the other direction.

4That preconditions and effects of a method are called the premises and conclusions of the method, respectively, is an example for the combination of AI-planning and tactical theorem proving in proof planning. If we see the method as tactic, then the effects of a method are the conclusions of a tactic and the preconditions are the premises.

As example, consider methods that employ a computer algebra system to simplify numerical expressions. A backward method can employ the computer algebra system in order to reduce a goal to a simplified goal. A corresponding forward method can employ the computer algebra system in order to derive a simplified support line. But what should the backward method perform when applied forwards? Does it obtain a “simplified” support line and tries to “complicate” it in order to obtain a more “difficult” support? Vice versa, what should the forward method perform when applied backwards? Does it obtain a “simplified” goal, which it tries to “complicate”?

Backward and forward methods are specified as follows: A backward method has ⊖ conclusions and ⊕ premises as well as ⊖ premises and blank premises. To compute an action of the method, one of the ⊖ conclusions is matched with the goal of a given task and both, the ⊖ premises and the blank premises, are matched with supports of the task. When the resulting action is introduced into the proof plan, then the goal is closed in the PDS and the ⊕ premises are added to the PDS and become goals of new tasks. These new tasks inherit the supports of the initial task except that the ⊖ premises are removed. The blank premises are not affected. A forward method has ⊕ conclusions as well as ⊖ premises and blank premises. To compute an action of the method, the ⊖ premises and the blank premises are matched with the support lines of a given task. When the resulting action is introduced into the proof plan, then the ⊕ conclusions are added to the PDS and become new support lines of the task. Moreover, the ⊖ premises are removed from the supports of the task. Again, the blank premises are not affected.

Consider the method =Subst-B, given in Figure 1, which can be used in all domains that employ the equality =^{.}. Essentially, the method performs an equality substitution. It has two preconditions L_{1} and L_{2}, where the proof schema determines L_{1} to be an equation. The only conclusion is L_{3}. =Subst-B is a backward method. The introduction of an action of =Subst-B closes a task line whose formula matches with the formula of L_{3} and introduces a new task whose goal is the instantiation of L_{2}. That is, the formula of the new goal results from the formula of the initial goal by substitution with the equation, which is the formula of a support of the initial task that matched with L_{1}. For instance, =Subst-B applied to the task even(a + 1) ◀ {a = 1, …}^{5} introduces the new goal even(1 + 1).

In the declarations of a method the variables of the method and their types are introduced.

The parameters of a method are specific variables that influence the resulting action, when the method is instantiated. The =Subst-B method has the parameter pos which is of type position. The method can be applied to different positions, e.g., for the task even(a + a) ◀ {a = 1, …} at the first or the second occurrence of a in the goal. The choice of pos determines which a should be replaced.

The application conditions of a method are meta-level descriptions that restrict the applicability of a method. The application conditions can consist of arbitrary LISP functions. The method =Subst-B has two application conditions: (1) the position pos has to be a

5To simplify this example, we just write the formulas of the goal and the support line instead of the whole proof lines.

Method: =Subst-B

declarations

type-variables: α

variables: f_{o}, f′_{o}, t_{α}, t′_{α}, posposition

tf_{α}, tf′_{α}, λf_{αo}
parameters  pos

appl. conds.

(1) valid-position-p(f,pos)

(2) [term-at-position(f,pos) = t ∨ term-at-position(f,pos) = t′]

premises  ⊕L_{2}, L_{1}
conclusions  ⊖L_{3}

outline computations f′ ← replace-at-position (f,t,t′,pos)

expansion computations

tf ← term-at-position(f,pos) tf′ ← term-at-position(f′,pos) λf ← lambda-abstraction(f,pos)

proof schema  \begin{matrix}L_{1}. & Δ ⊢ & t=^{.}t′ & () \\ L_{2}. & Δ ⊢ & f′ & (Open) \\ L_{4}. & Δ ⊢ & ∀P_{αo} P (tf′) ⇒ P (tf) & (≡_{E} =^{.}) \\ L_{5}. & Δ ⊢ & (λf)(tf′) ⇒ (λf)(tf) & (∀_{E} L_{4} λf) \\ L_{6}. & Δ ⊢ & f[tf′] ⇒ f[tf] & (λ↔ L_{5}) \\ L_{3}. & Δ ⊢ & f & (⇒_{E} L_{2} L_{6}) \end{matrix}

Figure 1: The =Subst-B method.

valid position in the formula f and (2) the subterm in f at the position pos is t or t′. Note that application conditions reason only about whether the application of a method is valid in a certain situation; they do not reason about whether the application is useful.

The outline computations of a method allow to apply arbitrary LISP functions to compute the new terms and formulas of new outline lines generated by an application of the method. The outline computation of =Subst-B specifies that the new formula f′ is computed from f by replacing t by t′ or t′ by t at the position pos depending on whether the subterm in f at position pos is t or t′.

Similarly, the expansion computations of a method allow to apply arbitrary LISP functions to compute the new terms and formulas generated during the expansion of an action of the method. The expansion computation of =Subst-B specifies that the terms tf and tf′ are computed as the subterms of f and f′ at position pos, respectively. Moreover, the term λf is computed as a λ-abstraction of f where the term at position pos is replaced by the λ -bound variable (that is, essentially λf has the form λx_{α} f[x], where f[x] is the term that results from f by replacing the subterm at position pos by x).

The proof schema of a method is a declarative description of the outline of a method and of the expansion of actions of the method. Expansions of actions corresponds to both tactic expansions and expansions of HTN-planning [60]. When an action of the method is expanded, then for each conclusion a new subproof is introduced into the PDS resulting in new justifications of the conclusion at a lower level of abstraction. For instance, the proof schema of =Subst-B specifies that the defined concept =^{.} in the premise is replaced by its definition. Then, the calculus rules ∀_{E}, λ↔, and ⇒_{E} are applied to derive the conclusion of the method.

Generally, proof construction may require to construct mathematical objects, for instance, if a method has to instantiate existentially quantified variables by witness terms. A witness term has to be a concrete term. However, if the method is applied at an early stage of the proof, the planner generally has no knowledge of the true nature of the witness term. Therefore, the actual instantiation of witnesses is postponed; rather, methods introduce so-called meta-variables as temporary substitutes for the actual witness terms, which will be determined at a later point in the planning process and subsequently instantiated.

Notation In this report, we write mv for meta-variables. If several meta-variables occur, we attach subscripts to mv in order to distinguish the meta-variables. We either use the variable for whose instantiation the meta-variable is a substitute as subscript (e.g., we write mv_{x} if mv is a substitute for the instantiation of the variable x) or we use numbers. If the decomposition of a quantified formula results in the introduction of a constant, then we write c for this constant. Similar to the notation for meta-variables, we use either the initial variable or numbers as subscripts to distinguish several occurring constants.

Notation Methods are written in small capital font (e.g., =Subst-B). The name of backward methods ends with -B whereas the name of forward methods ends with -F.

2.4 Actions

An action is an instantiation of a method. Technically, an action in Ωmega is a frame data structure that has the slots method, task, premises, conclusions, binding, and constraints. The method of an action is a pointer to the method of which the action is an instantiation. The task of an action is a pointer to the task with respect to which the action was computed. The conclusions and premises of an action are sets of proof lines, respectively, which can be annotated with ⊖ and ⊕. The binding of an action is a substitution that (1) maps outline lines of the method to proof lines and (2) maps variables specified in the declarations of the method to terms, positions, etc. The constraints of an action are constraints that can be created by the evaluation of the application conditions of a method and that have to be passed to external constraint solvers (see section 2.6). Similar to methods, we call the union of the premises and conclusions of an action the outline of the action. The union of ⊕ premises and ⊕ conclusions of an action is also called the new lines of an action (i.e., the proof lines which are produced by an action), whereas the union of ⊖ premises, blank premises, and ⊖ conclusions is called the given lines of an action (i.e., the proof lines which have to be given in order to compute an action). Actions of forward methods are also called forward actions whereas actions of backward methods are also called backward actions.

Example 2.1

Consider the action in Figure 2. It is an instantiation of the method =Subst-B computed with respect to the task L_{T hm} ◀ {L_{Ass_{1}}, L_{Ass_{2}}}. The proof line L_{T hm} is the only conclusion of the action (annotated with ⊖) whereas the proof lines L_{Ass_{1}} and L_{T hm′} are the premises of the action (L_{T hm′} annotated with ⊕). The binding maps all outline lines of the =Subst-B method (i.e., L_{1}, L_{2}, L_{3}) to the conclusions and the premises of the action and maps all

Action

method =Subst-B
task  L_{T hm} ◀ {L_{Ass_{1}}, L_{Ass_{2}}}
premises \begin{matrix}⊕ L_{T hm′}. L_{Ass_{1}}, L_{Ass_{2}} ⊢ even(c + b) (Open) \\ L_{Ass_{1}}. L_{Ass_{1}} ⊢ a=^{.}c (Hyp) \end{matrix}
conclusions ⊖ L_{T hm}. L_{Ass_{1}}, L_{Ass_{2}} ⊢ even(a + b) (Open)
binding  \begin{matrix}\{L_{3} → L_{T hm}, L_{1} → L_{Ass_{1}}, L_{2} → L_{T hm′}, f → even(a + b), α → ν, \\ t → a, t′ → c, pos →< 1 1 >, f′ ↦ even(c + b)\} \end{matrix}
constraints ∅

Figure 2: An action with the =Subst-B method.

variables declared in =Subst-B to terms and positions. The constraints of this action are empty.

The instantiation of a method in order to compute an admissible action comprises the following steps: First, the formulas of the conclusions and premises have to be matched with formulas of goals and their supports. If this succeeds, then the application conditions can be evaluated. If they evaluate to true, the method is applicable (wrt. to the computed matchings). Then, the outline computations have to be performed and the new lines of the outline have to be computed to complete the action. A detailed description on how actions are computed, selected, and introduced into a proof plan is given in the next section, when we describe PLAN. For the action in Figure 2 we give a summary of the computation and introduction into a proof plan here.

Suppose the current PDS corresponding to the task L_{T hm} ◀ {L_{Ass_{1}}, L_{Ass_{2}}} is:

\begin{matrix}L_{Ass_{1}}. & L_{Ass_{1}}  ⊢ & a_{ν}=^{.}c_{ν} & (Hyp) \\ L_{Ass_{2}}. & L_{Ass_{2}}  ⊢ & b_{ν}=^{.}c & (Hyp) \\ L_{T hm}. & L_{Ass_{1}} , L_{Ass_{2}} ⊢ & even_{νo}(a + b) & (Open) \end{matrix}

When the action in Figure 2 is computed, then first the lines L_{1} and L_{3} of the method =Subst-B are matched with the lines L_{Ass_{1}} and L_{T hm} of the PDS, respectively. Afterwards, the application conditions are evaluated and the outline computations of the method are performed. Next, the missing outline is computed. In our example, the new ⊕ premise L_{T hm′} is computed and is justified with Open. When the action is introduced, then its effect L_{T hm} is justified in the PDS by an application of the method =Subst-B to the premises L_{T hm′} and L_{Ass_{1}} of the action. Moreover, the new proof line L_{T hm′} is introduced into the PDS. The resulting PDS is:

\begin{matrix}L_{Ass_{1}}. & L_{Ass_{1}}  ⊢ & a_{ν}=^{.}c_{ν} & (Hyp) \\ L_{Ass_{2}}. & L_{Ass_{2}}  ⊢ & b_{ν}=^{.}c & (Hyp) \\ L_{T hm′}. & L_{Ass_{1}} , L_{Ass_{2}} ⊢ & even(c + b) & (Open) \\ L_{T hm}. & L_{Ass_{1}} , L_{Ass_{2}} ⊢ & even_{νo}(a + b) & (=Subst-B L_{T hm′} L_{Ass_{1}}) \end{matrix}

The task L_{T hm} ◀ {L_{Ass_{1}}, L_{Ass_{2}}} is then replaced by the task L_{T hm′} ◀ {L_{Ass_{1}}, L_{Ass_{2}}} in the agenda.

Proof planning in Ωmega is a process that computes actions and introduces them into the proof plan under construction. However, since the introduced actions are represented in the PDS as applications of their methods we also use the phrase action application instead of action introduction, if we want to emphasize the changes in the PDS. We also use the following vocabulary from tactical theorem proving. We say that the application of a backward action closes an open line or a task, if the open line or the goal of the task is an effect of the action and is closed by the introduction of the action into the proof plan under construction. We say that a forward action is applied to some lines or to some supports, if the lines or supports are the preconditions of the action. Moreover, we say that we apply a method to a task or to some lines as an abbreviation for the application of an action of the method to the task or to some lines.

2.5 Control Rules

Control rules provide guidance of the proof planning process by declaratively representing heuristical knowledge that corresponds to mathematical intuition about how to prove a goal in a certain situation. In particular, these rules provide the basis for meta-level reasoning and a global guidance since they can express conditions for a decision that depends on all available knowledge about the proof planning process so far. Several experiments indicate the superiority of a separate representation of control knowledge by control rules [49]. This representation is well-suited for modifications and for learning. The control rules used in Ωmega’s proof planning were adopted from the control rule approach of the AI-planner Prodigy [62],

In the planning process control rules guide decisions at choice points, e.g., which task to tackle next or which method to apply next. They achieve this by reasoning about the heuristic utility of different alternatives^{6} in order to promote the alternatives that seem to suit best in the current situation, where ‘situation’ comprises all available information on the current status such as the current tasks, their supports, the planning history, failed attempts etc. To manipulate an alternative list control rules can remove elements, prefer certain elements, or add new elements. This way, the ranking of alternatives is dynamically changed. This can help to prune the search space or to promote certain promising search paths.

Technically, control rules consist of an IF- and a THEN-part. The IF-part is a predicate on the current proof planning ‘situation’, whereas in the THEN-part modifications of alternative lists are stated. Moreover, each control rules specifies its kind, i.e., the choice point in the proof planning process it guides.

Figure 3 gives as example the control rule prove-inequality, which is evaluated during the selection of the next method to apply. In its IF-part prove-inequality checks whether the current goal is an inequality. If this is the case, it prefers the methods TellCS-B, TellCS-F, AskCS-B, Simplify-B, Simplify-F, Solve*-B, ComplexEstimate-B, and SetFocus-B in this order (these methods are explained in section 2.6 and section 3.5). The prefer states that the methods specified in the control rule are preferred before all other methods, i.e., the specified methods are ordered in front of the resulting alternative list.

6As opposed to application conditions of methods, which reason about the legal feasibility of applications of methods (see last section).

    (control-rule prove-inequality
                  (kind methods)
                  (IF (and (goal-matches (REL A B))
                           (in REL {<, >, ≤, ≥})))
                  (THEN (prefer (TellCS-B TellCS-F AskCS-B Simplify-B

                                 Simplify-F Solve*-B ComplexEstimate-B

                                 SetFocus-B))))

Figure 3: The control rule prove-inequality.

Other possible modifications of alternative lists are select, reject, defer, and order-in-front. select states that all other methods except those specified in the control rule are eliminated from the list of alternative methods. reject removes all alternatives specified in the control rule from a given alternative list, the latter two manipulations reorder the alternative list. defer orders all specified alternatives at the end of the alternative list, and order-in-front orders specified alternatives in front of other specified alternatives. Finally, there is the insert modification. It allows to introduce new elements in an alternative list. A typical situation for using an insert control rule is when a general control rule – which is applied first – removes some elements from the alternative list, which are needed in a particular situation. Then a more specific insert control rule, which is applied later on, can introduce the needed elements again.

Notation Control rules are denoted in the typewriter font (e.g., prove-inequality). Technically, control rules are frame data structures. Since they are considerably simpler as, for instance, methods, we do not present them in the data structure fashion (as we do with methods) rather we give their LISP encoding. That is, the content of Figure 3 is the specification of the control rule prove-inequality as it is in Ωmega’s data base.

2.6 Incorporating External Systems into Proof Planning

We use a special kind of domain knowledge in Ωmega, namely the knowledge about and in external “expert” systems. Proof problems usually require many different capabilities for their solution, for instance, computation and object construction. In order to solve problems, it is often necessary to access several systems with complementary capabilities and to make use of their results. Various “expert” systems exist for mathematical problem solving, which have their specific data structures and very efficient algorithms, e.g., computer algebra systems, constraint solvers, model generators, and machine-oriented automated theorem provers. They can support the proof planning process by performing computations, detecting inconsistencies, suggesting instantiations of variables, or solving subproblems.

In general, Ωmega’s proof planning can treat computations from external systems in two ways: as hints or as proof steps. The difference is that the soundness of hints is checked by the subsequent proof planning process, which either fails or succeeds for the given hint. To guarantee the soundness of proof steps, special procedures have to be provided, which transform the output of an external system into a subproof that Ωmega can check, i.e., special procedures that perform the expansion of such proof steps to ND. Technically, the interface of proof planning to external systems is realized by the LISP functions of methods and control rules. Methods can call external systems in their application conditions and outline computations;^{7} similarly, control rules can employ external systems in the predicates of their IF-part.

Figure 4 and Figure 5 show the two methods ComplexEstimate-B and TellCS-B whose application conditions comprise calls to external systems, respectively. Both methods are central for planning limit problems (see section 3.5).

Method: ComplexEstimate-B

declarations

variables: b, ϵ, a, ϵ′, l, k, aσ, kσ, lσ, bσ, ϵσ, ϵ′σ,

conjunct, σ

meta-variables: mv

parameters

appl. conds.  linearextract(a, b, l, k, σ)
premises  L_{1}, ⊕L_{2}, ⊕L_{4}, ⊕L_{5}, ⊕L_{6}, ⊕L_{7}
conclusions  ⊖L_{9}

outline computations

aσ := subst-apply(σ, a) kσ := subst-apply(σ, k) lσ := subst-apply(σ, l) bσ := subst-apply(σ, b) ϵσ := subst-apply(σ, ϵ) ϵ′σ := subst-apply(σ, ϵ′) conjunct := form-conjunction(σ)

expansion computations

proof schema

L_{1}. Δ ⊢ |a| < ϵ′  ()
L_{2}. Δ ⊢ ϵ′σ < \frac{ϵσ}{2∗mv}  (Open)
L_{3}. Δ ⊢ |aσ| < \frac{ϵσ}{2∗mv}  (< trans L_{1} L_{2})
L_{4}. Δ ⊢ |kσ| ≤ mv  (Open)
L_{5}. Δ ⊢ |lσ| < \frac{ϵσ}{2}  (Open)
L_{6}. Δ ⊢ 0 < mv  (Open)
L_{7}. Δ ⊢ conjunct  (Open)
L_{8}. Δ ⊢ bσ=^{.}kσ ∗ aσ + lσ (CAS)
L_{9}. Δ ⊢ |b| < ϵ  (fix L_{3} L_{4} L_{5} L_{6} L_{7} L_{8})

Figure 4: The ComplexEstimate-B method.

ComplexEstimate-B is a method for estimating the magnitude of the absolute value of complex terms.^{8} ComplexEstimate-B is applicable to tasks whose goal has the formula |b| < ϵ (corresponding to line L_{9} in Figure 4) and that have supports with formula |a| < ϵ′ (corresponding to line L_{1} in Figure 4). In its application conditions ComplexEstimate-B uses the function linearextract. When applied to a and b linearextract employs the computer algebra system Maple [52] to compute suitable terms k and l such that b = k ∗ a + l holds. linearextract also computes a substitution σ such that bσ = kσ∗aσ+lσ holds (where bσ, kσ, lσ result from b, k, l by the application of the substitution σ, respectively). Thereby, the substitution σ maps meta-variables in a, b to terms. ComplexEstimate-B is applicable only, if Maple provides k and l such that linearextract evaluates to true. If this is the case, the application of a corresponding action of the method reduces the original task to five tasks whose goals correspond to the lines L_{2}, L_{4}, L_{5}, L_{6}, L_{7} in Figure 4. L_{7} has the formula conjunct, which is computed from the substitution σ by the function form-conjunction. This formula is the conjunction of the mappings of the substitution σ. That is, if σ maps the meta-variables mv_{1}, …, mv_{n} to the terms t_{1}, …, t_{n}, respectively, then conjunct has the form mv_{1}=^{.}t1 ∧ … ∧ mv_{n}=^{.}t_{n}. If σ is empty, then conjunct is simply T rue, the primitive truth. The justification fix for L_{9} in the proof schema is only an abbreviation that stands for a sequence of about 20 tactic steps that comprises, in particular, an application of the triangle inequality. The application of Maple is reflected in line L_{8} of the proof schema, which is justified by the tactic CAS. When this tactic is expanded, it employs the sapper [58] system to obtain a formal proof of the statement bσ = kσ ∗ aσ + lσ suggested by Maple.

7Technically, calls of external systems in the expansion computations of methods are also possible.

Currently, there is no method that performs such calls.

8ComplexEstimate-B essentially is a reconstruction (see [41]) of Bledsoe’s limit heuristic that was used in a special-purpose program [8].

For instance, when applied to a task with formula |(f(c_{x}) − g(c_{x})) − (l_{1} − l_{2})| < ϵ and a support with formula |f(mv_{x}) − l_{1}| < ϵ′ with a meta-variable mv_{x}, then linearextract succeeds and provides k = 1, l = g(c_{x}) − l_{2}, and a substitution σ that maps mv_{x} to c_{x}. The application of a corresponding action of ComplexEstimate-B reduces the given task to

new tasks whose goals are |1| ≤ mv, ϵ′ < \frac{ϵ}{2∗mv}, |g(c_{x}) − L_{2}| < \frac{ϵ}{2}, 0 < mv, and mv_{x}=^{.}c_{x}.

Method: TellCS-B

declarations variables: a, b, rel

parameters

appl. conds.

(1) metavar-in(a) ∨ metavar-in(b)

(2) test-CS (CoSIE,rel(a, b))

premises

conclusions  ⊖L_{1}

outline computations expansion computations

proof schema  L_{1}. Δ ⊢ rel_{oνν}(a_{ν}, b_{ν})  (P roveCS)

Figure 5: The TellCS-B method.

The method TellCS-B realizes an interface to CoSIE [47], a constraint solver for inequalities and equations over the field of real numbers. TellCS-B is applicable to tasks with formulas rel(a, b) where rel is a binary predicate. Examples of matching predicates are, for instance, <, ≤. In its application conditions TellCS-B first tests whether a or b contain some meta-variables. If this is the case, rel(a, b) is interpreted as a constraint on these meta-variables. TellCS-B applies then the function test-CS that connects to CoSIE to test (1) whether rel(a, b) is a syntactically valid constraint for CoSIE (in particular, rel has to be <, ≤, >, ≥, =^{.}, or ≠) and (2) whether rel(a, b) is consistent with the current constraint store of CoSIE. If this is the case, TellCS-Bis applicable and the corresponding action of TellCS-B contains in its constraints slot the constraint rel(a, b). The introduction of the action closes the goal without producing further subtasks and passes rel(a, b) as new constraint to CoSIE.

Figure 6 shows an action of the method TellCS-B. This action contains the constraint 0 < mv_{D}, which is annotated with CoSIE to indicate that the constraint has to be passed to CoSIE. The constraint results from the evaluation of the application condition test-cs of TellCS-B.

Action

method TellCS-B
task  L_{10} ◀ {L_{4}, L_{5}}

premises

conclusions ⊖ L_{10}. L_{4}, L_{5} ⊢ 0 < mv_{D} (Open)
binding {L_{1} → L_{10}, a → 0, b → mv_{D}, rel →<}
constraints {CoSIE:0 < mv_{D}}

Figure 6: An action with the TellCS-B method.

CoSIE can provide instantiations of the constrained meta-variables that are consistent with the collected constraints. For instance, suppose during the proof planning process there are three tasks whose goals have the formulas 0 < mv_{D}, mv_{D} < δ_{1}, mv_{D} < δ_{2}, which all contain the meta-variable mv_{D}. All three goals are closed by actions of TellCS-B. Moreover, suppose there are also two supports with formulas 0 < δ_{1} and 0 < δ_{2}, which are passed to CoSIE by actions of the method TellCS-F, which is the analogous of TellCS-B to pass constraints in supports to CoSIE. From the resulting constraint store, CoSIE can compute min(δ_{1}, δ_{2}) as suitable instantiation for mv_{D}. Moreover, CoSIE provides traces of its computations, which can be used to expand the applications of the actions of TellCS-B.

Another method that establishes a connection to CoSIE is AskCS-B. Similar to TellCS-B, this method is applicable to tasks whose goal formulas are of the form rel(a, b). But whereas TellCS-B demands that a or b contain some meta-variables, AskCS-B covers the case that a and b contain no meta-variables. An application condition of AskCS-B passes the formula to CoSIE and asks CoSIE whether the formula holds with respect to the constraints collected so far. If this is the case, then AskCS-B closes the goal. Since CoSIE can also handle formulas on concrete real numbers, for instance, 1 < 2 or 0 ≤ 0, AskCS-B can also close goals whose formulas are expressions on concrete real numbers.

Note that besides TellCS-B and TellCS-F also the methods ∀I-B and ∃E-F pass constraints to CoSIE. Actions of ∀I-B perform backward applications of the ND-rule ∀_{I} by reducing a task with task formula ∀x P [x] to a new task with task formula P [c], where the variable x is replaced by a constant c. For each meta-variable mv in P [c] an action of ∀I-B also passes the Eigenvariable constraint c!∉mv to CoSIE that states that the instantiation for mv is not allowed to contain c. This constraint guarantees the adherence with the Eigenvariable conditions of the ∀_{I} rule of the ND-calculus. Actions of the ∃E-F method perform a forward step with the ∃_{E} rule. Similar to action of ∀I-B they pass Eigenvariable constraints to CoSIE that demand the adherence of the Eigenvariable conditions of the ∃_{E} rule.

3 Proof Planning with PLAN

PLAN is Ωmega’s simple proof planner. It proceeds by successively computing and introducing actions into a proof plan under construction. Preceding the formal description of PLAN (see section 3.2), Table 1 shows the skeleton of PLAN’s algorithm. Essentially, PLAN follows the precondition achievement paradigm (see section 2.1). First, it selects a task to work on. Then, it computes actions for this task and selects one action, which it introduces into the proof plan under construction. This results in new tasks on which PLAN continues. If PLAN fails to compute an action for a selected task, then it performs backtracking. Although actions can perform both, forward reasoning and backward reasoning, an action is always chosen with respect to a task in order to close or to reduce the gap between the goal and the supports of the task.^{9} Some decisions in PLAN can be guided by control rules, for instance, the selection of the next task and the selection of the next action. Other decisions, however, are hard-coded into the system. For instance, PLAN employs backtracking if and only if it tackles a task, for which it fails to compute an action. Moreover, it employs external constraint solvers to obtain instantiations for meta-variables if and only if the agenda is empty and the PDS is closed.

1. When the current agenda is empty and the current PDS is closed, then apply external constraint solvers to compute variable instantiations consistent with the collected constraints and terminate.

2. Select a task T from the agenda.

3. Compute and select an action A with respect to T.

4. If an action A could be computed for T, then introduce A. Goto step 1.

5. If no action A could be computed for T, then backtrack the action whose introduction created the task T. Goto step 1.

Table 1: Cycle of PLAN.

A node in the search space of PLAN is given by a set of tasks, i.e., an agenda. PLAN starts with the initial agenda. The next node in the search space is reached by the introduction of an action, which changes the agenda etc. A forward action creates a new task by changing the supports of a given task whereas a backward action replaces a task by some new tasks with new goals. The planning process stops as soon as a node in the search space is reached whose set of tasks is empty.

Proof planning does not suffer from the conjunctive goal problems of AI-planners that perform precondition achievement planning.^{10} The derivation of a formula F in the subplan for a subgoal is not threatened or removed by the derivation of the negated formula ¬F in the subplan for another subgoal. Hence, PLAN does not perform any threat resolution like demotion or promotion of actions. Moreover, since no re-ordering of introduced actions is performed, PLAN is a total-order planner that computes a sequence of actions.

9In the existing implementation PLAN can introduce a forward action with respect to several tasks simultaneously. This corresponds to the successive application of several actions to a single task, respectively. In order to simplify the formal discussion of PLAN we shall describe the action introduction only with respect to one task.

10Given a conjunctive goal, it seems natural to try divide and conquer, but the subplans achieving the single subgoals may interfere and do not achieve the desired goals together. A famous example for this problem is the so-called “Sussman anomaly” problem in the blocks world. A detailed discussion of planning

PLAN’s subprocedure for action deletion performs dependency-directed backtracking (e.g., see [59]). Instead of backtracking to the last decision point (so-called chronological backtracking), the idea of dependency-directed backtracking is to analyze which decisions along a search branch caused a failure. Then, decisions are removed and alternatives are tried based on the found dependencies, rather than the chronological order in which decisions were made. Since there is some ambiguity in the previous use of the term dependencydirected backtracking. We use the term as defined in [53] (p. 212): “Sometimes, though, we have additional information that tells us which guess (along a search branch) caused the problem. We’d like to retract only that guess and the work that explicitly depended on it, leaving everything else that has happened in the meantime intact. This is exactly what dependency-directed backtracking does.” Note that in this approach dependency-directed backtracking does not return to an already visited search state but can lead to a new state not visited before. In [24] the same approach is called dynamic backtracking because of the dynamic way in which the search is structured. In [28] the term dependency-directed backtracking refers to the approach that analyzes which decision caused a failure and to backtrack to this choice point. That is, all steps done after this decision are removed and an already visited search state is reached again.

Besides the information on the current planning state PLAN has also to maintain information on the search performed so far. In particular, it is necessary to store and make use of information on failing decisions in order to try alternatives instead. Search procedures that perform chronological backtracking often use search trees, which capture possible alternatives as well as made and failed decisions to store information on the traversed search space (e.g., see [1]). Since PLAN performs dependency-directed backtracking we decided for a different approach. PLAN maintains a so-called history. A history is a sequence of manipulation records. Figure 7 shows the skeletons of the two manipulation records, the action-introduction record and the action-deletion record, of PLAN.

Action-Introduction:

agenda

introduced-action alternatives new-tasks

Action-Deletion:

agenda

deleted-action

Figure 7: Manipulation records in PLAN.

The slot agenda captures the context in which the manipulation was done (i.e., the agenda before the manipulation), the slots introduced-action and deleted-action capture the performed manipulation (i.e., the introduced or deleted action), the slot alternatives captures alternative actions available as the introduced action was chosen, and the slot new-tasks captures the new tasks created by the application of the chosen action. PLAN records each action introduction or deletion with a corresponding entry in the history. It makes direct use of this information, when selecting the next action: it does not choose again an action that was already deleted (see section 3.4). Since PLAN does not return to a particular search state it does not make direct use of the stored alternative actions. However, the information of the history is available to the control rules, which can reason on backtracked steps and possible alternative actions.^{11}

in the blocks world as well as the “Sussman anomaly” can be found in standard AI-textbooks, e.g., in [54].

In the remainder of this section, we give a detailed description of PLAN. First, we give some formal definitions that culminate in a definition of proof plans and solution proof plans. Then, the subsequent sections give detailed descriptions of PLAN’s main algorithm and its subalgorithms for action computation and deletion. As conclusion of the section, we discuss a sample application of PLAN.

Notation In the remainder of the report, the following symbols (maybe labeled with some subscripts or superscripts) are associated with the following objects:

A⃗ denotes a sequence of actions,
P denotes a PDS,
Â denotes an agenda,
H⃗ denotes a history.

3.1 Formal Definition of Proof Plans in PLAN

The aim of this section is to give a formal description of proof plans. We start with definitions of a proof planning problem, an initial PDS of a proof planning problem, and an initial agenda of a proof planning problem.

Definition A proof planning problem is a quadruple (T hm, {Ass_{1}, …, Ass_{n}}, M, C) where T hm and Ass_{1}, …, Ass_{n} are formulas in Ωmega’s higher-order language, M is a set of methods, and C is a set of control rules. T hm is also called the theorem of the proof planning problem whereas Ass_{1}, …, Ass_{n} are called the assumptions of the proof planning problem.

Definition Let (T hm, {Ass_{1}, …, Ass_{n}}, M, C) be a proof planning problem. The initial PDS of this proof planning problem is the PDS that consists of an open line L_{T hm} with formula T hm and the lines L_{Ass_{i}} with formula Ass_{i} and the hypothesis justification Hyp, respectively. The initial agenda of the proof planning problem is the agenda that consists of the task L_{T hm} ◀ {L_{Ass_{1}}, …, L_{Ass_{n}}}. The task L_{T hm} ◀ {L_{Ass_{1}}, …, L_{Ass_{n}}} is also called the initial task of the proof planning problem.

Next, we define, when an action is applicable with respect to a PDS. Informally speaking, this is the case, when the given lines of the action are in the PDS. Afterwards, we introduce the action introduction function Φ, which describes the operational semantics of an action when it is applied to an agenda, a PDS, and a sequence of actions (i.e., Φ defines a transition relation between triples of agendas, PDSs, and sequences of actions).

11We are currently extending manipulation records to capture also information on the reasons that support a certain decision.

Definition Let P be a PDS and A_{add} an action. Moreover, let L be the set of proof lines of P and let ⊖Concs be the ⊖ conclusions, ⊖P rems the ⊖ premises, and BP rems the blank premises of A_{add}.

A_{add} is applicable with respect to P if

• (⊖Concs ∪ ⊖P rems ∪ BP rems) is a subset of L.

Definition The action introduction function Φ is a partial function that maps a sequence of actions, an agenda, a PDS, and an action into a sequence of actions, an agenda, and a PDS, i.e.,

Φ : A⃗ × Â × P × A_{add} ↦ A⃗’ × Â’ × P’.

Let A_{add} be an action that is applicable with respect to the PDS P. Let ⊕Concs be the ⊕ conclusions, ⊖Concs the ⊖ conclusions, ⊕P rems the ⊕ premises, ⊖P rems the ⊖ premises, and BP rems the blank premises of A_{add}. Moreover, let T = L_{open} ◀ SUPPS_{L_{open}} be the task of A_{add}. P rems:=⊕P rems ∪ ⊖P rems ∪ BP rems, Concs:=⊕Concs ∪ ⊖Concs New-Lines:=⊕Concs ∪ ⊕P rems New-Supps:=(SUPPS_{L_{open}} ∪ ⊕Concs) − ⊖P rems. New-T asks:=[L ◀ New-Supps | L ∈ ⊕P rems].

If A⃗ is a sequence of actions and Â is an agenda that contains the task T of A_{add}, then the result (A⃗’, Â’, P’) of Φ(A⃗, Â, P, A_{add}) is defined by:

• A⃗’:= A⃗ ∪ [A_{add}].

• Â’:= { ; New-T asks ∪ (Â − [T])  if L_{open} ∈ ⊖Concs, [L_{open} ◀ New-Supps] ∪ New-T asks ∪ (Â − [T])  else.

• P’ results from P by

1. adding the proof lines New-Lines, respectively, and

2. justifying the proof lines ⊖Concs and ⊕Concs with the justification (M P rems), respectively, where M is the method of A_{add}.

The recursive extension Φ is called Φ⃗. Φ⃗ introduces a whole sequence of actions (the arrow of Φ⃗ indicates that this function introduces a sequence of actions A⃗_{add}).

Definition The recursive action introduction function Φ⃗ is a partial function that maps a sequence of actions, an agenda, a PDS, and a sequence of actions into a sequence of actions, an agenda, and a PDS, i.e.,

Φ⃗ : A⃗ × Â × P × A⃗_{add} ↦ A⃗’ × Â’ × P’.

Φ⃗ is recursively defined as follows: Let A⃗ be a sequence of actions, Â an agenda, P a PDS, and A⃗_{add} a sequence of actions.

1. If A⃗_{add} is empty then Φ⃗(A⃗, Â, P, A⃗_{add}) = (A⃗, Â, P).

2. Otherwise let A_{add} := first(A⃗_{add}) and A⃗’_{add} := rest(A⃗_{add}). If A_{add} is applicable with

respect to P, and if Â contains the task of A_{add}, then Φ⃗(A⃗, Â, P, A⃗_{add}) = Φ⃗(Φ(A⃗, Â, P, A_{add}), A⃗’_{add}).

With the function Φ⃗ we can now define proof plans and solution proof plans.

Definition Let (T hm, {Ass_{1}, …, Ass_{n}}, M, C) be a proof planning problem, P_{init} the initial PDS of this problem, and Â_{init} its initial agenda.

A proof plan for the proof planning problem is a triple PP = (A⃗, Â, P) with a sequence of actions A⃗, an agenda Â, and a PDS P such that:

1. the methods of each action of A⃗ are in M,

2. (A⃗, Â, P) = Φ⃗([], Â_{init}, P_{init}, A⃗),

A solution proof plan for the proof planning problem is a sequence of actions A⃗ such that Φ⃗([], Â_{init}, P_{init}, A⃗) has an empty agenda and a closed PDS.

Because of this definition, we can also say that Φ maps a proof plan and an action into a proof plan and that Φ⃗ maps a proof plan and a sequence of actions into a proof plan.

3.2 The PLAN Algorithm

Figure 8 gives a pseudo-code description of the PLAN algorithm. PLAN obtains as input a proof plan PP = (A⃗, Â, P), a history H⃗, a list of methods M, and a list of control rules C.^{12} PLAN generates a sequence of pairs of proof plans PP and histories H⃗. The user of Ωmega can start PLAN with the initial PDS, the initial agenda, and the set of methods and control rules of a proof planning problem. In order to reach the next proof plan and the next history PLAN performs a cycle of termination check, task selection, action selection and action introduction or action deletion. It terminates when either the agenda of the current proof plan is empty (see step 1 in Figure 8) or when there are neither further actions to be introduced nor actions to be removed (see step 5 in Figure 8). In the former case PLAN was successful and returns the proof plan and the constructed closed PDS. In the latter case, PLAN did traverse the complete search space without finding a proof plan and returns fail.

12Both methods M and control rules C are lists and not sets since the order in these lists are relevant.

The order in M gives a default order in which the methods are tried, when no control rules fire and determine a different order (see section 3.4). The order in C determines the order in which the control rules are evaluated.

Input: (1) a proof plan PP = (A⃗, Â, P) with a sequence of actions A⃗, an agenda Â, and a PDS P, (2) a history H⃗, (3) a list of methods M, (4) a list of control rules C.

Output: Either a solution proof plan and a closed PDS or fail.

Algorithm: PLAN((A⃗, Â, P),H⃗,M,C)

1. Termination If Â is empty, then terminate and return employ-CS (A⃗,P).

2. Task Selection Let current task T:= first(evalcrules-tasks (Â,C)) where T is the pair L_{open} ◀ SUPPS_{L_{open}}.

3. Action Selection Let (A_{add},A):=ChooseAction(T,H⃗,M,C) where A_{add} is an action and A is a set of alternative actions.

4. Action Introduction

If A_{add} is given

then (A⃗’,Â’,P’):=Φ(A⃗, Â, P, A_{add}). H⃗’:=add-action-intro-record(H⃗,Â,A_{add},A).

If extract-constraints(A_{add}) ≠ ∅

then pass-constraints (extract-constraints(A_{add})).

PLAN((A⃗’,Â’,P’),H⃗’,M,C).

5. Action Deletion

If A_{add} is not given

then

If A⃗ is empty then

Terminate and return fail. else

Let A_{reason}:=find-introducing-action(T,H⃗).

((A⃗’,Â’,P’),H⃗’):=Backtrack ((A⃗,Â,P),H⃗,[A_{reason}]).

PLAN((A⃗’,Â’,P’),H⃗’,M,C).

Figure 8: The PLAN algorithm.

If the current agenda is not empty, then PLAN first selects the next task to tackle (step 2 in Figure 8). To do so, PLAN employs the function evalcrules-tasks . evalcrules-tasks evaluates the control rules C of the kind ‘Tasks’ on the tasks list of the current agenda and returns a (possibly) changed alternative list.^{13} Then, PLAN picks the fist element of the resulting list as current task.

Next, PLAN employs the subalgorithm ChooseAction to compute an action (step 3 in Figure 8). ChooseAction is applied to the current task, the methods M, and the control rules C. It tries to compute admissible actions and – if successful – it selects one action and returns it. Since ChooseAction is a complex algorithm we shall discuss it in detail in section 3.4.

If ChooseAction returns an action, then PLAN introduces the action (step 4 in Figure 8). It creates a new proof plan by applying the action introduction function Φ to the current proof plan and the chosen action. Moreover, it creates a new history by adding a new action-introduction record entry to the history. PLAN uses the function extract-constraints to access the constraints of an action. When the action contains constraints for the connected external constraint solvers, then PLAN employs the function pass-constraints , which passes the constraints to the respective external system. PLAN does not check whether the new constraints are accepted by the respective external system. Rather, it assumes that corresponding consistency checks are performed by ChooseAction as part of the evaluation of the application conditions of a method, when an action is computed.

When ChooseAction fails to provide an action, then PLAN tries to delete actions in the current proof plan (step 5 in Figure 8). If the current sequence of actions is empty, then this is obviously not possible. When there are no more actions that can be introduced and the current sequence of actions is empty, then PLAN did traverse the complete search space (complete wrt. to the methods M and the control rules C) without finding a solution proof plan. In this case, PLAN terminates and returns fail. If there are actions that can be deleted, then PLAN employs the function find-introducing-action to determine the action whose introduction created the task T for which no action can be computed. The information about which action introduction did introduce which task can be found in the history in the action-introduction entries. Then, PLAN employs the subalgorithm Backtrack to perform the deletion of the selected action and all further actions that explicitly depend on it. Backtrack is applied to the current proof plan, the current history, and a list with the action to be deleted as only element. It returns a changed proof plan and a changed history. Since Backtrack is a complex algorithm we shall discuss it in detail in the next section.

When the agenda is empty, then the introduction of actions stops and PLAN applies the function employ-CS to the computed action sequence and the constructed PDS (step 1 in Figure 8). This function employs the external constraint solvers to compute instantiations for the meta-variables. Then, it substitutes all occurrences of the meta-variables in proof lines of the PDS and the actions by their instantiations, respectively. It returns the resulting action sequence and the instantiated PDS, which are then the output of PLAN.

Although proof planning actions are complex actions in the sense of HTN-planning, the expansion of actions is not performed within PLAN. Rather, there are separate procedures in Ωmega for the expansion of actions. When an expansion fails to produce a calculus-level proof and results in new open lines, then PLAN can be re-invoked on the new tasks.

13Although we do not explicitly provide the current proof plan and the current history as arguments for evalcrules-tasks , the predicates in the IF-part of the evaluated control rules can make use of this status information. This holds for all kinds of control rules, not only for the control rules of kind ‘Tasks’ evaluated here.

3.3 Deletion of Actions

Before we describe the Backtrack algorithm, we shall introduce the notion of dependency among actions and when an action is deletable. When an action is introduced into a proof plan, then it modifies the elements of the proof plan. Other actions introduced later on may depend on these modifications. More concretely, when the new lines introduced by an action are used as given lines by other actions introduced later on, then these actions depend on the preceding action. Afterwards, we define the function for the deletion of an action from a proof plan. Since action deletion is conceptually the inverse operation of action introduction we call this function Φ^{−1} although technically Φ^{−1} is not the inverse function of Φ.

Definition Let A⃗ be a sequence of actions with

A⃗=[A_{1}, …, A_{i−1}, A_{i}, A_{i+1}, …, A_{n}].

Let A_{i} be an action with the ⊕ conclusions ⊕Concs, and the ⊕ premises ⊕P rems. An action A_{j} ∈ {A_{i+1}, …, A_{n}} depends on A_{i}, if A_{j} is an action whose sets of conclusions or premises contains a proof line of ⊕Concs or ⊕P rems (which are the new proof lines introduced by A_{i}).

Definition Let A⃗ be a sequence of actions with

A⃗=[A_{1}, …, A_{i−1}, A_{del}, A_{i+1}, …, A_{n}].

A_{del} is deletable with respect to A⃗, if the set of actions in A⃗ that depend on A_{del} is empty.

In the following definition of the function Φ^{−1} we describe the modifications of the sequence of actions, the agenda, and the PDS caused by the deletion of an action. Although the notion of deletability of an action is defined only with respect to a sequence of actions, we demand in the definition of Φ^{−1} that the agenda and the PDS are not arbitrary ones, but created by this sequence of actions (in particular, by the action that should be deleted). The described modifications cannot be performed with respect to an arbitrary PDS or an arbitrary agenda.

Definition The action deletion function Φ^{−1} is a partial function that maps a sequence of actions, an agenda, a PDS, and an action into a sequence of actions, an agenda, and a PDS, i.e.,

Φ^{−1} : A⃗ × Â × P × A_{del} ↦ A⃗’ × Â’ × P’.

Let A_{del} be a deletable action in A⃗. Let ⊕Concs be the ⊕ conclusions, ⊖Concs the ⊖ conclusions, ⊕P rems the ⊕ premises, ⊖P rems the ⊖ premises, and BP rems the blank premises of A_{del}. Moreover, let T = L ◀ SUPPS_{L} be the task of A_{del}. Lines-T o-Remove:=⊕Concs ∪ ⊕P rems. T asks-T o-Remove:=[L ◀ SUPPS_{L} ∈ Â | L ∈ ⊕P rems]. New-T asks:=[T].

If Â is an agenda and P is a PDS that results from the introduction of A⃗ (to some agenda and some PDS), then the result (A⃗’, Â’, P’) of Φ^{−1}(A⃗, Â, P, A_{del}) is defined by:

• A⃗’:= A⃗ − [A_{del}].

• Â’:= New-T asks ∪ (Â − T asks-T o-Remove).

• P’ results from P by

1. removing the lines Lines-T o-Remove and

2. justifying the proof lines ⊖Concs with Open, respectively.

A pseudo-code description of the algorithm Backtrack is given in Figure 9. Backtrack is applied to a proof plan PP = (A⃗, Â, P), a history H⃗, and a list of actions A⃗_{del} that have to be deleted. Backtrack generates a sequence of pairs of proof plans PP and histories H⃗ by deleting successively the actions in A⃗_{del}. If an action in A⃗_{del} is not deletable, then it is necessary to delete further actions. Backtrack returns the proof plan and the history that result from the deletion of all necessary actions.

The first step in Backtrack is a check whether the list of actions that should be deleted is empty. If this is the case, Backtrack terminates and returns the current proof plan and the current history. Otherwise, it selects the first action A_{del} from the list (step 2 in Figure 9). If A_{del} is deletable, Backtrack deletes it from the current proof plan by employing Φ^{−1} and adds a new action-deletion entry to the history (step 3 in Figure 9). When A_{del} contains constraints, then Backtrack employs the function delete-constraints , which tells the respective constraint solvers to delete these constraints since they are not longer existing. Afterwards, Backtrack is applied to the changed proof plan, the changed history, and the remaining actions to be deleted.

If the action A_{del} is not deletable (step 4 in Figure 9), then Backtrack calls the function dependent-actions to compute the actions that depend from A_{del} and that have to be deleted in order to make A_{del} deletable. Backtrack is then recursively applied to the current proof plan, the current history, and the concatenation of the actions computed by dependent-actions and the current actions that have to be deleted.

As example for a situation, where an action is not deletable because other actions depend on it, consider the following situation. PLAN introduces an action A that reduces a task with goal L to two new tasks with goals L_{1} and L_{2}. Next, PLAN applies the action A_{1} to close L_{1}. Afterwards, PLAN fails to apply an action to the task with goal L_{2} and employs Backtrack to remove the action A that introduced L_{2}. However, the deletion of A would not only remove the line L_{2} but also the line L_{1} with respect to which action A_{1} was introduced. Hence, before A can be deleted the action A_{1} has to be deleted.

3.4 Action Computation and Selection

ChooseAction is the subalgorithm of PLAN that computes alternative lists of actions and selects one of them. Figure 10 shows a pseudo-code description of the algorithm.

Input: (1) a proof plan PP = (A⃗, Â, P) with a sequence of actions A⃗, an agenda Â, and a PDS P, (2) a history H⃗, (3) a sequence of actions A⃗_{del}.

Output: A proof plan PP’ = (A⃗’, Â’, P’) and a history H⃗’.

Algorithm: Backtrack((A⃗, Â, P),H⃗,A⃗_{del})

1. Termination If A⃗_{del} is empty, then terminate and return ((A⃗, Â, P), H⃗).

2. Pick Action Let A_{del}:=first(A⃗_{del}).

3. Action Deletion

If A_{del} is deletable wrt. A⃗

then (A⃗’,Â’,P’):=Φ^{−1}(A⃗, Â, P, A_{del}). H⃗’:=add-action-del-record (H⃗,Â,A_{del}).

If extract-constraints(A_{del}) ≠ ∅

then delete-constraints (extract-constraints(A_{del})).

Backtrack ((A⃗’,Â’,P’),H⃗’,rest(A⃗_{del})).

4. Deletion Expansion

If A_{del} is not deletable wrt. A⃗

then A⃗_{del}^{new}:=dependent-actions (A_{del}, A⃗). Backtrack ((A⃗,Â,P),H⃗,A⃗_{del}^{new} ∪ A⃗_{del}).

Figure 9: The Backtrack algorithm.

ChooseAction is applied to a task, the current history, and the lists of methods M and control rules C. If successful, ChooseAction returns a selected action and a set of alternative actions (see step 7 in Figure 10), otherwise it returns fail (see step 2 in Figure 10).

Input: (1) a task T, (2) a history H⃗, (3) a list of methods M, (4) a list of control rules C.

Output: Either a pair of an action and a list of actions or fail.

Algorithm: ChooseAction(T,H⃗,M,C) Let T =L_{open} ◀ SUPPS_{L_{open}}.

1. Order Methods Methods:= evalcrules-methods (M,C,T).

2. Select Method

If Methods empty

then

Terminate and return fail. else

M:=first(Methods).

Actions:=initial-action-set(T, M).

3. Match Goal Let ⊖Concs be the ⊖ conclusions of M. Actions:=match-goal (L_{open},⊖Concs,Actions). If Actions empty, then Methods:=rest(Methods), goto 2.

4. Select and Match Supports and Parameters Let ⊖P rems and BP rems be the ⊖ premises and blank premises of M. Let P arams be the parameter variables of M. Supps+P arams:=evalcrules-s+p (SUPPS_{L_{open}},C,T,M,Actions). Actions:= match-s+p (Supps+P arams,⊖P rems ∪ BP rems,

P arams,Actions).

If Actions empty, then Methods:=rest(Methods), goto 2.

5. Evaluate Application Conditions Actions:=eval-appl-conds (Actions,M). If Actions empty, then Methods:=rest(Methods), goto 2.

6. Outline Computations eval-outline-computations(Actions). complete-outline (Actions).

7. Select an Action Actions:=remove-backtracked (Actions,H⃗). Actions:=evalcrules-actions (Actions,C). If Actions = ∅

then

Methods:=rest(Methods), goto 2. else

Terminate and return (first(Actions),rest(Actions)).

Figure 10: The ChooseAction algorithm.

ChooseAction computes actions successively. It starts with an under-specified, initial action that contains only a chosen method and the given task. Then, it successively matches lines of the method with the goal and the supports of the task as well as variables specified in the declarations of the method with terms, positions, etc. The substitutions of these matchings refine successively the binding of the action such that more and more specified actions are created. In order to check whether a particular action of a method is valid, ChooseAction evaluates the application conditions of the method with respect to the binding of the action. Afterwards, it completes the binding of the actions by conducting the outline computations and by computing the new lines. Finally, it selects one action among the resulting fully specified actions.

In the following, we explain ChooseAction with the example 2.1 of section 2.4. We apply ChooseAction to the task L_{T hm} ◀ {L_{Ass_{1}}, L_{Ass_{2}}}, an empty history, a list of methods that contains =Subst-B, and a list of control rules that contains the control rule supps+params-=Subst whose impact is explained below.

The first step in ChooseAction is the re-ordering of the alternative list of methods. This is done by the function evalcrules-methods , which obtains as input M, C and the given task. evalcrules-methods evaluates the control rules in C of kind ‘Methods’ on M and returns a (possibly) changed list of alternative methods. From this list ChooseAction picks the first one (step 2 in Figure 10) and employs the function initial-action-set to create the initial set of actions that consists of one action whose premises, conclusions, bindings, and constraints are empty, whose method is the chosen method, and whose task is the given task.

For our example, we assume that evalcrules-methods returns the list [=Subst-B, …]. Then, ChooseAction chooses =Subst-B as method and produces an initial set of actions that contains only the following action:

Action

method =Subst-B
task  L_{T hm} ◀ {L_{Ass_{1}}, L_{Ass_{2}}}

premises conclusions binding constraints

The next step (step 3 in Figure 10) in ChooseAction matches the goal with the ⊖ conclusions of the selected method. To do so, ChooseAction employs the function match-goal . This function is applied to the goal, the ⊖ conclusions of the selected method, and the set of actions computed so far. Its computations and its output depend on the existence of ⊖ conclusions in the chosen method. If the method has no ⊖ conclusions (i.e., a forward method), then match-goal simply returns the list of actions it obtained as input. If the method has ⊖ conclusions (i.e., a backward method), then match-goal matches the goal with the ⊖ conclusions, respectively. For each successful matching it creates a new action whose binding contains the substitution resulting from the matching and whose conclusions contain the goal annotated with ⊖. Finally, match-goal returns the set of all new actions.

In our example the matching of the goal L_{T hm} with the ⊖ conclusions of =Subst-B results in a substitution with two elements: L_{3} ↦ L_{T hm} and f ↦ even(a + b). Thus, match-goal returns an actions set that contains only the following action:

Action

method =Subst-B
task  L_{T hm} ◀ {L_{Ass_{1}}, L_{Ass_{2}}}

premises

conclusions ⊖ L_{T hm}. L_{Ass_{1}}, L_{Ass_{2}} ⊢ even(a + b) (Open)
binding {L_{3} ↦ L_{T hm}, f ↦ even(a + b)}

constraints

Next, ChooseAction chooses supports and parameters and matches them with ⊖ and blank premises and the parameter variables of the selected method (step 4 in Figure 10). This results in further substitutions, which refine the actions computed so far. First, ChooseAction evaluates the control rules of the kind ‘Supps+Params’. This is done by the function evalcrules-s+p , which is applied to the supports of the goal, the control rules C, the task, the current method, and the actions computed so far. Control rules of the kind ‘Supps+Params’ do not only reorder and manipulate the support lines but they return a new type of elements, namely pairs of support lines and parameter instantiations. Thus, the parameter selection is not an isolated decision but is combined with the selection of support lines.^{14} Then, ChooseAction employs the function match-s+p . match-s+p obtains as input the pairs of support lines and parameter instantiations, the ⊖ and blank premises of the selected method, and the set of actions computed so far. With respect to each action computed so far (i.e., depending on the binding of an action computed so far) match-s+p matches the support lines and parameters pairs with the ⊖ and blank premises and the parameter variables of the method, respectively. For each successful matching it creates a new action whose binding is extended with the substitution resulting from the matching and whose premises comprise the matched support lines. Finally, match-s+p returns the set of new actions.

In our example, the control rule supps+params-=Subst fires and returns the two support lines and parameter instantiation pairs ({L_{Ass_{1}}}, < 1 1 >) and ({L_{Ass_{2}}}, < 1 2 >), where < 1 1 > is the parameter position of the a in the formula even(a + b) of the goal L_{T hm} and < 1 2 > is the parameter position of the b.^{15} For both pairs and with respect to the only action computed so far, match-s+p succeeds to match the premise L_{1} and the parameter pos of =Subst-B with the content of the pairs, respectively. It returns a set of actions that contains the following two elements:

14We decided for this combined approach since typically the parameter selection is directly related to the support line selection.

15The control rule supps+params-=Subst fires if the current method is =Subst-B and if there are some support lines that are equations such that one side of the equations equals a subterm in the formula of the goal. If supps+params-=Subst finds such a support line it returns a pair consisting of the support line and the respective subterm position in the formula of the goal.

Action

method =Subst-B
task L_{T hm} ◀ {L_{Ass_{1}}, L_{Ass_{2}}}
premises L_{Ass_{1}}. L_{Ass_{1}} ⊢ a=^{.}c (Hyp)
conclusions ⊖ L_{T hm}. L_{Ass_{1}}, L_{Ass_{2}} ⊢ even(a + b) (Open)
binding  \begin{matrix}\{L_{3} ↦ L_{T hm}, L_{1} → L_{Ass_{1}}, f ↦ even(a + b), α → ν, \\ t → a, t′ → c, pos →< 1 1 >\} \end{matrix}

constraints

Action

method =Subst-B
task L_{T hm} ◀ {L_{Ass_{1}}, L_{Ass_{2}}}
premises L_{Ass_{2}}. L_{Ass_{2}} ⊢ b=^{.}c (Hyp)
conclusions ⊖ L_{T hm}. L_{Ass_{1}}, L_{Ass_{2}} ⊢ even(a + b) (Open)
binding  \begin{matrix}\{L_{3} ↦ L_{T hm}, L_{1} → L_{Ass_{2}}, f ↦ even(a + b), α → ν, \\ t → b, t′ → c, pos →< 1 2 >\} \end{matrix}

constraints

The first action results from matching L_{1} and pos with L_{Ass_{1}} and < 1 1 >, respectively, whereas the second action results from matching L_{1} and pos with L_{Ass_{2}} and < 1 2 >, respectively.

In the next step (step 5 in Figure 10), ChooseAction evaluates the application conditions of the selected method. The evaluation of the application conditions is performed by the function eval-appl-conds , which obtains as input the actions computed so far and the selected method. For each given action eval-appl-conds evaluates the application conditions of the method with respect to the binding of the action. The evaluation of application conditions can create further substitutions, which are then added to the binding of the action. Moreover, the evaluation can create constraints for external constraint solvers, which are then added as constraints of the action. Each action for which the evaluation fails is rejected. eval-appl-conds returns the set of all actions for which the evaluation succeeds.

In our example, the application conditions of =Subst-B evaluate to true for both actions computed so far. Since no constraint results from the evaluation of the application conditions the constraints of both actions are set to the empty set.

Next, ChooseAction completes the actions by conducting the outline computations of the selected method and by computing the new outline lines (i.e., ⊕ premises and conclusions) (see step 6 in Figure 10). This is done by the functions eval-outline-computations and complete-outline , which both are applied to the set of actions computed so far. Both functions do not change the set of actions but they refine the actions already in the set. eval-outline-computations evaluates the outline computations for each action and adds the resulting substitutions to the binding of the action. Similarly, complete-outline computes the missing outline lines for each action and adds the corresponding substitutions to the binding of the action. New outline lines are justified as follows: ⊕ premises are justified with Open whereas new ⊕ conclusions are justified by an application of the selected method to the premises of the action.

For our example, eval-outline-computations and complete-outline complete the actions computed so far as follows:

Action

method =Subst-B
task  L_{T hm} ◀ {L_{Ass_{1}}, L_{Ass_{2}}}
premises \begin{matrix}⊕ L_{T hm′}. L_{Ass_{1}}, L_{Ass_{2}} ⊢ even(c + b) (Open) \\ L_{Ass_{1}}. L_{Ass_{1}} ⊢ a=^{.}c (Hyp) \end{matrix}
conclusions ⊖ L_{T hm}. L_{Ass_{1}}, L_{Ass_{2}} ⊢ even(a + b) (Open)
binding  \begin{matrix}\{L_{3} ↦ L_{T hm}, L_{1} → L_{Ass_{1}}, L_{2} → L_{T hm′}, f ↦ even(a + b), α → ν, \\ t → a, t′ → c, pos →< 1 1 >, f′ → even(c + b)\} \end{matrix}
constraints ∅

Action

method =Subst-B
task  L_{T hm} ◀ {L_{Ass_{1}}, L_{Ass_{2}}}
premises \begin{matrix}⊕ L_{T hm′}. L_{Ass_{1}}, L_{Ass_{2}} ⊢ even(a + c) (Open) \\ L_{Ass_{2}}. L_{Ass_{2}} ⊢ b=^{.}c (Hyp) \end{matrix}
conclusions ⊖ L_{T hm}. L_{Ass_{1}}, L_{Ass_{2}} ⊢ even(a + b) (Open)
binding  \begin{matrix}\{L_{3} ↦ L_{T hm}, L_{1} → L_{Ass_{2}}, L_{2} → L_{T hm′}, f ↦ even(a + b), α → ν, \\ t → b, t′ → c, pos →< 1 2 >, f′ → even(a + c)\} \end{matrix}
constraints ∅

Finally, ChooseAction decides for one of the computed actions (step 7 in Figure 10). First, it rejects all actions that correspond to actions that have already been backtracked. This is done by the function remove-backtracked , which is applied to the current set of actions and the given history. If an action has the same given lines and the same binding as an action that is stored in the history as deleted action, then this action is removed from the alternative list. To the remaining actions ChooseAction applies the function evalcrules-actions to evaluate the control rules of kind ‘Actions’. Provided the resulting list of actions is not empty, ChooseAction terminates and returns a pair consisting of the first element of the list of actions and the rest of the list of actions (i.e., the chosen action and the list of alternatives). If the list of actions is empty, then ChooseAction returns to the method selection point (step 2 in Figure 10) and repeats the sequence of matchings, application condition evaluation, outline computations evaluation, and outline completion for the next method of the method list. Similarly, ChooseAction returns to the method selection point and selects the next method, when the set of actions becomes empty during the matchings or by the evaluation of the application conditions. If ChooseAction fails to compute an action that does not correspond to a backtracked action and is not rejected by the control rules, then it terminates and returns fail (see step 2 in Figure 10).

3.5 Example

In the following, we shall explain the application of PLAN to a problem from the limit domain. Theorems of the limit domain make statements about the limit lim_{x→a} f(x) of a function f at a point a, about the limit limseq X of a sequence X, about the continuity of a function f at a point a, and about the derivative of a function f at a point a. The standard definitions of limit, continuity, and derivative comprise so-called ϵ–δ criterions, i.e., proofs of such theorems postulate the existence of a δ such that a conjecture of the form … |X| < ϵ is proved under assumptions of the form … |Y | < δ. For instance, the definition of lim in λ-notation is:

lim ≡ λf λa λl ∀ϵ (0 < ϵ ⇒ ∃δ (0 < δ∧∀x (|x−a| > 0∧|x−a| < δ ⇒ |f(x)−l| < ϵ)))

An example theorem from the limit domain is LIM+ that states that the limit of the sum of two functions f and g equals the sum of their limits; that is, if lim_{x→a} f(x) = l_{1} and lim_{x→a} g(x) = l_{2} then lim_{x→a}(f(x) + g(x)) = l_{1} + l_{2}. When the definition of lim_{x→a} is expanded, the corresponding planning problem consists of two assumptions

∀ϵ_{1} (0 < ϵ_{1} ⇒ ∃δ_{1} (0 < δ_{1} ∧ ∀x_{1} (|x_{1} − a| > 0 ∧ |x_{1} − a| < δ_{1} ⇒ |f(x_{1}) − l_{1}| < ϵ_{1}))) and

∀ϵ_{2} (0 < ϵ_{2} ⇒ ∃δ_{2} (0 < δ_{2} ∧ ∀x_{2} (|x_{2} − a| > 0 ∧ |x_{2} − a| < δ_{2} ⇒ |g(x_{2}) − l_{2}| < ϵ_{2}))).

And the theorem becomes

∀ϵ (0 < ϵ ⇒ ∃δ (0 < δ ∧ ∀x (|x − a| > 0 ∧ |x − a| < δ ⇒ |(f(x) + g(x)) − (l_{1} + l_{2})| < ϵ))).

Similar theorems in this class are LIM- and LIM* for the difference and the product of limits of functions. Moreover, there are corresponding theorems about continuity. Continuous+ states that the sum of two continuous functions is continuous, and Continuous- and Continuous* make similar statements for the difference and product of continuous functions.

When proving a limit theorem like LIM+, a δ has to be constructed that depends on an ϵ such that certain estimations hold. This is a non-trivial task for students as well as for traditional automated theorem provers.^{16} The typical way a mathematician discovers a suitable δ is by incrementally restricting the possible values of δ. When proof planning limit theorems, PLAN adapts this approach by cooperating with the constraint solver CoSIE: (in)equality tasks that are simple enough for CoSIE (i.e., tasks that are in the input language for CoSIE) are passed to CoSIE and CoSIE provides suitable instantiations for δ, when solutions for meta-variables are computed and inserted into the final proof plan.

For finding ϵ-δ-proofs, among others, the general methods ∃I-B, ∃E-F, ∀I-B, ∀E-F, ∧I-B, ∧E-F, ⇒I-B, ⇒E-F, SetFocus-B, and =Subst-B and the domain-specific methods TellCS-B, TellCS-F, AskCS-B, ComplexEstimate-B, Solve*-B, Simplify-B, and Simplify-F are required. We introduced ComplexEstimate-B, AskCS-B, TellCS-B, TellCS-F, ∀I-B, and ∃E-F already in section 2.6; =Subst-B is explained already in section 2.3. Similar to ∀I-B and ∃E-F also ∃I-B, ∀E-F, ∧I-B, ∧E-F, ⇒I-B, and ⇒E-F apply certain natural deduction rules. Actions of ∃I-B perform a backward ∃_{I} step. They close a goal with formula ∃x P [x] and introduce a task whose goal has the formula P [mv] in which x is replaced by a new meta-variable mv. Similarly, actions of ∀E-F perform a forward ∀_{E} step and derive a new support P [mv] with a new meta-variable mv from a given support ∀x P [x]. Actions of ∧I-B perform a backward ∧_{I} step and reduce a task whose goal has the formula A_{1} ∧ A_{2} to new tasks whose goals have the formulas A_{1} and A_{2}. Actions of ∧E-F perform the corresponding forward ∧_{E} decompositions on conjunctive support lines. Actions of ⇒I-B perform a backward ⇒_{I} step and reduce a task with goal A ⇒ B to a new task whose goal has the formula B and A as additional hypothesis. Moreover, A becomes the formula of a new support for this task. Actions of ⇒E-F perform an ⇒_{E} step. When applied to a task with goal C and an support with formula A ⇒ B they introduce two new tasks: a task with goal C, which contains also a new support with B as formula, and a task with goal A. Actions of the Solve*-B method exploit transitivity of <, >, ≤, ≥ and reduce a goal with formula a_{1} < b_{1} to a new task with formula b_{2}σ ≤ b_{1}σ in case a support a_{2} < b_{2} exists and a_{1}, a_{2} can be unified by the substitution σ. Then, also a further new task is created whose formula is the conjunction of all mappings of the substitution σ (compare description of method ComplexEstimate-B in section 2.6). Simplify-B passes the goal of a given task to the computer algebra system Maple and asks Maple to simplify it. If Maple succeeds, then the given task is reduced to a new task with the simplified formula. The analogous method Simplify-F derives a support with a simpler formula from a given support by calling Maple. Actions of SetFocus-B highlight a subformula in a support.

16Bledsoe proposed in 1990 several versions of LIM+ as a challenge problem for automated theorem proving [7]. The simplest versions of LIM+ (problem 1 and 2 in [7]) are at the edge of the capabilities of traditional automated theorem provers but LIM* is certainly beyond their capabilities.

When applied to an ϵ–δ–problem, PLAN first decomposes the initial task with a complex formula into subtasks whose formulas are (in)equalities. This is done by actions that decompose formulas in tasks, e.g., actions of the methods ∧I-B, ∀I-B, ∃I-B etc.

When faced with an inequality goal, PLAN first tries to apply the methods TellCS-B and AskCS-B, which both employ CoSIE. TellCS-Bpasses the goal to CoSIE, whereas AskCS-Basks CoSIE whether the goal is entailed by its current constraints. If an inequality is too complex to be handled by CoSIE, then PLAN tries to apply methods that reduce an inequality to simpler inequalities. So, PLAN successively produces simpler inequalities, until it reaches inequalities that are accepted by CoSIE. This approach – handle with CoSIE or simplify – is guided by the control rule prove-inequality given in Figure 3 in section 2.5, which is the central control rule to accomplish ϵ-δ-proofs with PLAN. In its IF-part prove-inequality checks whether the current goal is an inequality. If this is the case, it prefers the methods TellCS-B, TellCS-F, AskCS-B, Simplify-B, Simplify-F, Solve*-B, ComplexEstimate-B, and SetFocus-B in this order.

In order to apply methods such as ComplexEstimate-B and Solve*-B unwrapping of (in)equality supports from the initial assumptions is necessary. This is realized as follows: First, PLAN applies SetFocus-B to highlight a promising subformula in a support (the application of SetFocus-B is suggested by prove-inequality if no other method is applicable, promising subformulas are chosen by another control rule guiding the supports and parameters choice point). Next, the highlighted subformula is unwrapped by actions that decompose supports, e.g., actions of the methods ∧E-F, ∀E-F, ∃E-F etc.

Finally, when no task is left and PLAN invokes the function employ-CS , CoSIE computes instantiations for the meta-variables that are consistent with the collected constraints.

Next, we briefly discuss the application of PLAN to the LIM+ problem.^{17} PLAN first decomposes the initial theorem to tasks with the formulas 0 < mv_{δ} and |(f(c_{x}) + g(c_{x})) − (l_{1} + l_{2})| < c_{ϵ} where mv_{δ} is a meta-variable introduced for δ and c_{x} and c_{ϵ} are constants that replace x and ϵ, respectively. Moreover, the assumptions 0 < c_{ϵ}, |c_{x} − a| > 0, and |c_{x} − a| < mv_{δ} are created during the decomposition of the initial theorem and become supports of the new tasks. 0 < mv_{δ} can be passed directly to CoSIE by an action of TellCS-B. |(f(c_{x})+g(c_{x}))−(l_{1}+l_{2})| < c_{ϵ} cannot be passed to CoSIE directly. This triggers the decomposition of one of the two initial assumptions. If the initial assumption on f is decomposed, then PLAN obtains as new supports 0 < c_{δ_{1}} and |f(mv_{x_{1}}) − l_{1}| < mv_{ϵ_{1}}. Now PLAN can compute and introduce an action of ComplexEstimate-B using the latter new support line. During the evaluation of the application conditions of ComplexEstimate-B the substitution mv_{x_{1}} ↦ c_{x} is created and the computer algebra system Maple computes a decomposition (f(c_{x})+g(c_{x}))−(l_{1} +l_{2}) = 1∗(f(c_{x})−l_{1})+(g(c_{x})+l_{2}) (that is, the variables k and l of ComplexEstimate-B are bound to 1 and g(c_{x}) − l_{2}, respectively). Thus, the action of ComplexEstimate-B introduces new tasks with formulas mv_{ϵ_{1}} < \frac{c_{ϵ}}{2∗mv}, |1| ≤ mv, 0 < mv, |g(c_{x}) − l_{2}| < \frac{c_{ϵ}}{2} , and mv_{x_{1}} =^{.}c_{x}. The formulas of the former three tasks and of the last one can all be passed directly to CoSIE by actions of TellCS-B. To deal with the remaining task with formula |g(c_{x}) − l_{2}| < \frac{c_{ϵ}}{2} PLAN decomposes the second initial assumption (on g) and derives new support lines with formulas 0 < c_{δ_{2}} and |g(mv_{x_{2}}) − l_{2}| < mv_{ϵ_{2}}. An action of Solve*-B reduces the goal with respect to the second new support to two new tasks with formulas mv_{ϵ_{2}} ≤ \frac{c_{ϵ}}{2} and mv_{x_{2}} =^{.}c_{x}. Both tasks are closed by actions of TellCS-B and their formulas are passed to CoSIE.

17A detailed description on how Multi solves this problem is given in section 4.5.

The decomposition of the initial assumptions results not only in the used support lines but also in tasks with the formulas 0 < mv_{ϵ_{1}}, |mv_{x_{1}} − a| > 0, |mv_{x_{1}} − a| < c_{δ_{1}} from the assumption on f and the analogue tasks from the assumption on g. The task 0 < mv_{ϵ_{1}} is closed by the introduction of an action of TellCS-B, which passes the formula to CoSIE. To close the other tasks PLAN introduces actions of the method Solve*-B that use the supports with formulas |c_{x} − a| < mv_{δ} and |c_{x} − a| > 0 (from the decomposition of the initial goal). The application of Solve*-B to the task |mv_{x_{1}} − a| < c_{δ_{1}} and the support |c_{x} − a| < mv_{δ} results in two new tasks with formulas mv_{δ} ≤ c_{δ_{1}} and mv_{x_{1}} =^{.}c_{x}. The application of Solve*-B to the task |mv_{x_{1}} − a| > 0 and the support |c_{x} − a| > 0 results also in two new tasks with formulas 0 ≤ 0 and mv_{x_{1}} =^{.}c_{x}. Whereas 0 ≤ 0 is closed by an actions of AskCS-B the other three tasks are closed by actions of TellCS-B, which pass their formulas to CoSIE. The corresponding tasks from the assumption on g are handled in the same way. Thereby the constraints mv_{δ} ≤ c_{δ_{2}}, mv_{x_{2}} =^{.}c_{x}, and mv_{x_{2}} =^{.}c_{x} are passed to CoSIE. Moreover, some actions of the TellCS-F method during the planning process pass constraints in support lines to CoSIE: 0 < c_{δ_{1}}, 0 < c_{δ_{2}}, 0 < c_{ϵ}.

After propagating constraints, CoSIE has the final constraint store in Figure 11. When asked for suitable instantiations for the meta-variables, CoSIE provides the bindings mv_{x_{1}} ↦ c_{x}, mv_{x_{2}} ↦ c_{x}, mv ↦ 1, mv_{ϵ_{1}} ↦ \frac{c_{ϵ}}{2} , mv_{ϵ_{2}} ↦ \frac{c_{ϵ}}{2} , and mv_{δ} ↦ min(c_{δ_{1}}, c_{δ_{2}}). These instantiations computed by CoSIE are exactly the solutions that standard textbooks use for δ, ϵ_{1}, and ϵ_{2} for LIM+.

PLAN can successfully plan all the challenge problems of Bledsoe [7], i.e., the limit theorems LIM+, LIM-, LIM*, the theorems Continuous+, Continuous−, Continuous*, lim_{x→a} x = a, lim_{x→a} c = c, and the theorem that the composition of continuous functions is again continuous.

mv_{x_{1}} = c_{x}
mv_{x_{2}} = c_{x}
0 < c_{δ_{1}} < +∞
0 < c_{δ_{2}} < +∞
0 < c_{ϵ}  < +∞
0 < mv_{ϵ_{1}} ≤ \frac{c_{ϵ}}{2} , \frac{c_{ϵ}}{2∗mv}
0 < mv_{ϵ_{2}} ≤ \frac{c_{ϵ}}{2}
0 < mv_{δ} ≤ c_{δ_{1}}, c_{δ_{2}}
1 ≤ mv ≤ \frac{c_{ϵ}}{2∗mv_{ϵ_{1}}}

Figure 11: The final constraint store of CoSIE for LIM+.

4 Proof Planning with Multiple Strategies

Proof planning with multiple strategies decomposes the previous monolithic proof planning process and replaces it by separated parameterized algorithms as well as different instances of these algorithms, so-called strategies. The strategies, which specify different behaviors of the algorithms, are the basic elements for proof construction in multiple-strategy proof planning. That is, the goal of multiple-strategy proof planning is to compute a sequence of strategy applications that derives a given theorem from a given set of assumptions. The decision on when to apply a strategy is not encoded once and forever into the system but rather is determined by meta-level reasoning using heuristic control knowledge of strategies and their combination.

In the following, we first introduce in section 4.1 the basic concepts of proof planning with multiple strategies and illustrate them with examples. Then, we describe in section 4.2 Multi’s blackboard architecture. Section 4.3 discusses the reasoning at the strategy-level with strategic control rules. We conclude with an informal description of all algorithms currently employed by Multi that are not exemplified in section 4.1.

4.1 Algorithms, Strategies, and Tasks

Algorithms

Multi enables the incorporation of heterogeneous, parameterized algorithms for different kinds of proof plan refinements and modifications. Currently, Multi employs the following algorithms (technical descriptions of these algorithms, i.e., of the plan refinements or modifications they perform, are given in section 5):

PPlanner refines a proof plan by introducing new actions.

InstMeta refines a proof plan by instantiating meta-variables.

BackTrack modifies a proof plan by removing refinements of other algorithms.

Exp refines a proof plan by expanding complex steps.

ATPrefines a proof plan by solving subproblems with traditional machine-oriented automated theorem provers.

CPlanner refines a proof plan by transferring steps from a source proof plan or fragment.

The decomposition of PLAN allows to extend and generalize the functionalities of its subcomponents. This results in the independent and parameterized algorithms PPlanner, InstMeta, and BackTrack for action introduction, meta-variable instantiation, and backtracking. Exp, ATP, and CPlanner integrate new refinements of the proof plan.

Strategies

Instances of these algorithms can be specified in different strategies. Technically, a strategy is a condition-action pair. The condition part states when the strategy is applicable. The action part consists of a modification or refinement algorithm and an instantiation of its parameters. Similar to the knowledge of the applicability of methods we separate the legal and heuristic knowledge of the applicability of strategies. The condition part of a strategy states the legal conditions that have to be satisfied in order for the strategy to be applicable, whereas strategic control rules reason about the heuristic utility of the application of strategies.

To execute or to apply a strategy means to apply its algorithm to the current proof planning state with respect to the parameter instantiation specified by the strategy. For instance, the parameters of PPlanner are a set of methods, a list of control rules, a termination condition, and an action selection procedure. When Multi executes a PPlanner strategy, the PPlanner algorithm introduces only actions that use the methods specified in the strategy. The actions are computed and selected by the action selection procedure (e.g., ChooseAction or ChooseActionAll ) specified by the strategy. The action selection procedures evaluate then the control rules specified by the strategy during the computation of actions. The application of the strategy terminates, when its termination condition is satisfied. Hence, different strategies of PPlanner provide a means to structure the method and control rule knowledge. Both algorithms, InstMeta and BackTrack, have one parameter. The parameter of InstMeta is a function that determines how the instantiation for a meta-variable is computed. If Multi applies a InstMeta strategy with respect to a metavariable mv, and if the computation function of the strategy yields a term t for mv, then InstMeta substitutes mv by t in the proof plan. The parameter of BackTrack is a function that computes a set of refinement steps of other algorithms that have to be deleted. When Multi applies a BackTrack strategy, then BackTrack removes all refinement steps that are computed by the function of the strategy as well as all steps that depend from these steps.

Notation Strategies are denoted in the sans serif font (e.g., NormalizeLineTask, UnwrapHyp).

Tasks

Multi extends the task concept of PLAN. Since Multi employs further kinds of tasks, the tasks used in PLAN (i.e., a pair consisting of an open line and its supports) are called line-tasks in Multi. Multi uses also instantiation-tasks and expansion-tasks. The introduction of a meta-variable into the plan results in an instantiation-task, that is, the task to instantiate this meta-variable. Similarly, the introduction of a method or tactic step into the PDS, which is constructed during the proof planning process, results in an expansion-task, that is, the task to expand this step. An instantiation-task stores the meta-variable for which an instantiation has to be constructed. The instantiation task for meta-variable mv is written as mv|^{Inst}. An expansion-task consists of a proof line L in the PDS, which is justified with a method or a tactic application. The expansion-task with line L is written as L|^{Exp}. Multi stores all used kinds of tasks in an agenda.

Different tasks can be tackled by different algorithms and strategies. For instance, since strategies of InstMeta introduce instantiations for meta-variables they can tackle instantiation-tasks. Expis the suitable choice to deal with expansion-tasks, whereas strategies of PPlanner or ATPcan tackle line-tasks. A strategy checks in its condition part whether it is applicable to a particular task. That is, the condition of a strategy is a predicate on tasks. To apply a strategy to a task means to execute the strategy with respect to the task.

The algorithms and kinds of tasks currently employed by Multi have been derived from the case studies. However, the Multi framework is envisaged to be extended by further algorithms and further kinds of tasks, if needed.

Example Strategies

In the following, we describe some strategies needed to accomplish ϵ-δ-proofs (see section 3.5). The methods and control rules for ϵ-δ-proofs are structured into the three strategies NormalizeLineTask, UnwrapHyp, and SolveInequality. All three strategies are instantiations of PPlanner. A more detailed description of the application of these strategies and their cooperation when accomplishing ϵ-δ-proofs is given in section 4.5.

The strategy SolveInequality (see Table 2) is applicable to prove line-tasks whose formulas are inequalities or whose formulas can be reduced to inequalities. It comprises methods such as ComplexEstimate-B, TellCS-B, TellCS-F, AskCS-B, and Solve*-B (see section 3.5). Its list of control rules contains prove-inequality and eager-instantiate. Possible actions are computed and selected with the ChooseAction procedure. The strategy terminates, when there are no further line-tasks whose formulas are inequalities or whose formulas can be reduced to inequalities. Note that it is the parameterization of PPlanner that makes SolveInequality appropriate to tackle line-tasks whose formulas are inequalities as stated in the condition part of the strategy.

Strategy: SolveInequality

Condition inequality-task

Action

Algorithm  PPlanner
Action Procedure ChooseAction
Methods  ComplexEstimate-B, TellCS-B,

TellCS-F, Solve*-B, AskCS-B …

                 C-Rules  prove-inequality, eager-instantiate,

…

Termination  no-inequalities

Table 2: The SolveInequality strategy.

NormalizeLineTask (see Table 3) is used to decompose line-tasks whose goals are complex formulas with logical connectives and quantifiers. Typical methods in NormalizeLineTask are ∧I-B and ∀I-B (see section 3.5). NormalizeLineTask employs the ChooseAction procedure for the action computation and selection and terminates, when all complex line-tasks are decomposed to literal line-tasks.

Strategy: NormalizeLineTask

Condition complex-line-task

Action

Algorithm  PPlanner
Action Procedure ChooseAction
Methods  ∀I-B, ∃I-B, ∧I-B,
…

C-Rules

Termination  literal-line-tasks-only

Table 3: The NormalizeLineTask strategy.

The aim of UnwrapHyp (see Table 4) is to unwrap a focused subformula of an assumption in order to make it available for proving a line-task. The list of its methods includes, for instance, ∀E-F and ∧E-F. The control rule tackle-focus determines that, if UnwrapHyp is applied, then the actions of the available methods can be used only if they use a support in their premises that carries a focus and when their conclusions do not tackle the focused subformula. For instance, if a line-task has the supports B_{1} ∧ B_{2} and A_{1} ∧ (A_{2} ∧ focus(A_{3} ∧ A_{4})), then only actions of ∧E-F that use the second support with the focus are allowed. The introduction of two actions of ∧E-F derive the new support focus(A_{3} ∧A_{4}) to which no further action of ∧E-F can be applied since it would decompose the focused subformula. Similar to NormalizeLineTask and SolveInequality, UnwrapHyp uses the ChooseAction algorithm. It terminates as soon as all focused formulas are unwrapped.

Strategy: UnwrapHyp

Condition focus-in-subformula

Action

Algorithm  PPlanner
Action Procedure ChooseAction
Methods  ∀E-F, ∃E-F, ∧E-F, …

                        C-Rules  tackle-focus

Termination  focus-at-top

Table 4: The UnwrapHyp strategy.

In order to instantiate meta-variables that occur in constraints collected by CoSIE, we implemented the two InstMeta strategies InstIfDetermined and ComputeInstFromCS (see Table 5). InstIfDetermined is applicable only, if CoSIE states that a meta-variable is already determined by the constraints collected so far. Then, the computation function connects to CoSIE and receives this unique instantiation for the meta-variable. ComputeInstFromCS is applicable to all meta-variables for which constraints are stored in CoSIE. The computation function of this strategy requests from CoSIE to compute an instantiation for a metavariable that is consistent with all constraints collected so far.

The dependency-directed backtracking described in section 3.3 is realized as the strategy BackTrackActionToTask (see Table 6) of the BackTrack algorithm. BackTrackActionToTask Strategy: InstIfDetermined

Condition determined-in-cs

Action

Algorithm InstMeta Function get-determined-instantiation

Strategy: ComputeInstFromCS

Condition mv-in-cs

Action

Algorithm InstMeta Function compute-consistent-instantiation

Table 5: The InstMeta strategies InstIfDetermined and ComputeInstFromCS.

instantiates the BackTrack algorithm with the function step-to-line-task, which computes the action that introduced a line-task. BackTrackActionToTask is applicable to each line-task.

Strategy: BackTrackActionToTask

Condition line-task

Action

Algorithm BackTrack Function step-to-line-task

Table 6: The BackTrackActionToTask strategy.

4.2 Multi ’s Blackboard Architecture

When we designed proof planning with multiple strategies, we aimed at a system that allows for the flexible cooperation of independent components for proof plan refinement and modification, guided by meta-reasoning. For the implementation we decided to use a blackboard architecture because this is an established means to organize the cooperation of independent components for solving a complex problem.

The fundamental ideas of the blackboard model [18] are (1) the segmentation of the knowledge base into modules that are kept separate and independent and (2) the separation of the inference engines that work on that knowledge. Each knowledge module can employ its own inference engine. The communication between the modules is limited to reading and writing in a common working memory, the blackboard. The blackboard can be further structured into regions that, for instance, contain different data structures. A basic blackboard architecture consists of a structured blackboard and the modular inference engine/knowledge base pairs which are called the knowledge sources.

The objective of each knowledge source is to contribute to the solution of the problem whose problem-solving state data are kept on the global blackboard. Control of knowledge source activation in blackboard systems is data-directed and event-driven. That is, the activation of the next knowledge source is determined by the changes of the data on the blackboard caused by other knowledge sources, rather than by explicit calls from other knowledge sources or some central sequencing mechanism. Knowledge sources check whether they are applicable with respect to the current solution state on the blackboard and indicate their applicability. Control modules choose the next knowledge source based

Figure 12: Multi’s blackboard architecture.

on the solution state and on the existence of knowledge sources capable of improving the current state of the solution. As a result, blackboard systems do not rely on a pre-defined control of the application of the involved components but provide the flexibility to employ their knowledge sources opportunistically.

In the following, we give an informal overview on the Multi system and the ideas behind it. A detailed technical description of the algorithms and concepts as well as a formal definition of strategic proof planning with Multi are given in the next section.

Multi’s architecture is displayed in Figure 12. In this figure dashed arrows indicate information flow whereas solid arrows indicate that a knowledge source changes the content of the respective blackboard. Multi’s architecture is similar to the Hearsay-III [19] and the BB1 [26] blackboard systems in that it employs two blackboards, the so-called proof blackboard and the control blackboard.

We decided for a two-blackboard architecture to emphasize the importance of both the solution of the proof planning problem whose status is stored on the proof blackboard and the solution of the control problem, that is, which possible strategy should the system perform next. The proof blackboard contains the current strategic proof plan, which consists of a sequence of actions, an agenda, a PDS, and a sequence of binding stores, which store the collected instantiations of meta-variables, as well as the strategic history. The control blackboard contains three repositories to store information relevant for the control problem: job offers, demands, and a memory.

Corresponding to the two blackboards, there are also two sets of knowledge sources shown in Figure 12 that work on these blackboards. The strategies are the knowledge sources that work on the proof blackboard. A strategy can change the proof blackboard by refining or modifying the agenda, the PDS, the history of strategies, and bindings of the meta-variables. The strategy component contains all the strategies that can be used. If a strategy’s condition part is satisfied with respect to a certain task in the agenda, then the strategy posts its applicability with respect to this task as a job offer onto the control blackboard. Technically, a job offer is a pair (S, T) with a strategy S and a task T, which signs that T satisfies the condition of S. That is, in the terminology of blackboard systems, a task that satisfies the condition of a strategy is the event that triggers the strategy. The MetaReasoner is the knowledge source working on the control blackboard. It evaluates strategic control knowledge represented by strategic control rules in order to rank the job offers. The architecture contains a scheduler that checks the control blackboard, for its highest ranked job offer. Then, it executes the strategy of the job offer with respect to the task specified in the job offer. In a nutshell, Multi operates according to the cycle in Figure 13, which passes the following steps:

Job Offer Strategies whose condition is true put a job offer onto the control blackboard.

Guidance The MetaReasoner evaluates the strategic control rules to order the job offers on the control blackboard.

Invocation A scheduler invokes the strategy who posed the highest ranked job offer.

Execution The algorithm of the invoked strategy is executed with respect to the parameter instantiation specified by the strategy.

Figure 13: Cycle of Multi.

Demands and the Memory

The choice of a job offer can depend on particular demand information issued by strategies onto the control blackboard and the content of the memory. An executed strategy can reason on whether it should interrupt. This can be sensible if the strategy is stuck or if it turns out that it should not proceed before another strategy is executed. Then, the execution of a strategy interrupts itself, places demands for other strategies onto the control blackboard, and stores a pair consisting of its execution status and the demands it posed in the memory. Interrupted executions of a strategy stored in the memory place job offers for their re-invocation onto the control blackboard. A job offer from the memory consists just of a pointer to the memory entry that posed this job offer. If such a job offer is scheduled, the interrupted strategy execution is re-invoked from the memory.

By posing demands and interrupting strategies particularly desired cooperations between strategies can be realized. For instance, in order to enable a flexible instantiation of meta-variables during the proof planning process (as opposed to PLAN’s approach) the InstMeta strategy InstIfDetermined and the PPlanner strategy SolveInequality have to cooperate. This cooperation works as follows: The strategy SolveInequality contains the control rule eager-instantiate. If evaluated during an execution of SolveInequality, this control rule checks whether InstIfDetermined is applicable for an occurring meta-variable. If this is the case, it causes the interruption^{18} of the execution of the SolveInequality strategy and poses the demand that InstIfDetermined should be applied with respect to the instantiationtask of the meta-variable. The status of the interrupted SolveInequality strategy is stored in the memory from where it can be reinvoked as soon as the posed demand is satisfied by the corresponding application of InstIfDetermined.

Binding Stores

Multi allows to reason on existing meta-variables and possible instantiations for them. An equation of the form mv_{α}:=^{b} t_{α} where mv_{α} is a meta-variable and t_{α} is a term of the same type α is called a binding. t is called the instantiation of the binding for mv. During the strategic proof planning process the current set of bindings is stored in a so-called binding store.

New bindings are not applied to existing proof lines in the constructed PDS or to proof lines in existing actions. Since the application of the bindings would replace occurrences of the meta-variables by occurrences of their current instantiations, it would not be possible to backtrack binding decisions in order to bind meta-variables differently (since the information on which subterms of the proof lines have been which meta-variables would have been lost). Rather, the current bindings are applied to copies of proof lines as soon as these are used. For instance, if a line-task has the task formula |mv_{x} −c| < c_{δ} and the current binding store contains the binding mv_{x}:=^{b} c, then PPlanner applies the current binding to a copy of the task formula (see section 5.5.2 for details). The resulting formula, namely |c − c| < c_{δ}, is then used in the action computation process instead of |mv_{x} −c| < c_{δ}. Methods can become applicable wrt. the instantiated formula whereas they are not applicable wrt. the original formula with the meta-variables. For our example, a method for arithmetic simplifications becomes applicable and can reduce the formula |c − c| < c_{δ} to 0 < c_{δ} which is not possible for |mv_{x} − c| < c_{δ}. However, this step depends on the binding of mv_{x}; if this binding is removed (by backtracking the step that introduced the binding), then this step is not valid anymore.

Multi constructs a sequence of binding stores in order to keep track of the dependencies between the changing bindings and the introduced actions. The introduction of a new binding creates a new binding store in the sequence. All following steps are performed with respect to this current binding store. When bindings are removed, then the binding store before the introduction of this binding is restored and all following binding stores are removed from the sequence. Moreover, all actions that potentially depend on the removed binding stores are deleted as well (for details see section 5.5.7 where backtracking in Multi is described). We extended the notion of an action in proof planning for Multi (see section 5.2). Actions have an additional slot binding-store in order to store a pointer to the binding store that was the current one when the action was computed.

18Interruption is an explicit choice point in the PPlanner algorithm, see section 5.5.2.

Notation In the remainder of the report, the following symbols (maybe labeled with some subscripts or superscripts) are associated with the following objects:

BS denotes a binding store,
B⃗S denotes a sequence of binding stores.

4.3 Reasoning at the Strategy-Level

In the Multi system, no order or combination of refinements or modifications on the proof blackboard is pre-defined. The choice of strategy applications results from metareasoning at the strategy-level that is conducted by the MetaReasoner, which evaluates the strategic control rules on the job offers on the control blackboard. Strategic control rules are formulated in the same control rule language as control rules on tasks, methods, supports and parameters, and actions (see section 2.5). They can reason about all information stored on the control blackboard and the proof blackboard (i.e., about the proof plan constructed so far and the plan process history) as well as about the mathematical domain of the proof planning problem.

The advantage of this knowledge-based control approach is that the control of Multi can be easily extended and changed by modifying the strategic control rules. In contrast, when the combination of integrated components of a system is hard-coded into a control procedure, then each extension or change requires reimplementation of parts of the main control procedure. Moreover, the strategic control rules declaratively represent the heuristical control knowledge of how to combine the strategies of Multi, so that this knowledge can be communicated to the user.

In the following, we shall discuss five strategic control rules, which are the backbone of the strategic control in Multi.

The use of demands and the memory for the goal-directed cooperation of strategies is re-

alized by the strategic control rules prefer-demand-satisfying-offers, prefer-memory-
offers, and defer-memory-offers given in Figure 14. The rule prefer-demand-sat-

isfying-offers states that, if a job offer on the control blackboard satisfies a demand on the control blackboard, then this job offer is preferred. Similarly, prefer-memory-offers states that, if there is a job offer from an interrupted strategy execution in the memory and all demands of this strategy execution are already satisfied, then this job offer should be preferred. defer-memory-offers defers job offers from interrupted strategy executions, if they have still unsatisfied demands.

   The rules prefer-backtrack-if-failure and reject-applied-offers in Figure 15

realize a basic failure reasoning and the rejection of already applied strategies. The purpose of the prefer-backtrack-if-failure rule is to integrate backtracking with strategies of PPlanner. When a PPlanner strategy runs into a failure, that is, it encounters a line-task for which it finds no applicable action, then it interrupts and stores the status of its execution in the memory. prefer-backtrack-if-failure causes backtrack-

            (control-rule prefer-demand-satisfying-offers
                          (kind strategic)
                          (IF (job-offer-satisfies-demand JO))
                          (THEN (prefer JO)))
            (control-rule prefer-memory-offers
                          (kind strategic)
                          (IF (and (job-offer-from-memory JO)
                                   (no-further-demands JO)))
                          (THEN (prefer JO)))
            (control-rule defer-memory-offers
                          (kind strategic)
                          (IF (and (job-offer-from-memory JO)
                                   (further-demands JO)))
                          (THEN (defer JO)))

Figure 14: The three strategic control rules prefer-demand-satisfying-offers,

prefer-memory-offers, and defer-memory-offers.

      (control-rule reject-applied-offers
                    (kind strategic)
                    (IF (job-offer-already-applied JO))
                    (THEN (reject JO)))
      (control-rule prefer-backtrack-if-failure
                    (kind strategic)
                    (IF (and (algorithm-of-last-strategy-is PPlanner)
                            (last-strategy-failure-on-line-task T)
                            (backtrack-job-offer-on JO T)))
                    (THEN (prefer JO)))

Figure 15: The strategic control rules reject-applied-offers and prefer-back

-track-if-failure.

ing by preferring a job offer of the BackTrackActionToTask strategy with the line-task on which the execution of the PPlanner strategy failed. Afterwards, the interrupted strategy execution can be re-invoked on the changed proof blackboard. The idea behind reject-applied-offers is that a strategy that failed on a task should not be tried again on this task (although it is still applicable to the task, and, thus, it places a job offer onto the control blackboard). reject-applied-offers checks whether a job offer corresponds to a strategy execution that has already been tried but was backtracked later on. In this case, reject-applied-offers rejects the job offer.

The priority^{19} of these control rules increases in the following order: prefer-demand-

satisfying-offers, prefer-memory-offers, defer-memory-offers, reject-applied-

offers, prefer-backtrack-if-failure. Although these control rules are the backbone of Multi’s control, they realize only a default behavior and can be excluded by the user of Multi or can be overridden by other strategic control rules with higher priority.

4.4 Further Algorithms

The strategies PPlanner, InstMeta, and BackTrack are introduced and exemplified in section 4.1. Here we shall informally introduce the other three algorithms used in Multi, namely Exp, ATP, and CPlanner. Formal descriptions of all algorithms can be found in section 5.5.

Exp

The algorithm Exptackles expansion-tasks. An expansion-task does not refer directly to an introduced action but contains a proof line in the constructed PDS whose justification is a complex step, that is, a method or a tactic application. For a proof line L with an abstract justification (J P_{1} … P_{n}) where J is a method or a tactic and P_{1}, …, P_{n} are the premises, Expcomputes a proof segment, which derives L from P_{1}, …, P_{n} at a lower level of abstraction. If J is a method, then Exp computes the proof segment by instantiating the proof schema of J. If J is a tactic, then Exp evaluates the expansion function of J. Afterwards, Expadds the new proof lines into the constructed PDS and adds a new justification to L at a lower level of abstraction.

Currently, the algorithm Exp is not parameterized. Since we distinguish technically between a strategy and its algorithm we have implemented the strategy ExpS as the only strategy for the Expalgorithm. The application condition of ExpS states that this strategy is applicable to all expansion-tasks.

ATP

The algorithm ATPenables the application of automated theorem provers within Multi in order to prove line-tasks. Its parameters are two functions for the application of an automated theorem prover (or several ones) and the check whether the obtained output is accepted as a proof. The first function obtains as input the line-task to which the ATP strategy is applied and returns the output of the employed ATP(s). The second function obtains the output of the ATPs and returns either true or false where true means that the function accepts the output as proof.

When a strategy of ATPsucceeds for a line-task L_{open} ◀ SUPPS_{L_{open}}, then ATPcloses the line L_{open} by the application of the tactic atp to the premises SUPPS_{L_{open}}. Moreover, the output obtained from the application function of the strategy becomes the parameter of the justification. Whether this tactic application can be expanded depends on the accepted output. Currently, the expansion function of atp can deal with the following outputs:

19The MetaReasoner evaluates first the strategic control rules with lower priority. Since they are evaluated later on, the strategic control rules with higher priority cause the final changes of the alternative list of job offers.

• Resolution proofs from the provers Otter [31], Bliksem [16], Spass [63], Pro-TeIn [5], and equational proofs produced by the provers eqp [32] and WaldMeister [27]. On these outputs the expansion function of atp calls Tramp [33], a proof transformation system that transforms resolution-style proofs into assertion level NDproofs to be integrated into the PDS.

• ND-proofs produced by Tramp, if Tramp is used as prover and not as transformation system (see below), and — with little transformational effort — ND-proofs provided by the higher-order prover tps [3] (see [6] on what kind of transformations are necessary to incorporate tps proofs into a PDS).

Other output of automated theorem provers can be accepted by the respective strategies of ATPbut cannot be further processed currently by the expansion function of the atp tactic.

Strategy: CallTramp

Condition first-order-problem

Action

ATP Apply employ-tramp-on-task ATP Output Check check-assertion-proof

Table 7: The CallTramp strategy.

As example of a strategy of ATPconsider CallTramp, which is depicted in Table 7. The application condition of CallTramp, first-order-problem, is satisfied by line-tasks, whose formulas are first-order. The application function, employ-tramp-on-task, employs Tramp not as transformation module but as prover. This is possible since Tramp cannot only transform the output of the connected provers but can also call these provers on a problem. When employed in this mode, Tramp obtains a problem formalization, calls the connected automated theorem provers on the problem, and returns — if one of the connected provers succeeds — an assertion-level ND-proof. The output check function of CallTramp, check-assertion-proof , checks whether the output provided by Tramp is an ND-proof of the task.^{20}

CPlanner

Case-based reasoning is the approach to tackle new problems or subproblems by adapting given solutions or parts of given solutions of other problems or subproblems [10]. Case-based reasoning components for Ωmega were first developed as stand-alone systems not directly intertwined with the proof planner or other components. The last system developed in this paradigm was the Topal system [61, 46].

Topal obtains as input a source proof plan and a target problem. It successively transfers method applications from the source proof plan into a proof plan of the target problem. To do so, it computes and maintains possible mappings from objects of the source proof plan (e.g., tasks and proof lines) to corresponding objects of the target proof plan. With these mappings it computes new actions for the target proof plan from actions in the source proof plan. Topal processes the given source proof plan chronologically which means that Topal selects the actions to transfer in the order of the source proof plan.

20check-assertion-proof checks only whether the returned object is a proof tree whose root is the goal of the task and whose leaves are the supports of the task. It does not check whether each justification is correct since this would demand to expand the assertion-level proof.

The CPlanner algorithm in Multi extends Topal in several ways. First, CPlanner is parameterized and enables the realization of different kinds of case-based reasoning. For instance, we realized a task-directed approach as an alternative to the chronological Topal approach. This task-directed approach, which is encoded in the CPlanner strategy TaskDirectedAnalogy (see Table 8), first selects a task in the target proof plan and then selects an action to transfer in the source proof plan depending on the selected task. Second, CPlanner allows not only for the transfer of method applications but also for the transfer of strategy applications from a strategic source proof plan into a strategic target proof plan. Moreover, the integration of CPlanner into Multi enables the flexible combination of case-based reasoning with the other algorithms in Multi.

The parameters of CPlanner are a list of so-called action transfer procedures, a list of control rules, and a termination condition. Action transfer procedures describe how source actions are transfered into target actions. The control rules guide the selection of action transfer procedures and interrupts. The termination condition specifies when the execution of the strategy terminates.

Technically, an action transfer procedure is a triple of a list of choice points, a list of instantiation functions, and a computation function. The choice points specify which objects have to be selected during the transfer process, the instantiation functions provide the alternative lists for the choice points, respectively, and the computation function computes either a new target action or a new demand for a tuple of selected objects. When the computation function provides a new target action, then CPlanner introduces this action into the proof plan under construction. A demand causes CPlanner to interrupt with this demand (see section 5.5.3 for details).

For instance, T askMeth is an action transfer procedure that realizes a task-directed transfer of source actions. T askMeth specifies the choice points target task, source action, target premises, and target parameters in this order. That is, it first selects the task in the target problem to tackle and then selects the action to transfer in the source problem depending on this task. Finally, it chooses the target premises and target parameters depending on the selected target task and the selected source action. The computation function of T askMeth obtains the chosen objects as input and computes a new action of the method of the source action.

T askInst is an action transfer procedure for applications of InstMeta strategies. It first chooses an instantiation-task in the target plan. Next, it chooses an application of an InstMeta strategy in the source plan. Then, its computation function creates the demand to tackle the instantiation-task with the InstMeta strategy of the source action.

T askP P lanner is an action transfer procedure for applications of PPlanner strategies. It first chooses a line-task in the target proof plan and next an application of a PPlanner strategy in the source plan. The application of a PPlanner strategy essentially consists of a sequence of method actions (see section 5.2 for details). T askP P lanner reduces the transfer of the selected PPlanner strategy application to the transfer of the corresponding method action sequence. That is, it creates a demand for the recursive application of the CPlanner strategy TaskDirectedAnalogy with respect to the selected task and with the sequence of method actions as source actions.

The action transfer procedures T askMeth, T askInst, and T askP P lanner are combined in the CPlanner strategy TaskDirectedAnalogy, which is given in Table 8, in order to realize the task-directed transfer approach. The application condition of TaskDirectedAnalogy, always-true-line+inst, is satisfied by all line- and instantiation-tasks. The list of control rules is empty. The termination condition, no-local-tasks , is satisfied, when the initial task to which the strategy is applied and all tasks derived from this task are closed.

Strategy: TaskDirectedAnalogy

Condition always-true-line+inst

Action

Action Trans. Procs. T askMeth, T askP P lanner, T askInst
C-Rules  ∅
Termination  no-local-tasks
Source Actions  (free)

Table 8: The TaskDirectedAnalogy strategy

The applicability of TaskDirectedAnalogy is primarily not restricted by its condition part always-true-line+inst, but by its additional parameter, source actions, which is not a parameter of the algorithm CPlanner. Such additional parameters of strategies are called free parameters. They are not instantiated once and forever in the strategy. Rather, strategic control rules can suggest instantiations for a free parameter during the proof planning attempt.^{21} A strategy with free parameters is applied only if a strategic control rule instantiates the free parameters.

The free parameter of TaskDirectedAnalogy, source actions, has to be instantiated by a strategic control rule with the sequence of source actions that the strategy should transfer.^{22} A strategic control rule can choose, for instance, a complete source proof plan from a database of solved problems or it can choose a subsequence of actions of a given source proof plan. Instead of using actions of another problem (so-called external analogy) a strategic control rule can also suggest a subsequence of actions of the proof plan under construction to be transfered to another part of the same proof plan (so-called internal analogy).

Examples and a detailed discussion of case-based reasoning in Multi can be found in [55].

4.5 Example

To accomplish ϵ-δ-proof plans Multi combines the PPlanner strategies NormalizeLineTask, UnwrapHyp, and SolveInequality and the InstMeta strategies InstIfDetermined and Compute-InstFromCS (see section 4.1), which interface CoSIE. In the following, we illustrate with the LIM+ example (introduced in section 3.5) how Multi employs these strategies. However, before we elaborate the examples we discuss the employed strategies and their cooperation.

21Technically, strategies with free parameters post job offers, when their condition is satisfied and strategic control rules can then instantiate the free parameters by attaching instantiations to the job offer.

22The instantiation functions of the action transfer procedures look up the given source actions during the execution of the strategy and suggest then alternatives depending on these actions.

4.5.1 The Strategies and Their Cooperation

The strategy SolveInequality (see Table 2 in section 4.1) is central for accomplishing ϵ-δ-proofs with Multi. It is applicable to prove line-tasks whose goals are inequalities or whose goals can be reduced to inequalities. A goal is reducible to inequalities if it contains defined terms whose unfolding will result in inequalities, for instance, lim, limseq, cont, and deriv. SolveInequality unfolds occurrences of these concepts both in the goal and in the supports of the task. The method for unfolding defined concepts in goals is DefnUnfold-B, whereas DefnUnfold-F unfolds defined concepts in supports. The central idea of SolveInequality to tackle inequality goals is similar to the approach of PLAN when accomplishing ϵ-δ-proofs (see section 3.5): pass to CoSIE or simplify. Hence, also similar to PLAN’s approach, the control rule prove-inequality given in Figure 3 in section 2.5 is central in SolveInequality.

SolveInequality comprises the knowledge of how to deal with inequalities and with problems that can be reduced to inequalities. As opposed thereto, the strategies Normalize-LineTask and UnwrapHyp comprise the domain-independent, general knowledge of how to decompose complex formulas with logical connectives and quantifiers. SolveInequality decides once for the decomposition of a complex goal or the unwrapping of a subformula from a complex support. Then, it switches to NormalizeLineTask or UnwrapHyp, which perform all single decomposition steps. This saves SolveInequality from reasoning permanently on the application of methods that decompose single logical connectives and quantifiers such as ∧I-B or ∧E-F.

Technically, the cooperation between SolveInequality and NormalizeLineTask and UnwrapHyp works as follows. For line-tasks whose goals are complex formulas that contain inequality subformulas (e.g., goals that arise from unfolding lim, limseq, cont, or deriv) SolveInequality interrupts and places a demand for the strategy NormalizeLineTask on the control blackboard. Guided by this demand, Multi invokes NormalizeLineTask, which decomposes the complex goal. When re-invoked by Multi, SolveInequality can tackle the inequalities in the resulting goals. The switch from SolveInequality to UnwrapHyp is driven by missing support inequalities, which are needed for the application of the methods ComplexEstimate-B and Solve*-B. If the other methods preferred by prove-inequality fail, then the application of SetFocus-B highlights a subformula in an existing support. Afterwards, SolveInequality interrupts and places a demand for the invocation of UnwrapHyp to unwrap the highlighted subformula. When the subformula is unwrapped, SolveInequality can continue with a new support that may enable further steps. The application of SetFocus-B (i.e., the selection of the support and the subformula to highlight) is guided by the control rule choose-unwrap-support for the supports and parameters choice point. choose-unwrap-support analyzes the supports of the task on which the other methods are not applicable. It searches for inequality subformulas in the supports that are similar to the goal of the task. The idea is that similar formulas are likely to unify with the goal such that ComplexEstimate-B and Solve*-B become applicable.

To accomplish ϵ-δ-proofs plans also two InstMeta strategies, namely ComputeInstFromCS and InstIfDetermined, are used that interface the constraint solver CoSIE. Whereas InstIfDetermined asks CoSIE for instantiations of meta-variables that are already determined by the collected constraints, ComputeInstFromCS asks CoSIE to compute instantiations for the occurring meta-variables that are consistent with the collected constraints.

The invocation of ComputeInstFromCS is delayed by the strategic control rule delay-ComputeInstCosie until all line-tasks are closed. This delay of the computation of instantiations for meta-variables is sensible, since the instantiations should not be computed before all constraints are collected, that is, not before all line-tasks are closed. However, when the current constraints already determine a meta-variable, then a further delay of the corresponding instantiation is not necessary. Rather, immediate instantiations of determined meta-variables can simplify a problem (e.g., see [35]).

To enable the flexible instantiation of determined meta-variables SolveInequality cooperates with the strategy InstIfDetermined. Technically, this works as follows. When CoSIE signals that a meta-variable is determined, then the control rule eager-instantiate in SolveInequality fires. It interrupts SolveInequality and places a demand for InstIfDetermined with respect to the determined meta-variable. After the introduction of a binding for the meta-variable by InstIfDetermined Multi re-invokes SolveInequality.

4.5.2 The LIM+ Example with Multi

The LIM+ problem states that the limit of the sum of two functions f and g equals the sum of their limits. That is, the problem states that

LIM+: lim_{x→a}(f(x) + g(x)) = l_{f} + l_{g}

follows from Lim_{f}: lim_{x→a} f(x) = l_{f}
and Lim_{g}: lim_{x→a} g(x) = l_{g}.

Figure 16 and Figure 17 show the interesting parts, i.e., the parts created by SolveInequality, of the resulting PDS. We indicate the contributions of NormalizeLineTask and UnwrapHyp by justifications in the PDS such as (UnwrapHyp L_{3}) in line L_{49}, which abbreviate the proof segments created by these strategies. The complete PDS is given in appendix B. Note that we describe the proof planning process in progress. Hence, we introduce metavariables, when they arise. When there is a binding for a meta-variable during the proof planning process, then the proof lines created after the introduction of the binding use the instantiation of the meta-variable in order to clarify the following computations.

The proof planning process starts with the invocation of SolveInequality on the initial task LIM+ ◀ {Lim_{f}, Lim_{g}}. SolveInequality first unfolds the occurrences of lim. Afterwards, it switches to NormalizeLineTask, which decomposes the resulting complex goal in line L_{1} into the goals |(f(c_{x}) + g(c_{x})) − (l_{f} + l_{g})| < c_{ϵ} in L_{12} and 0 < mv_{δ} in L_{8} where c_{ϵ} and c_{x} are constants introduced for the universally quantified variables ϵ and x in L_{1} and mv_{δ} is a meta-variable introduced for the existentially quantified variable δ.

Both new goals are inequalities and SolveInequality tackles them guided by the control rule prove-inequality. It closes 0 < mv_{δ} directly by an application of TellCS-B, which passes the formula to CoSIE. |(f(c_{x}) + g(c_{x})) − (l_{f} + l_{g})| < c_{ϵ} is not accepted by CoSIE and therefore TellCS-B is not applicable. SolveInequality simplifies this goal to |((f(c_{x}) + g(c_{x})) − l_{f}) − l_{g}| < c_{ϵ} in line L_{16} but then fails to solve this goal with the given supports. choose-unwrap-support detects the subformula |f(x_{1}) − l_{f}| < ϵ_{1} of L_{2} as a promising support and guides the application of the method SetFocus-Bto highlight the subformula. This triggers the interruption of SolveInequality and the invocation of UnwrapHyp for this subformula. The application of UnwrapHyp yields the new support |f(mv_{x_{1}}) − l_{f}| < mv_{ϵ_{1}}

Lim_{f}. Lim_{f}  ⊢ lim_{x→a} f(x) = l_{f}  (Hyp)
Lim_{g}. Lim_{g} ⊢ lim_{x→a} g(x) = l_{g}  (Hyp)

L_{2}. Lim_{f} ⊢ ∀ϵ_{1} (0 < ϵ_{1} ⇒ ∃δ_{1} (0 < δ_{1} ∧ ; ∀x_{1} (|x_{1}−a| < δ_{1}∧|x_{1}−a| > 0 ; ⇒ |f(x_{1}) − l_{f}| < ϵ_{1}))) (DefnUnfold-F Lim_{f})

L_{3}. Lim_{g} ⊢ ∀ϵ_{2} (0 < ϵ_{2} ⇒ ∃δ_{2} (0 < δ_{2} ∧ ; ∀x_{2} (|x_{2}−a| < δ_{2}∧|x_{2}−a| > 0 ; ⇒ |g(x_{2}) − l_{g}| < ϵ_{2}))) (DefnUnfold-F Lim_{g})

L_{21}.  L_{21}  ⊢ 0 < c_{δ_{1}} ∧ ∀x_{1} (|x_{1} − a| < c_{δ_{1}} ∧ |x_{1} − ; a| > 0 ; ⇒ |f(x_{1}) − l_{f}| < mv_{ϵ_{1}}) (Hyp)
L_{42}.  L_{42}  ⊢ 0 < c_{δ_{2}} ∧ ∀x_{2} (|x_{2} − a| < c_{δ_{2}} ∧ |x_{2} − ; a| > 0 ; ⇒ |g(x_{2}) − l_{g}| < mv_{ϵ_{2}}) (Hyp)
L_{11}.  L_{11}  ⊢ |c_{x} − a| > 0 ∧ |c_{x} − a| < mv_{δ}  (Hyp)
L_{5}.  L_{5}  ⊢ 0 < c_{ϵ}  (Hyp)
L_{52}.  H_{2}  ⊢ mv_{x_{2}} =^{.}c_{x}  (TellCS-B)
L_{53}.  H_{2}  ⊢ mv_{ϵ_{2}} ≤ \frac{1}{2} ∗ c_{ϵ}  (TellCS-B)

L_{49}. H_{2} ⊢ |g(mv_{x_{2}}) − l_{g}| < mv_{ϵ_{2}} (UnwrapHyp L_{3})

L_{48}. H_{2} ⊢ |g(c_{x}) − l_{g}| < \frac{1}{2} ∗ c_{ϵ} (Solve*-B L_{49} L_{52} L_{53})

L_{37}. H_{1} ⊢ |g(c_{x}) − l_{g}| < \frac{1}{2} ∗ c_{ϵ} (UnwrapHyp

L_{3} L_{48} L_{39} L_{50} L_{51})

L_{31}.  H_{1}  ⊢ |1| ≤ mv  (TellCS-B)
L_{32}.  H_{1}  ⊢ mv_{ϵ_{1}} ≤ \frac{c_{ϵ}}{2∗mv}  (TellCS-B)

L_{33}. H_{1} ⊢ |g(c_{x}) − l_{g}| < \frac{c_{ϵ}}{2} (Simplify-B L_{37})

L_{34}.  H_{1}  ⊢ 0 < mv  (TellCS-B)
L_{35}.  H_{1}  ⊢ mv_{x_{1}} =^{.}c_{x}  (TellCS-B)

L_{28}. H_{1} ⊢ |f(mv_{x_{1}}) − l_{f}| < mv_{ϵ_{1}} (UnwrapHyp L_{2})

L_{27}.

H_{1} ⊢ |((f(c_{x}) + g(c_{x})) − l_{f}) − l_{g}| < c_{ϵ} (ComplexEstimate-B

L_{28} L_{31} L_{32} L_{33} L_{34} L_{35})

L_{16}. H_{3} ⊢ |((f(c_{x}) + g(c_{x})) − l_{f}) − l_{g}| < c_{ϵ} (UnwrapHyp

L_{2} L_{27} L_{18} L_{29} L_{30})

L_{12}. H_{3} ⊢ |(f(c_{x}) + g(c_{x})) − (l_{f} + l_{g})| < c_{ϵ} (Simplify-B L_{16})

L_{8}. H_{4} ⊢ 0 < mv_{δ} (TellCS-B)

L_{1}. Lim_{f} , Lim_{g}⊢ ∀ϵ (0 < ϵ ⇒ ∃δ (0 < δ ∧ ; ∀x (|x − a| < δ ∧ |x − a| > 0 ; ⇒ |(f(x) + g(x)) − (l_{f} + l_{g})| < ϵ))) (NormalizeLineTask L_{8} L_{12})

LIM+.

Lim_{f} , Lim_{g}⊢ lim_{x→a}(f(x) + g(x)) = l_{f} + l_{g}

(DefnUnfold-B L_{1})

H_{1} = {Lim_{f} , Lim_{g}, L_{5}, L_{11}, L_{21}}, H_{2} = {Lim_{f} , Lim_{g}, L_{5}, L_{11}, L_{21}, L_{42}} H_{3} = {Lim_{f} , Lim_{g}, L_{5}, L_{11}}, H_{4} = {Lim_{f} , Lim_{g}, L_{5}}

Figure 16: ϵ-δ-proof for LIM+ (part I).

in line L_{28}, but also the three new goals 0 < mv_{ϵ_{1}} in line L_{18}, |mv_{x_{1}} − a| < c_{δ_{1}} in L_{29}, and |mv_{x_{1}} − a| > 0 in L_{30}. Here UnwrapHyp introduces the constant c_{δ_{1}} for the existentially quantified variable δ_{1} and the meta-variables mv_{ϵ_{1}} and mv_{x_{1}} for the universally quantified variables ϵ_{1} and x_{1} in L_{2}.

When SolveInequality is re-invoked, it can apply ComplexEstimate-B to the goal |((f(c_{x}) + g(c_{x})) − l_{f}) − l_{g}| < c_{ϵ} and the new support |f(mv_{x_{1}}) − l_{f}| < mv_{ϵ_{1}}. This results in the five new goals |1| ≤ mv in L_{31}, mv_{ϵ_{1}} ≤ \frac{c_{ϵ}}{2∗mv} in L_{32}, |g(c_{x}) − l_{g}| < \frac{c_{ϵ}}{2} in L_{33}, 0 < mv in L_{34}, and mv_{x_{1}} =^{.}c_{x} in L_{35}. Except L_{33} all goals are closed by applications of TellCS-B, which pass the respective formulas as constraints to CoSIE. Since mv_{x_{1}} =^{.}c_{x} determines mv_{x_{1}} in CoSIE the control rule eager-instantiate fires and interrupts SolveInequality. Its demand causes Multi to invoke InstIfDetermined on the instantiation-task of mv_{x_{1}}. InstIfDetermined introduces the binding mv_{x_{1}}:=^{b} c_{x} into the strategic proof plan.

The re-invoked SolveInequality simplifies |g(c_{x}) − l_{g}| < \frac{c_{ϵ}}{2} to |g(c_{x}) − l_{g}| < \frac{1}{2} ∗ c_{ϵ} in L_{37} but then fails on this goal with the existing supports. choose-unwrap-support detects the subformula |g(x_{2}) − l_{g}| < ϵ_{2} of L_{3} as a promising support and guides the corresponding application of the method SetFocus-B to highlight this subformula. Afterwards, SolveInequality interrupts and Multi switches to UnwrapHyp, which unwraps the subformula and yields the new support |g(mv_{x_{2}}) − l_{g}| < mv_{ϵ_{2}} in line L_{49}. The unwrapping yields also the three new goals 0 < mv_{ϵ_{2}} in line L_{39}, |mv_{x_{2}} − a| < c_{δ_{2}} in L_{50}, and |mv_{x_{2}} − a| > 0 in L_{51}. UnwrapHyp introduces the constant c_{δ_{2}} for the existentially quantified variable δ_{2} and the meta-variables mv_{ϵ_{2}} and mv_{x_{2}} for the universally quantified variables ϵ_{2} and x_{2} in L_{3}.

When re-invoked, SolveInequality applies Solve*-B to the goal |g(c_{x}) − l_{g}| < \frac{1}{2} ∗ c_{ϵ} and the new support |g(mv_{x_{2}}) − l_{g}| < mv_{ϵ_{2}}. This results in the new goals mv_{x_{2}} =^{.}c_{x} in L_{52} and mv_{ϵ_{2}} ≤ \frac{1}{2} ∗ c_{ϵ} in L_{53}, which SolveInequality closes by TellCS-B. mv_{x_{2}} =^{.}c_{x} determines the meta-variable mv_{x_{2}} in CoSIE. Thus, the control rule eager-instantiate suggests a switch from SolveInequality to InstIfDetermined, which introduces the binding mv_{x_{2}}:=^{b} c_{x} into the strategic proof plan.

L_{18}.  H_{3}  ⊢ 0 < mv_{ϵ_{1}}  (TellCS-B)
L_{39}.  H_{3}  ⊢ 0 < mv_{ϵ_{2}}  (TellCS-B)
L_{11}.  L_{11}  ⊢ |c_{x} − a| > 0 ∧ |c_{x} − a| < mv_{δ}  (Hyp)
L_{14}.  L_{11}  ⊢ |c_{x} − a| > 0  (∧E-F L_{11})
L_{13}.  L_{11}  ⊢ |c_{x} − a| < mv_{δ}  (∧E-F L_{11})
L_{61}.  H_{1}  ⊢ 0 ≤ 0  (AskCS-B)
L_{59}.  H_{1}  ⊢ mv_{δ} ≤ c_{δ_{1}}  (TellCS-B)
L_{57}.  H_{2}  ⊢ 0 ≤ 0  (AskCS-B)
L_{55}.  H_{2}  ⊢ mv_{δ} ≤ c_{δ_{2}}  (TellCS-B)
L_{29}.  H_{1}  ⊢ |mv_{x_{1}} − a| < c_{δ_{1}}  (Solve*-B L_{13} L_{59})
L_{30}.  H_{1}  ⊢ |mv_{x_{1}} − a| > 0  (Solve*-B L_{14} L_{61})
L_{50}.  H_{2}  ⊢ |mv_{x_{2}} − a| < c_{δ_{2}}  (Solve*-B L_{13} L_{55})
L_{51}.  H_{2}  ⊢ |mv_{x_{2}} − a| > 0  (Solve*-B L_{14} L_{57})
H_{1} = {Lim_{f} , Lim_{g}, L_{5}, L_{11}, L_{21}}, H_{2} = {Lim_{f} , Lim_{g}, L_{5}, L_{11}, L_{21}, L_{42}}
H_{3} = {Lim_{f} , Lim_{g}, L_{5}, L_{11}}, H_{4} = {Lim_{f} , Lim_{g}, L_{5}}

Figure 17: ϵ-δ-proof for LIM+ (part II).

Afterwards, SolveInequality has to deal with the remaining goals L_{18}, L_{29}, L_{30}, and L_{39}, L_{50}, L_{51}, which resulted from the applications of the UnwrapHyp strategy. Figure 17 gives the PDS segment created by SolveInequality for these goals. It closes L_{18} and L_{39} directly by TellCS-B. The inequalities in the other goals cannot be passed to CoSIE directly because TellCS-B is not applicable to them. Instead, SolveInequality applies Solve*-B to these goals with supports that stem from the decomposition of the initial goal by NormalizeLineTask. The applications of Solve*-B result in inequality goals, which SolveInequality closes either with TellCS-B or AskCS-B.

After closing all line-tasks, SolveInequality terminates. Next, Multi invokes Compute-InstFromCS on the instantiation-tasks and CoSIE provides instantiations for the metavariables that are consistent with the collected constraints (see Figure 11 in section 3.5).

ComputeInstFromCS inserts these instantiations as the bindings

mv:=^{b} 1, mv_{ϵ_{1}}:=^{b} \frac{c_{ϵ}}{2} , mv_{ϵ_{2}}:=^{b} \frac{c_{ϵ}}{2} , and mv_{δ}:=^{b} min(c_{δ_{1}}, c_{δ_{2}})

into the strategic proof plan.

5 Formal Description of Multi

In the previous section, we explained the design of Multi and its basic concepts. In this section, we shall give a formal description of Multi.

Proof planning with multiple strategies computes strategic actions and introduces them into a strategic proof plan. A strategic action is the instantiation of a strategy pattern corresponding to method actions, which are instantiations of methods. Similar to proof plans in PLAN a strategic proof plan consists of a sequence of actions, an agenda, and a PDS. Strategic proof plans contain additionally a sequence of so-called binding stores to keep track of introduced meta-variable instantiations.

The structure of the section is as follows. First, we introduce some new data structures used by Multi. In section 5.2, we describe the different kinds of strategic actions in Multi. Afterwards, we formally describe strategic proof plans and give the operational semantics of strategic actions in section 5.3. Section 5.4 describes the strategic manipulation records, which Multi uses to construct a history. After the introduction of all necessary elements, we describe Multi’s main cycle and the modification and refinement algorithms integrated so far in section 5.5. We conclude this section with the discussion of some particular technical features of Multi in section 5.6.

5.1 New Data Structures

In this section, we discuss some new data structures used in Multi and their role during the strategic proof planning process.

Task Tags

In Multi, a strategy is executed with respect to a particular task (from the blackboard point of view we can say that the existence of the task triggers the invocation of the strategy). A particular execution of a strategy tackles then the task by which it was triggered rather than arbitrary tasks. This is easy to realize for the algorithms Exp, ATP, and InstMeta since these algorithms perform just one refinement step before they terminate. The situation is more complicated for the algorithms PPlanner and CPlanner since they may perform a sequence of proof plan modifications (e.g., introduce several actions) before they terminate or interrupt. When applied with respect to an initial task, these algorithm should tackle this task and tasks that are derived from it but they should ignore other tasks in the agenda. Moreover, if a strategy execution of CPlanner or PPlanner interrupts and other strategies are executed, then some of these strategies work on tasks created by the interrupted strategy some of them work on other tasks. When the initial strategy is re-invoked again, then it should tackle tasks derived from its own tasks but it should ignore other tasks created meanwhile. To organize this behavior a maintenance mechanism is needed, which keeps track of which tasks are relevant for which strategies.

In Multi, the desired behavior is supported by so-called task tags. When a strategy of CPlanner and PPlanner is invoked, then it creates a new task tag @_{T}, which uniquely refers to this execution of the strategy. The task tag is pinned to the task that triggered the strategy. When a proof plan modification in Multi reduces a task to some new tasks, then the new tasks inherit all tags from the initial one. An execution of a strategy of CPlanner or PPlanner considers only tasks that carry its tag. When the strategy execution terminates, then its tag is removed from all tasks. When a strategy execution interrupts and is reinvoked later on, then the re-invocation continues to work with the task tag created by the initial invocation.

If used in several not-terminated strategies, then one task can carry several tags. For instance, when an execution of a PPlanner strategy creates a task T, then T carries the tag of this execution. Afterwards, the execution interrupts and a different strategy is applied to T. Then, this second strategy execution creates a new tag, which is also pinned to T. All actions introduced by this second strategy execution inherit both tags of T. When the second strategy execution terminates and its tag is removed, then the resulting tasks carry still the tag of the first strategy execution. Thus, when the first strategy execution is re-invoked, it can continue to tackle these tasks.

Note that the task tags describe only which tasks can be tackled by a strategy execution. This does not mean that the other tasks are “invisible” or temporarily removed. Control rules evaluated by CPlanner and PPlanner can reason on all tasks of the current agenda.

Execution Messages

When a strategy execution stops, then its result and the reason why it stops are relevant information for Multi since Multi treats different kinds of termination differently (see section 5.5). Moreover, this information is important for the meta-reasoning with strategic control rules. Therefore, each strategy execution in Multi stops with a so-called execution message, which contains the available termination information. So far, Multi uses the following execution messages:

• A success message occurs when the strategy execution is successful on the given task.

• A failure message occurs when the strategy execution fails on the given task because of some problems (e.g., a strategy of PPlanner fails because there are no further applicable actions).

• An interruption message occurs when a strategy of CPlanner or PPlanner is interrupted.

The algorithms can attach further information to the execution messages, which can also be used by the strategic control rules. For instance, an algorithm can attach information on what kind of failure occurred to a failure message (see section 5.6.5).

Execution messages are stored in the history entries created by the strategy executions (see section 5.4). When which algorithm terminates with which execution message is described in detail in section 5.5. When a strategy execution terminates with a success message we also say that the application of the strategy was successful.

Demands and Memory Entries

For the algorithms CPlanner and PPlanner a strategy execution can interrupt. If this is the case, the strategy execution creates so-called demands and adds them to the demand repository on the control blackboard. Multi knows for the following demands:

• A demand S − ON − T, which specifies a strategy S and a task T, is called a strategytask-demand. This demand is satisfied by a successful application of the strategy S to the task T.

• A demand S − ON−?, which specifies a strategy S but no task, is called a strategydemand. This demand is satisfied by a successful application of the strategy S to any task.

• A demand ? − ON − T, which specifies a task T but no strategy, is called a taskdemand. This demand is satisfied by a successful application of any strategy to the task T.

An interrupted strategy execution writes also an entry into the memory repository on the control blackboard. A memory entry is a pair (@_{T} , {P_{D_{1}}, …, P_{D_{n}}}) of a task tag @_{T} and a set of pointers {P_{D_{1}}, …, P_{D_{n}}} to the demands of the interrupted strategy execution in the demands repository. Multi uses the @_{T} to re-invoke the strategy execution later on (see section 5.5.2 for details). Moreover, it makes use of the pointers to check whether the demands of the interrupted strategy are satisfied such that the strategy execution can be re-invoked again (see section 5.5.1 for details).

5.2 Strategic Actions

PLAN computes and introduces actions into a proof plan. An action is an instantiation of a method, which is a pattern of a proof step (see section 2.4). To extend this approach of action computation and introduction to strategic proof planning there is a strategic pattern associated with each algorithm in Multi (except BackTrack). The application of a strategy computes an instantiation of the pattern of its algorithm, a so-called strategic action, and introduces it into the strategic proof plan.

In this section, we shall describe the strategic actions created by PPlanner, InstMeta, Exp, ATP, and CPlanner. The algorithm BackTrack does not create actions but deletes actions of other algorithms. Note that, henceforth, we call instantiations of methods method actions in order to distinguish them from the different strategic actions, which we call PPlanner actions, InstMeta actions, Expactions, ATPactions, and CPlanner actions.

Technically, strategic actions are implemented as frame data structures. Each strategic action has the slots strategy, task, and binding-store. The strategy of an action and the task of an action are pointers to the strategy and the task with respect to which the action was computed. The binding store of an action is a pointer to the binding store, which was the current binding store, when the action was computed. Depending on the algorithm the different strategic actions have also further slots.

PPlanner and CPlanner

The algorithms PPlanner and CPlanner successively introduce actions into a strategic proof plan, PPlanner with respect to a given set of methods and control rules, CPlanner with respect to a given plan or a given plan fragment. Thus, actions of PPlanner and CPlanner are essentially abstractions of the sequence of actions introduced by the respective algorithm. The sequence of introduced actions is stored in the slot action-sequence of a PPlanner or CPlanner action.

Executions of PPlanner and CPlanner strategies can interrupt and can be re-invoked later on. Thus, one execution can consist of several periods. PPlanner and CPlanner create a strategic action for each period of the same strategy execution. Each of these actions contains the initial task to which the strategy was applied in the task slot. In its action-sequence slot each action contains only those actions that were introduced during the corresponding execution period. Note that the information stored in the strategic actions is not sufficient to identify actions that belong to the same strategy execution. For that purpose also information stored in the corresponding history entries is needed (see section 5.4 for details on the history entries).

PPlanner Action

strategy  NormalizeLineTask
task  L_{T hm}. L_{Ass_{1}}, L_{Ass_{2}} ⊢ ∃x (0 < x ∧ F [x]) (open) ◀ {L_{Ass_{1}}, L_{Ass_{2}}}

binding store

BS

action-sequence

[A∃I-B, A∧I-B, …]

Figure 18: A strategic action of PPlanner.

An example for an action of PPlanner is given in Figure 18. The strategic action results from the application of the strategy NormalizeLineTask to the line-task

L_{T hm}. L_{Ass_{1}}, L_{Ass_{2}} ⊢ ∃x (0 < x ∧ F [x]) (open) ◀ {L_{Ass_{1}}, L_{Ass_{2}}}.

First, PPlanner applies the method ∃I-B to the initial task. Then, it applies the method ∧I-B to the resulting task with task-formula 0 < mv_{x} ∧ F [mv_{x}]. If F [mv_{x}] is again a complex formula, then PPlanner can perform further actions in order to decompose F [mv_{x}]. The sequence of actions performed by PPlanner, [A∃I-B, A∧I-B, …], is stored in the slot action-sequence of the strategic action.

ATP

The algorithm ATPemploys external automated theorem provers to prove line-tasks. If the automated theorem prover succeeds, then the ATPalgorithm closes the goal of the line-task and creates a strategic action and stores the output of the external system in the slot output.

An example for an action of ATPis given in Figure 19. The strategy CallTramp is applied to the (trivial) problem to show that P ⇒ P holds. The problem is passed to Tramp, which provides as output the ND-proof given in the output slot of the action.

ATPAction

strategy CallTramp
task  L.∅ ⊢ P ⇒ P (open) ◀ ∅

binding store

BS
output  \begin{matrix}L_{1}. & L_{1} ⊢ & P & (Hyp) \\ L_{2}. & L_{1} ⊢ & P & (W eaken) \\ L. & ∅ ⊢ & P ⇒ P & (⇒_{I} L_{2}) \end{matrix}

Figure 19: A strategic action of ATP.

Exp

The algorithm Expexpands complex steps, i.e., method or tactic steps in the constructed PDS. For a proof line L with justification (J P_{1} … P_{n}), where J is a method or a tactic and P_{1}, …, P_{n} are the premises, Expcomputes a proof segment that derives the conclusion L of the step from its premises P_{1}, …, P_{n} at a lower level of abstraction. This proof segment is stored in the slot expansion-segment of an action of Exp. Moreover, an Expaction contains the slot open-lines, which contains the set of new open lines that are introduced in the expansion-segment.^{23}

An example is given in Figure 20. This Expaction results from the expansion of the justification (=Subst-B L_{T hm′} L_{Ass_{1}}) of proof line L_{T hm} (compare with example 2.1 in section 2.4). When this step is expanded, then the proof schema of the method =Subst-B (see section 2.3) is instantiated in order to derive L_{T hm} from the premises L_{T hm′} and L_{Ass_{1}} as given in the expansion-segment in Figure 20.

ExpAction

strategy  Exp
task  L_{T hm}. L_{Ass_{1}}, L_{Ass_{2}} ⊢ even(a + b) (=Subst-B L_{T hm′} L_{Ass_{1}})|^{Exp}

binding store

BS

expansion- segment

\begin{matrix}L_{Ass_{1}}. & L_{Ass_{1}} ⊢ & a=^{.}c & (Hyp) \\ L_{T hm′}. & L_{Ass_{1}} , L_{Ass_{2}} ⊢ & even(c + b) & (Open) \\ L_{1}. & L_{Ass_{1}} , L_{Ass_{2}} ⊢ & ∀P P (c) ⇒ P (a) & (≡_{E} L_{Ass_{1}} (=^{.})) \\ L_{2}. & L_{Ass_{1}} , L_{Ass_{2}} ⊢ & \begin{matrix}(λx even(x + b))(c) ⇒ \\ (λx even(x + b))(a) \end{matrix} & (∀_{E} L_{1} (λx even(x + b))) \\ L_{3}. & L_{Ass_{1}} , L_{Ass_{2}} ⊢ & even(c + b) ⇒ even(a + b) & (λ↔ L_{2}) \\ L_{T hm}. & L_{Ass_{1}} , L_{Ass_{2}} ⊢ & even(a + b) & (⇒_{E} L_{3} L_{T hm′}) \end{matrix}

open-lines {}

Figure 20: A strategic action of Exp.

InstMeta

The algorithm InstMeta computes instantiations of meta-variables. Actions of InstMeta store the computed instantiation in the slot instantiation. An example for an action of InstMeta is given in Figure 21. This action results from the application of the strategy ComputeInstFromCS to the task mv_{δ}|^{Inst}. InstMeta computes the instantiation min(c_{δ_{1}}, c_{δ_{2}}) for mv_{δ} and stores it in the instantiation slot.

23If one of the premises P_{1}, …, P_{n} is open, then it is not in this slot, since it was not changed by the expansion (i.e., its open justification was not created by the expansion).

InstMeta Action

strategy ComputeInstFromCS
task  mv_{δ}|^{Inst}

binding store

BS

instantiation min(c_{δ_{1}}, c_{δ_{2}})

Figure 21: A strategic action of InstMeta.

5.3 Strategic Proof Plans

In this section, we shall extend the notions introduced in section 3.1 to strategic proof plans. We start with the definitions of a strategic proof planning problem, an initial PDS of a strategic proof planning problem (which is the same as the initial PDS of a proof planning problem), and an initial agenda of a strategic proof planning problem (which is different from the initial agenda of a proof planning problem since it may contains instantiationtasks).

Definition A strategic proof planning problem is a quadruple (T hm, {Ass_{1}, …, Ass_{n}}, S, C_{S}), where T hm and Ass_{1}, …, Ass_{n} are formulas in Ωmega’s higher-order language, S is a set of strategies, and C_{S} is a set of strategic control rules. T hm is also called the theorem of the strategic proof planning problem whereas Ass_{1}, …, Ass_{n} are called the assumptions of the strategic proof planning problem.

Definition Let (T hm, {Ass_{1}, …, Ass_{n}}, S, C_{S}) be a strategic proof planning problem. The initial PDS of this problem is the PDS that consists of an open line L_{T hm} with formula T hm and the lines L_{Ass_{i}} with formula Ass_{i} and the hypothesis justification Hyp, respectively. The initial agenda of the strategic proof planning problem is the agenda that consists of the linetask L_{T hm} ◀ {L_{Ass_{1}}, …, L_{Ass_{n}}} and an instantiation-task mv|^{Inst} for each meta-variable in L_{T hm}, L_{Ass_{1}}, …, L_{Ass_{n}}.

Next, we extend the action applicability notion of PLAN. In Multi, actions are applicable with respect to a PDS and a binding store. In particular, an action is applicable only if the current binding store equals^{24} the binding store with respect to which the action was computed (i.e., the binding store that is stored in the slot binding store of the action). This restriction is necessary since the computation of actions can rely on given bindings in the current binding store. Moreover, we extend the action introduction functions Φ and Φ⃗ of PLAN (see definition 3.1 and definition 3.1) to the strategic action introduction functions Φ_{Multi} and Φ⃗_{Multi}. Φ_{Multi} describes the operational semantics of an action in Multi when it is applied to an agenda, a PDS, a sequence of actions, and a sequence of bindings stores, i.e., Φ_{Multi} defines a transition relation between quadruples of agendas, PDSs, sequences of actions, and sequences of binding stores. First, we give general definitions of Φ_{Multi} and Φ⃗_{Multi}. Then, we define for each kind of action used in Multi when it is applicable and the results of its introduction by Φ_{Multi}.

24Two binding stores are equal when they contain the same bindings.

Definition The action introduction function Φ_{Multi} is a partial function that maps a sequence of actions, an agenda, a PDS, a sequence of binding stores, and an applicable action into a sequence of actions, an agenda, a PDS, and a sequence of binding stores, i.e.,

Φ_{Multi} : A⃗ × Â × P × B⃗S × A_{add} ↦ A⃗’ × Â’ × P’ × B⃗S’.

The recursive action introduction function Φ⃗_{Multi} is a partial function that maps a sequence of actions, an agenda, a PDS, a sequence of binding stores, and a sequence of actions into a sequence of actions, an agenda, a PDS, and a sequence of binding stores, i.e.,

Φ⃗_{Multi} : A⃗ × Â × P × B⃗S × A⃗_{add} ↦ A⃗’ × Â’ × P’ × B⃗S’.

Φ⃗_{Multi} is recursively defined as follows: Let A⃗ be a sequence of actions, Â an agenda, P a PDS, B⃗S a sequence of binding stores, and A⃗_{add} a sequence of actions.

1. If A⃗_{add} is empty, then Φ⃗_{Multi}(A⃗, Â, P, B⃗S, A⃗_{add}) := (A⃗, Â, P, B⃗S).

2. Otherwise let A_{add} := first(A⃗_{add}) and A⃗’_{add} := rest(A⃗_{add}). If A_{add} is applicable with respect to P and the last binding store of B⃗S, and if Â contains the task of A_{add}, then Φ⃗_{Multi}(A⃗, Â, P, B⃗S, A⃗_{add}) := Φ⃗_{Multi}(Φ_{Multi}(A⃗, Â, P, B⃗S, A_{add}), A⃗’_{add}).

Method Actions

A method action is applicable with respect to a PDS, if the given lines of the action are in the PDS. Φ_{Multi} differs from Φ in two points. First, Φ_{Multi} creates not only new line-tasks but also new instantiation-tasks (for each new meta-variable in the new outlines created by the method action) and new expansion-tasks (for each conclusion of the method action). Second, Multi allows method actions that contain binding constraints in their constraints slot. These binding constraints are labeled with Binding, which indicates that they are not passed to an external constraint solver but to the binding store.^{25} When the action is introduced, a new binding store is created and added to the sequence of binding stores. The new binding store results from the union of the bindings of the last binding store and the new bindings. The instantiation-tasks whose meta-variables are bound by the new bindings are then removed from the agenda.

Definition Let P be a PDS, BS a binding store, and A_{add} a method action with the binding store BS_{A_{add}}. Moreover, let L be the set of proof lines of P and let ⊖Concs be the ⊖ conclusions, ⊖P rems the ⊖ premises, and BP rems the blank premises of A_{add}. A_{add} is applicable with respect to P and BS, if 1. (⊖Concs ∪ ⊖P rems ∪ BP rems) is a subset of L,

25Internal binding constraints in method actions were first introduced by Lassaad Cheikhrouhou in an extension of PLAN for proof planning diagonalization proofs [11].

2. BS_{A_{add}} = BS.

Definition Let B⃗S be a sequence of bindings stores and let BS be the last binding store of B⃗S. Let A⃗ be a sequence of actions and let A_{add} be a method action, which is applicable with respect to a PDS P and BS.

Moreover, let ⊕Concs be the ⊕ conclusions, ⊖Concs the ⊖ conclusions, ⊕P rems the ⊕ premises, ⊖P rems the ⊖ premises, and BP rems the blank premises of A_{add}. Let T = L_{open} ◀ SUPPS_{L_{open}} be the task of A_{add} and let σ be the binding constraints of A_{add}. P rems:=⊕P rems ∪ ⊖P rems ∪ BP rems, Concs:=⊕Concs ∪ ⊖Concs New-Lines:=⊕Concs ∪ ⊕P rems New-Supps:=(SUPPS_{L_{open}} ∪ ⊕Concs) − ⊖P rems. New-Line-T asks:=[L ◀ New-Supps | L ∈ ⊕P rems]. New-Inst-T asks:=[mv|^{Inst} | mv ∈ New-Lines and not mv|^{Inst} in Â]. New-Exp-T asks:=[C|^{Exp} | C in Concs]. New-T asks:=New-Line-T asks ∪ New-Inst-T asks ∪ New-Exp-T asks. Old-Inst-T asks:=[mv|^{Inst} | mv:=^{b} t ∈ σ]. Â_{rest}:=Â − ([T] ∪ Old-Inst-T asks)).

If Â is an agenda that contains the task T of A_{add}, then the result (A⃗’, Â’, P’, B⃗S’) of Φ_{Multi}(A⃗, Â, P, B⃗S, A_{add}) is defined by:

• A⃗’:= A⃗ ∪ [A_{add}].

• Â’:= { ; New-T asks ∪ Â_{rest}  if L_{open} ∈ ⊖Concs, [L_{open} ◀ New-Supps] ∪ New-T asks ∪ Â_{rest}  else.

• P’ results from P by

1. adding the proof lines New-Lines, respectively, and

2. justifying the proof lines ⊖Concs and ⊕Concs by the application of the method of A_{add} to P rems, respectively.

• If σ is empty, then B⃗S’:=B⃗S. Otherwise, B⃗S’:=B⃗S ∪ [BS_{new}] where BS_{new} := {mv_{i}:=^{b} t_{i}σ|(mv_{i}:=^{b} t_{i}) ∈ BS} ∪ σ.^{26} InstMeta Actions

26t_{i}σ is the term that results from the application of the binding constraints in σ to the subterms of t_{i}.

That is, each occurrence of a meta-variable mv′ in t_{i} that is bound by a constraint mv:=^{b} t′ in σ is replaced by an occurrence of t′.

An InstMeta action is applicable with respect to a binding store and a PDS, if the proof lines of the PDS contain occurrences of its meta-variable but there is no binding for the meta-variable in the binding store. When applied to an action of InstMeta, Φ_{Multi} creates a new binding store, which is added to the sequence of binding stores. The new binding store results from adding a binding for the meta-variable of the instantiation-task of the action to the last binding store of the sequence.

Definition Let P be a PDS with proof lines L, BS a binding store, and A_{add} an InstMeta action. Let T_{A_{add}} = mv|^{Inst} be the task of A_{add} and BS_{A_{add}} its binding store. A_{add} is applicable with respect to P and BS, if

1. there are occurrences of mv in the formulas of the proof lines L,

2. there is no binding for mv in BS,

3. BS_{A_{add}} = BS.

Definition Let B⃗S be a sequence of bindings stores and let BS be the last binding store of B⃗S. Let A⃗ be a sequence of actions and let A_{add} be an InstMeta action, which is applicable with respect to a PDS P and BS.

Moreover, let T = mv|^{Inst} be the task of A_{add} and let t be the instantiation for mv in A_{add}. σ:={mv:=^{b} t}.

If Â is an agenda that contains the task T of A_{add}, then the result (A⃗’, Â’, P’, B⃗S’) of Φ(A⃗, Â, P, B⃗S, A_{add}) is defined by:

• A⃗’:= A⃗ ∪ [A_{add}].

• Â’:= Â - [T].

• P’:= P.

• B⃗S’:=B⃗S ∪ [BS_{new}] where BS_{new} := {mv_{i}:=^{b} t_{i}σ|(mv_{i}:=^{b} t_{i}) ∈ BS} ∪ σ.

ATPActions

An ATPaction is applicable wrt. a PDS, if the proof lines of the line-task of the action are in the PDS. When applied to an action of ATPwith task L_{open} ◀ {S_{1}, …, S_{n}}, Φ_{Multi} closes L_{open} in the PDS with an application of the tactic atp. The only resulting new task is an expansion-task for L_{open}.

Definition Let P be a PDS with the proof lines L, BS a binding store, and A_{add} an ATP action. Let T_{A_{add}} = L_{open} ◀ {S_{1}, …, S_{n}} be the task of A_{add} and BS_{A_{add}} its binding store. A_{add} is applicable with respect to P and BS, if 1. L_{open} ∈ L and SUPPS_{L_{open}} ⊆ L,

2. BS_{A_{add}} = BS.

Definition Let B⃗S be a sequence of bindings stores and let BS be the last binding store of B⃗S. Let A⃗ be a sequence of actions and let A_{add} be an ATPaction, which is applicable with respect to a PDS P and BS.

Moreover, let T = L_{open} ◀ SUPPS_{L_{open}} be the task of A_{add} and let Out be the content of the slot output of A_{add}.

If Â is an agenda that contains the task T of A_{add}, then the result (A⃗’, Â’, P’, B⃗S’) of Φ(A⃗, Â, P, B⃗S, A_{add}) is defined by:

• A⃗’:= A⃗ ∪ [A_{add}].

• Â’:= (Â − [T]) ∪ [L_{open}|^{Exp}].

• P’ results from P by justifying the proof line L_{open} with an application of the tactic atp to the supports SUPPS_{L_{open}} and the parameter Out.

• B⃗S’:=B⃗S.

ExpActions

An Expaction is applicable with respect to a PDS, if the closed line in the expansiontask of the action is in the PDS and if the premises of the justification of the closed line are in the PDS. When applied to an action of Exp, Φ_{Multi} introduces the new proof lines of the expansion-segment slot into the PDS and adds all resulting new tasks to the agenda, namely new instantiation-tasks for new meta-variables in the new proof lines, new line-tasks for open lines in the new proof lines, and new expansion-tasks for all new proof lines, which have a tactic or a method justification.

Definition Let P be a PDS with the proof lines L, BS a binding store, and A_{add} an Expaction with the binding store BS_{A_{add}}. Moreover, let T_{A_{add}} = L|^{Exp} be the task of A_{add} where L has the justification (J P_{1} … P_{n}). A_{add} is applicable with respect to P and BS, if

1. L ∈ L and {P_{1} … P_{n}} ⊆ L,

2. BS_{A_{add}} = BS.

Definition Let B⃗S be a sequence of bindings stores and let BS be the last binding store of B⃗S. Let A⃗ be a sequence of actions and let A_{add} be an Expaction, which is applicable with respect to a PDS P and BS.

Moreover, let T = L|^{Exp} be the task of A_{add} and (J P_{1} … P_{n}) the justification of L (before the expansion). SUPPS:={P_{1}, …, P_{n}}. New-Lines:=expansion-segment of A_{add} without L, P_{1}, …, P_{n}. New-Open-Lines:=open-lines of A_{add}. New-Line-T asks:=[L′ ◀ SUPPS | L′ in New-Open-Lines]. New-Inst-T asks:=[mv|^{Inst} | mv ∈ New-Lines and not mv|^{Inst} in Â]. New-Exp-T asks:=[L′|^{Exp} |(L′ ∈ New-Lines or L′ = L) andL′ closed by tactic or method]. New-T asks:=New-Line-T asks ∪ New-Inst-T asks ∪ New-Exp-T asks.

If Â is an agenda that contains the task T of A_{add}, then the result (A⃗’, Â’, P’, B⃗S’) of Φ(A⃗, Â, P, B⃗S, A_{add}) is:

• A⃗’:= A⃗ ∪ [A_{add}].

• Â’:= (Â − [T]) ∪ New-T asks.

• P’ results from P by

1. adding the new justification specified in the expansion segment to L as the justification of the lowest level of abstraction, and

2. adding the proof lines New-Lines.

• B⃗S’:=B⃗S.

PPlanner and CPlanner Actions

A PPlanner or CPlanner action A_{S} is applicable, if all actions [A_{1}, …, A_{n}] in its action-sequence slot are applicable when introduced successively. When applied to A_{S}, Φ_{Multi} stepwise introduces the actions from the sequence [A_{1}, …, A_{n}] using the function Φ⃗_{Multi}. Afterwards, it replaces [A_{1}, … A_{n}] in the constructed action sequence by A_{S}. That is, the actions A_{1}, …, A_{n} are not explicitly mentioned in the constructed action sequence but only implicitly as part of the action of PPlanner or CPlanner. This guarantees that Φ_{Multi} and Φ⃗_{Multi} create a sequence of strategic actions.

Definition Let P be a PDS, BS a binding store, and A_{add} a PPlanner or CPlanner with the action sequence [A_{1}, …, A_{n}]. Moreover, let T_{A_{add}} be the task of A_{add} and BS_{A_{add}} its binding store. A_{add} is applicable with respect to P and BS, if for each A_{i}, i = 1 … n in [A_{1}, …, A_{n}] holds:

• Let (A⃗_{i}, Â_{i}, P_{i}, B⃗S_{i}) := Φ⃗_{Multi}(A⃗, Â, P, B⃗S, [A_{1}, …, A_{i−1}]) for an arbitrary sequence of actions A⃗ and an agenda Â that contains the task T_{A_{add}}. Then, A_{i} is applicable with respect to P_{i}, and B⃗S_{i} and Â_{i} contains the task of A_{i}.

Definition Let B⃗S be a sequence of bindings stores and let BS be the last binding store of B⃗S. Let A⃗ be a sequence of actions and let A_{add} be a PPlanner or CPlanner action, which is applicable with respect to a PDS P and BS.

Moreover, let [A_{1}, …, A_{n}] be the action-sequence of A_{add}. (A⃗_{rec}, Â_{rec}, P_{rec}, B⃗S_{rec}) := Φ⃗_{Multi}(A⃗, Â, P, B⃗S, [A_{1}, …, A_{n}]).

If Â is an agenda that contains the task of A_{add}, then the result (A⃗’, Â’, P’, B⃗S’) of Φ(A⃗, Â, P, B⃗S, A_{add}) is defined by:

• A⃗’:= (A⃗_{rec} − [A_{1}, …, A_{n}]) ∪ [A_{add}].

• Â’:= Â_{rec}.

• P’:= P_{rec}.

• B⃗S’:=B⃗S_{rec}.

With the function Φ⃗_{Multi} we can define strategic proof plans and strategic solution proof plans. Actually, we shall give three different notions of solution proof plans, which specify more and more strict conditions for strategic proof plans.

Definition Let (T hm, {Ass_{1}, …, Ass_{n}}, S, C_{S}) be a strategic proof planning problem, P_{init} the initial PDS of this problem, and Â_{init} its initial agenda.

A strategic proof plan to the strategic proof planning problem is a quadruple SPP = (A⃗, Â, P, B⃗S) with a sequence of strategic actions A⃗, an agenda Â, a PDS P, and a sequence of binding stores B⃗S such that:

1. each strategy of an action of A⃗ is in S,

2. (A⃗, Â, P, B⃗S) = Φ⃗_{Multi}([], Â_{init}, P_{init}, [], A⃗),

With respect to this definition of a strategic proof plan we can also say that Φ_{Multi} maps a strategic proof plan and an action into a strategic proof plan and that Φ⃗_{Multi} maps a strategic proof plan and a sequence of strategic actions into a strategic proof plan.

Definition Let (T hm, {Ass_{1}, …, Ass_{n}}, S, C_{S}) be a strategic proof planning problem, P_{init} the initial PDS of this problem, and Â_{init} its initial agenda.

We distinguish the following three notions of a strategic solution proof plan:

• A method-level solution proof plan for the problem is a sequence of strategic actions A⃗ such that Φ⃗_{Multi}([], Â_{init}, P_{init}, [], A⃗) results in an agenda without line-tasks and a closed PDS.

• An instantiated method-level solution proof plan for the problem is a sequence of strategic actions A⃗ such that Φ⃗_{Multi}([], Â_{init}, P_{init}, [], A⃗) results in an agenda without line-tasks and instantiation-tasks, a closed PDS, and a binding store sequence such that the last binding store contains bindings for all meta-variables occurring in proof lines of the final PDS.

• A full solution proof plan for the problem is a sequence of strategic actions A⃗ such that Φ⃗_{Multi}([], Â_{init}, P_{init}, [], A⃗) results in an empty agenda, a closed PDS in which all nodes are justified by ND-rules, and a binding store sequence such that the last binding store contains bindings for all meta-variables occurring in proof lines of the final PDS.

The first notion of solution proof plan is called method-level solution proof plan since a strategic proof plan satisfying these conditions is reached by computing method actions whose introduction satisfies all line-tasks and creates a closed PDS. Instantiation-tasks and expansion-tasks can be ignored. The second notion of solution proof plan, instantiated method-level solution proof plan, demands to tackle also instantiation-tasks. However, expansion-tasks can still be ignored. Finally, in order to obtain a full solution proof plan the expansion-tasks have to be solved. We shall describe in section 5.6.2 how a user can make Multi search for a particular kind of solution proof plan.

5.4 Strategic Manipulation Records

Similar to PLAN, Multi constructs a history consisting of manipulation records. These manipulation records contain information, which can be used by the control rules in order to perform meta-reasoning.

Strategy-Application:

agenda

alternative-job-offers introduced-action new-tasks execution-message

Figure 22: A strategy-application record.

A strategy execution of the algorithms Exp, ATP, and InstMeta creates one so-called strategy-application record (see Figure 22). The slots agenda and alternative-job-offers capture the context in which the manipulation was done whereas the the slots introduced-action, new-tasks, and execution-message store the result of the manipulation. The slot agenda captures the agenda before the strategy is applied. The slot alternative-job-offers contains the list of alternative job offers, when the strategy was applied. The first job offer in this list is the applied strategy and the task to which the strategy was applied. The performed manipulation, namely the action introduced by the execution of the strategy, is stored in the introduced-action slot. This slot is empty, if the execution of a strategy failed. The new tasks created by the introduction of the action are stored in the slot new-tasks. The slot execution-message contains the execution-message returned by the strategy execution.

Strategy executions of the algorithms PPlanner and CPlanner create two manipulation records. When they are invoked or re-invoked, they create a strategy-start record; when they terminate or are interrupted, then they create a strategy-stop record. Figure 23 shows the skeletons of these two manipulation records.

Strategy-Start:

agenda

alternative-job-offers task-tag

Strategy-Stop:

task-tag

introduced-action new-tasks execution-message

Figure 23: Manipulation records created by PPlanner and CPlanner.

The strategy-start and strategy-stop records divide the information of a strategy-appli-cation record into two parts: the information available when the strategy is invoked or re-invoked, which is stored in a strategy-start record, and the information available when the strategy stops, which is stored in a strategy-stop record. Hence, a strategy-start record has the slots agenda and alternative-job-offers whereas a strategy-stop record has the slots introduced-action, new-tasks, and execution-message. Additionally, both records have the slot task-tag, which contains the task-tag that uniquely identifies the strategy execution.

Note that the manipulation records of the steps performed within a strategy execution of PPlanner or CPlanner are themselves part of the history. They are not stored in a PPlanner or CPlanner history element but only delimited by the strategy-start and strategy-stop records of the strategy execution. This approach makes information available as early as possible. In particular, the information on the situation when the strategy was invoked or re-invoked and the information on all steps performed by a strategy execution so far are available for the control rules evaluated within the strategy execution.

Strategies of the BackTrack algorithm create two manipulation records whose skeletons are given in Figure 24. The backtrack-start record contains the information available when the backtracking is started (stored in the agenda and alternative-job-offers slots) as well as the information which actions the strategy decided to delete. The backtrack-stop record contains the information available when the BackTrack strategy stops. Since strategies of BackTrack do not create actions, this record contains only a slot for the execution message.

BackTrack-Start:

agenda

alternative-job-offers actions-to-delete

BackTrack-Stop:

execution-message

Figure 24: Manipulation records created by BackTrack.

Similar to CPlanner and PPlanner, strategy executions of BackTrack successively perform also a set of individual steps. When executed, a strategy of BackTrack computes first which actions it has to delete. These actions are stored in the start record. However, in order to delete these actions maybe other actions have to be deleted as well (see section 5.5.7 for details). All single deletion steps are stored in action-deletion records as in PLAN (see section 3). Hence, a start and stop record pair of a BackTrack strategy execution delimits the manipulation records of all single deletion steps performed within this strategy execution.

5.5 The Algorithms

In this section, we shall describe the algorithms used in Multi. First, we explain Multi’s top-level algorithm. Then, we describe the refinement and modification algorithms integrated so far, namely PPlanner, CPlanner, Exp, ATP, InstMeta, and BackTrack.

In the remainder of this section we assume that each function and algorithm used in Multi has access to the blackboards and the entries on them. Hence, when an algorithm or a function accesses information from a blackboard we shall not mention the respective blackboard explicitly as an argument of the function. The only exceptions are the functions write-onto-blackboard, which sets the value of an entry on a blackboard, and take-from-blackboard, which returns the value of an entry on a blackboard. Both functions obtain the blackboard on which they should work as argument. In the following descriptions of the algorithms we use PB and CB as abbreviations for the proof blackboard and the control-blackboard, respectively.

5.5.1 The Multi Algorithm

Figure 25 gives a pseudo-code description of the Multi algorithm. Multi is applied to a strategic proof planning problem with a theorem T hm, a set of assumptions Ass_{1}, …, Ass_{n}, a set of strategies S, and a set of strategic control rules C_{S}. Its output is a strategic proof plan for the given problem (T hm, {Ass_{1}, …, Ass_{n}}, S, C_{S}). Multi’s first step is to initialize the proof and the control blackboard. It writes onto the proof blackboard an empty sequence of actions, the initial agenda and the initial PDS of the given problem, and a sequence of binding stores whose only entry consists of an empty binding store. Moreover, it writes onto the control blackboard an empty set of memory entries, an empty set of demands, and an empty sequence of job offers.

Input: A strategic proof planning problem (T hm, {Ass_{1}, …, Ass_{n}}, S, C_{S}) with a theorem formula T hm, a set of assumption formulas Ass_{1}, …, Ass_{n}, a list of strategies S, and a list of strategic control rules C_{S}.

Output: A strategic proof plan SPP = (A⃗, Â, P, B⃗S) with a sequence of strategic actions A⃗, an agenda Â, a PDS P, and a sequence of binding stores B⃗S.

Algorithm: Multi(T hm, {Ass_{1}, …, Ass_{n}}, S, C_{S})

1. Initialization Let Â:=initial-agenda(T hm, {Ass_{1}, …, Ass_{n}}). Let P:=initial-PDS(T hm, {Ass_{1}, …, Ass_{n}}). write-onto-blackboard([], sequence-of-actions, P B). write-onto-blackboard(Â, agenda, P B). write-onto-blackboard(P, pds, P B). write-onto-blackboard([{}], sequence-of-binding-stores, P B). write-onto-blackboard([], history, P B). write-onto-blackboard(∅, memory, CB). write-onto-blackboard(∅, demands, CB). write-onto-blackboard([], job-offers, CB).

2. Job Offers trigger-jobs-from-strategies (S). trigger-jobs-from-memory().

3. Guidance invoke(MetaReasoner, C_{S}).

4. Invocation Let J:=remove-free-jobs (take-from-blackboard(job-offers, CB)). If J = ∅

then terminate and return (take-from-blackboard(sequence-of-actions, P B), take-from-blackboard(agenda, P B), take-from-blackboard(pds, P B), take-from-blackboard(sequence-of-binding-stores, P B)).

else Let J:=first(J). If job-offer-from-strategy(J) then (i.e., J = (S, T))

invoke(algorithm-of-strategy(S), (S, T), J). else (i.e., J = (@_{T} , Demands))

invoke(algorithm-of-task-tag(@_{T}), @_{T} , J).

5. Execution Wait until strategy-ks-terminated().

6. Administration If strategy-ks-terminated-successful (), then delete-satisfied-demands (). Goto step 2.

Figure 25: The Multi algorithm.

The next four steps, steps 2—5 in Figure 25, of Multi perform the strategy selection and invocation cycle that is sketched in Figure 13 in the previous section. Step 2 employs the functions trigger-jobs-from-strategies and trigger-jobs-from-memory. trigger-jobs-from-strategies checks whether the condition of an element of S is satisfied by some tasks of the current agenda on the proof blackboard. A strategy S ∈ S places a job offer onto the control blackboard for each task T for which its condition is true. The function trigger-jobs-from-memory writes for each memory entry a job offer onto the control blackboard. Afterwards, step 3 invokes the MetaReasoner, which evaluates the strategic control rules C_{S} on the job offers.

In step 4, Multi first reads the resulting list of job offers and deletes the job offers whose strategies have still uninstantiated free parameters. If the resulting list is empty, then Multi terminates and returns the strategic proof plan (i.e., the sequence of actions, the agenda, the PDS, and the sequence of binding stores) on the proof blackboard. Otherwise Multi picks the first job offer and invokes the corresponding strategy. If the job offer was placed by a strategy S with respect to a task T, which satisfies the condition of S, then Multi invokes the algorithm of S with the pair (S, T) as argument. If the job offer was placed from a memory entry with task tag @_{T}, then algorithm-of-task-tag computes the algorithm that created the tag @_{T} using information stored in the history and invokes this algorithm with @_{T} as argument. In both cases the invoked algorithm obtains the list of all job offers on the control blackboard as second argument.

The invoked algorithm refines or modifies the proof blackboard objects and maybe places demands and a memory entry onto the control blackboard. Multi waits until the execution of the strategy terminates (see step 5). Then, step 6 checks whether the strategy terminated successfully. This check is performed by the function strategy-ks-terminated-successful , which looks up the execution message of the last history on the proof blackboard. If this execution message is a success message, then Multi employs the function delete-satisfied-demands to delete all demands on the control blackboard that are satisfied by the terminated strategy execution as well as all pointers in memory entries to those demands. Afterwards, Multi restarts its cycle by proceeding with step 2.

We conclude this section with two remarks on the described algorithm:

1. When employing the two functions trigger-jobs-from-memory (in step 2) and delete-satisfied-demands (in step 6) Multi changes the content of the control blackboard. This is a violation of the blackboard principle, which states that the content of the blackboards should only be changed by respective knowledge sources. For the sake of simplicity of Multi’s blackboard approach we implemented these minor blackboard changes as direct functionalities of the Multi algorithm. However, in order to avoid a violation of the blackboard principle, we could understand these two functions as particular knowledge sources working on the control blackboard, which are scheduled by Multi in a pre-defined way.

2. PLAN terminates either with a solution proof plan or, after traversing the search space, with a failure. Multi terminates as soon as there is no further job offer to invoke (see step 4). However, the lack of job offers states nothing about the status of the strategic proof planning process. When there are no further tasks in the agenda, then there are no further job offers since there is a strategic solution proof plan on the proof blackboard. But it is possible that there are still tasks in the agenda although there are no further job offers. It is possible that there are no strategies to tackle these tasks (i.e., there is no strategy whose condition is satisfied by the task) or strategic control rules can remove all existing job offers. If Multi terminates and there are still tasks in the agenda, then it is up to the user to analyze the situation. Is the strategic proof plan created so far a sufficient solution proof plan (when the user is interested in a method-level solution proof plan then expansion-tasks and instantiation-tasks can be ignored)? Are further strategies needed that can deal with particular tasks? Are less restrictive strategic control rules needed that do not remove so much job offers?

5.5.2 The PPlanner Algorithm

Strategies of the algorithm PPlanner refine a strategic proof plan by successively adding method actions, which PPlanner abstracts in one strategic action, when it terminates. A strategy of PPlanner specifies four parameters: a procedure for the computation of the next method action to introduce, parameters for the set of usable methods and control rules, and a termination condition. We discussed some strategies of PPlanner already in section 4.1.

Figure 26 gives a pseudo-code description of the PPlanner algorithm. PPlanner obtains two arguments. When a PPlanner strategy S is initially invoked, then PPlanner’s first input is a pair (S, T) consisting of the strategy S and a line-task T. When a strategy execution is re-invoked, then the first argument is the task tag of the strategy execution. The second argument for PPlanner is the list of all alternative job offers on the control blackboard, when PPlanner is invoked. PPlanner returns no specific output but updates the content of the proof blackboard by introducing successively method actions. Essentially, PPlanner performs a cycle of task selection, action selection, and action introduction, which is similar to the cycle of PLAN. This core cycle is completed by an initialization step and different events that stop the PPlanner algorithm, namely successful termination, interruption, and failure.

In the initialization step (step 1 in Figure 26) PPlanner extracts the information of the strategy and the initial task with respect to which it runs. First, it employs the function extract-from-input, which computes the current task tag @_{T}, the current strategy S, and the initial task T. If the first input of PPlanner is a pair (S, T) (i.e., initial call of S on T), then the information on S and T is directly accessible and extract-from-input creates a new task tag @_{T}, which it attaches to T. If the first input of PPlanner is a task tag @_{T} (i.e., re-invocation of interrupted strategy execution), then extract-from-input employs information from the history to compute the strategy S and the initial task T that correspond to the given task tag. Next, PPlanner uses the function parameters-of-strategy to obtain the parameters of the strategy S, which are a list of methods M, a list of control rules C, the termination condition, and the action computation and selection procedure. So far, we have implemented two action computation and selection procedures, namely ChooseAction (see section 3.4) and ChooseActionAll (see appendix A).^{27} Afterwards, PPlanner adds a

27Note that parts of these algorithms work slightly differently when used in Multi as opposed to the functionality described in section 3.4 and appendix A. All functions used within these algorithms that match proof lines of a method with proof lines of a task (e.g., match-task-line, match-s+p see section 3.4)

apply first the bindings of the current binding store to the proof lines of the task. Then, they perform the respective matchings with respect to this “up-to-date” proof lines instead of the original ones.

Input: (1) either a pair (S, T) where S is a PPlanner strategy and T is a line-task or a task tag @_{T}, (2) the list of all alternative job offers J.

Output: No output, only changes of the blackboards.

Algorithm: PPlanner(arg_{1}, J_{rest}))

1. Initialization Let (@_{T} , S, T):=extract-from-input(arg_{1}). Let (M, C, term-cond, action-proc):=parameters-of-strategy (S). add-strategy-start-record-to-history(J_{rest}, @_{T}). Let A⃗_{add}:=liste.

2. Successful Termination Check (see Figure 27)

3. Interruption Check (see Figure 27)

4. Task Selection:

Let current task T_{curr}:= first(evalcrules-tasks (tasks-with-tag(@_{T}), C)).

5. Action Selection Let (A_{add},A):=apply(action-proc, T_{curr}, M, C) where A_{add} is an action and A is the set of computed alternative actions.

6. Action Introduction

If A_{add} is given

then PB:=Φ_{Multi}(A_{add}, P B). add-action-intro-record(A_{add},A). A⃗_{add}:=A⃗_{add} ∪ [A_{add}]. If extract-constraints(A_{add}) ≠ ∅

then

pass-constraints (extract-constraints(A_{add})). Goto step 2.

7. Failure (see Figure 27)

Figure 26: The PPlanner algorithm.

strategy-start record to the history and sets the algorithm variable A⃗_{add} to the empty list. In this variable PPlanner stores the method actions, which it introduces successively.

Step 2 and step 3 in Figure 26 check whether PPlanner terminates successfully or interrupts. We postpone the detailed discussion of these two steps until the discussion of step 7 in order to discuss together all three steps that stop PPlanner and the differences among them. The next three steps — step 4, step 5, and step 6 — are the core cycle of selecting the next task, computing and selecting the next method action, and introducing the selected action. Essentially, these steps correspond to step 2, step 3, and step 4 of PLAN in Figure 8 in section 3.2, they are only slightly adapted to Multi. When PPlanner selects the next task to tackle in step 4, then it evaluates the control rules of kind ‘Task’ not on the whole agenda of the proof blackboard, but only on the tasks that carry the current task tag @_{T} (the restricted initial alternative list is computed by the function tasks-with-tag). Whereas in PLAN the application of the algorithm ChooseAction is fix, PPlanner applies the action computation procedure specified as parameter of the current strategy in step 5. When an action is found, then PPlanner applies this action in step 6 with the function Φ_{Multi} to the action sequence, the agenda, the PDS, and the sequence of binding stores on the proof blackboard. We write this as “PB:=Φ_{Multi}(A_{add}, P B)” and do not refer to the changed elements of the proof blackboard explicitly. Similar to PLAN, PPlanner adds a history entry for the introduced action and passes new constraints to external constraint solvers. Additionally, the introduced action is added to A⃗_{add}. Afterwards, PPlanner continues with step 2.

PPlanner can stop at three different places, namely step 2, step 3 and step 7, which are given in detail in Figure 27. Step 2 checks whether the application of the strategy of PPlanner was successful such that PPlanner should stop. This is the case either when the termination condition of the strategy is satisfied or when there are no further tasks which carry the task tag of the strategy execution. Step 3 employs the function evalcrules-interrupt to evaluate the control rules of kind ‘Interrupt’ on the alternative list [False,True], where False causes no interrupt whereas True causes an interrupt. The control rules of kind ‘Interrupt’ can also compute demands and attach the demands to the True element of the alternative list. Finally, step 7 is performed, when step 5 does not provide a method action to introduce, that is, step 7 deals with a failure situation in PPlanner.

Some computations are the same in all three steps. They all compute an execution message message and employ the function create-strategic-action to compute a strategic action A_{add}^{S} from the collected sequence of method actions A⃗_{add}. Moreover, they all replace the sequence of method actions by a new strategic action in the action sequence on the proof blackboard (this is done by the function replace-actions ). Finally, they all add a strategy-stop entry to the history before they terminate. The three steps differ in the created execution message and in whether and which memory entries and demands they create. When the strategy knowledge source terminates successfully, then PPlanner creates a success message and does not write memory entries or demands onto the control blackboard. Rather, it applies the function remove-tag , which removes its task tag from all tasks in the agenda on the proof blackboard. If the execution of the strategy interrupts, then it creates an interruption message and places a memory entry and demands onto the control blackboard. The demands stem from the evaluated control rules of kind ‘Interrupt’ and the memory entry consists of the task tag and pointers to the added demands. If PPlanner has to deal with a failure occurring with respect to the task T_{curr}, then it creates a failure message. Moreover, it writes a task-demand ? − ON − T_{curr} and a memory entry consisting of the task tag and a pointer to this task-demand onto the control blackboard. Since a failure creates a memory entry and a demand, we can understand it as a special kind of interrupt — the difference with respect to the origin of the interruption is recorded in the execution messages.

2. Termination Check

If no-tasks-with-tag(@_{T}) or apply(term-cond) = true

then Let message:=create-success-message (S, T). Let A_{add}^{S}:=create-strategic-action (A⃗_{add}). replace-actions (A⃗_{add}, A_{add}^{S}). remove-tag (@_{T}). add-strategy-stop-record-to-history(@_{T} , A_{add}^{S}, message). Terminate.

3. Interruption Check Let I:=first(evalcrules-interrupt([Nil, True], C)). If I = True

then Let message:=create-interrupt-message (S, T). Let A_{add}^{S}:=create-strategic-action (A⃗_{add}). replace-actions (A⃗_{add}, A_{add}^{S}). write-to-demands (demands (I)). write-to-memory(@_{T} , demands (I)). add-strategy-stop-record-to-history(@_{T} , A_{add}^{S}, message). Terminate.

7. Failure

IF A_{add} is not given

then Let message:=create-failure-message (S, T). Let A_{add}^{S}:=create-strategic-action (A⃗_{add}). replace-actions (A⃗_{add}, A_{add}^{S}). write-to-demands ({? − ON − T }). write-to-memory(@_{T} , {? − ON − T }). add-strategy-stop-record-to-history(@_{T} , A_{add}^{S}, message). Terminate.

Figure 27: Leaving the PPlanner algorithm.

The further interpretation of and reaction to the termination is left to Multi and meta-reasoning at the strategy-level (this holds also for all other refinement and modification algorithms employed by Multi, which can terminate in different ways). If the last strategy execution terminated with a success message, then Multi deletes all demands on the control blackboard that are satisfied by this strategy execution (see previous section). Moreover, strategic control rules can make use of the information contained in the execution messages. For instance, the strategic control rule prefer-backtrack-if-failure (see section 4.3) analyzes the execution messages and prefers to perform some backtracking if the last strategy was a PPlanner strategy and terminated with a failure message. This control rule (which can be overwritten by more specific control rules) forces a systematic traversal of the search space given by a PPlanner strategy.

5.5.3 The CPlanner Algorithm

Strategies of the algorithm CPlanner refine a strategic proof plan by successively transferring actions from a source proof plan into the proof plan under construction. A strategy of CPlanner specifies three parameters: a list of action transfer procedures, a list of control rules, and a termination condition. We discussed an example strategy of CPlanner already in section 4.4. More examples are discussed in [55].

Figure 28 gives a pseudo-code description of CPlanner. CPlanner obtains two arguments. When a CPlanner strategy S is initially invoked, then CPlanner’s first input is a pair (S, T) consisting of the strategy S and a line-task T. When a strategy execution is re-invoked, then the first argument is the task tag of the strategy execution. The second argument for CPlanner is the list of all alternative job offers on the control blackboard, when CPlanner is invoked. CPlanner returns no specific output but updates the content of the proof blackboard by introducing successively method actions.

Input: (1) either a pair (S, T) where S is a CPlanner strategy and T is a task or a task tag @_{T}, (2) the list of all alternative job offers J.

Output: No output, only changes of the blackboards.

Algorithm: CPlanner(arg_{1}, J_{rest}))

1. Initialization Let (@_{T} , S, T):=extract-from-input(arg_{1}). Let (T P, C, term-cond):=parameters-of-strategy (S). add-strategy-start-record-to-history(J_{rest}, @_{T}). Let A⃗_{add}:=[].

2. Successful Termination Check (see PPlanner Figure 27)

3. Interruption Check (see PPlanner Figure 27)

4. Select and Evaluate Transfer Procedures Let T P_{rest}:=evalcrules-transferprocs (T P). Until (Obj is action or demand) or (T P_{rest} = [])

Let T P_{curr}:=first(T P_{rest}). Let Obj:=evaluate (T P_{curr}). T P_{rest}:=rest(T P_{rest}).

5. Action Introduction

If Obj is action A_{add}

then PB:=Φ_{Multi}(A_{add}, P B). add-action-intro-record(A_{add},A). A⃗_{add}:=A⃗_{add} ∪ [A_{add}]. If extract-constraints(A_{add}) ≠ ∅

then pass-constraints (extract-constraints(A_{add})). Goto step 2.

6. Demand Interruption

If Obj is demand D_{add}

then Let message:=create-interrupt-message (S, T). Let A_{add}^{S}:=create-strategic-action (A⃗_{add}). replace-actions (A⃗_{add}, A_{add}^{S}). write-to-demands (D_{add}). write-to-memory(@_{T} , D_{add}). add-strategy-stop-record-to-history(@_{T} , A_{add}^{S}, message). Terminate.

7. Failure (see PPlanner Figure 27)

Figure 28: The CPlanner algorithm.

Several parts of the CPlanner algorithm are equal or similar to the PPlanner algorithm. As PPlanner CPlanner starts with the extraction of the strategy information and the initial task in step 1. In particular, step 1 extracts the action transfer procedures T P and sets the algorithm variable A⃗_{add} to the empty list. In this variable CPlanner stores the actions, which it introduces successively. Afterwards, step 2 and step 3 check whether CPlanner terminates successfully or interrupts. These two steps equal step 2 and step 3 of PPlanner, respectively, given in Figure 27.

Step 4 first evaluates the control rules of kind ‘TransferProcedure’ on the alternative action transfer procedures T P. This results in a changed and re-ordered alternative list T P_{rest}. Then, step 4 evaluates the action transfer procedures in the order of this list until either one procedure provides an action or a demand, which is stored in the algorithm variable Obj, or all procedures have been tried. That is, at the end of step 4 Obj is either bound to an action A_{add} or to a demand D_{add} or it is unbound. These three cases are covered by the following steps, respectively. Step 5 describes the processing of an action A_{add}. In this case, CPlanner introduces A_{add} into the proof plan under construction employing the function Φ_{Multi}. Moreover, it adds a history entry for the introduced action and passes new constraints to external constraint solvers. Additionally, the introduced action is added to A⃗_{add}. Then, CPlanner continues with step 2. Step 6 processes a demand D_{add}. It writes the demand onto the control blackboard and terminates then with an interrupt message. If the evaluation of the action transfer procedure provides neither an action nor a demand, then CPlanner terminates in step 7 with a failure message. This step equals step 7 of PPlanner in Figure 27.

5.5.4 The InstMeta Algorithm

Strategies of the algorithm InstMeta tackle an instantiation-task and compute a binding for the meta-variable of the instantiation-task. With this new binding a new binding store is created, which is added to the sequence of binding stores on the proof blackboard. A strategy of InstMeta specifies one parameter, namely a function that determines how the instantiation for a meta-variable is computed. We discussed some strategies of InstMeta in section 4.1.

Figure 29 contains a pseudo-code description of InstMeta. InstMeta has two arguments. First, a pair (S, T), which consists of an InstMeta strategy S and an instantiation-task T. Second, the list of all alternative job offers on the control blackboard, when the InstMeta strategy was invoked. InstMeta returns no specific output but updates the content of the proof blackboard.

Step 1 in Figure 29 applies the instantiation computation function of the strategy S to the task T. This function application can either succeed or fail. If the function application succeeds, then the algorithm variable inst is bound to the returned value. Otherwise inst stays unbound. Step 2 computes an instantiation action when inst is bound and applies this action with Φ_{Multi} to the strategic proof plan elements on the proof blackboard. Finally, step 3 adds a new strategy-application record to the history on the proof blackboard. The execution message of this record entry depends on whether inst is bound or not. When inst is bound InstMeta creates a success message, otherwise InstMeta creates a failure message.

Currently, the computation function of an InstMeta strategy is provides either one

Input: (1) a pair (S, T) where S is a InstMeta strategy and T is an instantiation-task, (2) the list of all alternative job offers J.

Output: No output, only changes of the blackboards.

Algorithm: InstMeta((S, T), J)

1. Compute Instantiation Let inst:=apply(compute-inst-function(S), T).

2. Compute and Apply Action

If bound(inst) then

Let A_{add}:=new-instmeta-action (S, T, inst).

PB:=Φ_{Multi}(A_{add}, P B).

3. Update History If bound(inst) than

Let message:=create-success-message (S, T).

add-strategy-application-record-to-history(J , A_{add}, ∅, message). else

Let message:=create-failure-message (S, T).

add-strategy-application-record-to-history(J , ∅, ∅, message). Terminate.

Figure 29: The InstMeta algorithm.

(success) or no (failure) solution. This was sufficient for the case studies conducted so far. When it turns out that a set of alternative instantiations and reasoning on the selection of one alternative is needed, then InstMeta can easily be extended to cover this functionality: The variable inst has to store a list of alternatives. Moreover, between step 1 and step 2 an additional step is needed, which evaluates control rules on the alternative instantiations and selects one. The control rules would become an additional parameter of InstMeta.

5.5.5 The ATPAlgorithm

Strategies of the algorithm ATPrefine a strategic proof plan by solving a line-task with an ATPaction. They apply external automated theorem provers and check whether their output is a proof. A strategy of ATPspecifies two parameters for these two functionalities, namely an application function and an output check function. We discussed a strategy of ATPin section 4.4.

Figure 30 contains a pseudo-code description of the ATPalgorithm. ATPhas two arguments. First, a pair (S, T), which consists of an ATPstrategy S and an instantiation-task T. Second, the list of all alternative job offers on the control blackboard, when the ATP strategy was invoked. ATPreturns no specific output but updates the content of the proof

Input: (1) a pair (S, T) where S is an ATPand T is a line-task, (2) the list of all alternative job offers J.

Output: No output, only changes of the blackboards.

Algorithm: ATP((S, T), J)

1. Apply Provers Let out:=apply(atp-apply-function(S), T).

2. Check Output Let check:=apply(atp-output-check-function(S), out, T).

3. Compute and Apply Action

If check = true then

Let A_{add}:=new-atp-action(S, T, out).

PB:=Φ_{Multi}(A_{add}, P B).

4. Update History If check = true then

Let message:=create-success-message (S, T).

add-strategy-application-record-to-history(J , A_{add}, ∅, message). else

Let message:=create-failure-message (S, T).

add-strategy-application-record-to-history(J , ∅, ∅, message). Terminate.

Figure 30: The ATPalgorithm.

blackboard.

Step 1 applies the application function of the strategy S to the task T. This function application provides an output, which is stored in the algorithm variable out. Step 2 applies the output check function to out, which returns either true or nil. If the result, which is stored in the algorithm variable check, is true, then out is accepted as proof. In this case, ATPcomputes an action and applies this action with Φ_{Multi} to the strategic proof plan elements on the proof blackboard (see step 3 in Figure 30). Finally, step 4 adds a new strategy-application record to the history on the proof blackboard. The execution message of this record entry depends on whether check is true. If check is true, then ATPcreates a success message, otherwise it creates a failure message.

5.5.6 The ExpAlgorithm

The algorithm Exprefines a strategic proof plan by expanding complex steps. When applied to a closed proof line L whose justification is (J P_{1} … P n), then Expcomputes a proof segment that derives L from P_{1}, …, P_{n} at a lower level of abstraction. Exphas no parameters. The only strategy of Expis ExpS.

Input: (1) a pair (S, T) where S is an Expstrategy and T = L|^{Exp} is an expansion-task, (2) the list of all alternative job offers J.

Output: No output, only changes of the blackboards.

Algorithm: Exp((S, T), J)

1. Compute Expansion-Segment Let (J P_{1} … P_{n}) be the justification of L. If is-tactic(J) then

Let exp-segment:=expand-tactic(L). else

Let exp-segment:=expand-method (L).

2. Compute and Apply Action

If bound(exp-segment)

then Let A_{add}:=new-expansion-action (S, T, exp-segment). PB:=Φ_{Multi}(A_{add}, P B).

3. Update History If boundexp-segment

then Let message:=create-success-message (S, T). add-strategy-application-record-to-history(J , A_{add}, ∅, message).

else Let message:=create-failure-message (S, T). add-strategy-application-record-to-history(J , ∅, ∅, message).

Terminate.

Figure 31: The Expalgorithm.

Figure 31 contains a pseudo-code description of the Exp algorithm. Exp obtains two arguments. First, a pair (S, T), which consists of a Exp strategy S (i.e., ExpS) and an expansion-task T. Second, the list of all alternative job offers on the control blackboard, when the Expstrategy was invoked. Expreturns no specific output but updates the content of the proof blackboard.

Step 1 tests whether the justification Exp should expand is a tactic application or a method application. Depending on what kind of step it finds Exp employs either the function expand-tactic or the function expand-method to compute the expansion proof segment. expand-tactic evaluates the expansion procedure of the found tactic whereas expand-method instantiates the proof schema of the found method. When these function applications succeed, then the algorithm variable exp-segment is bound to the computed proof segment. Otherwise exp-segment stays unbound. When exp-segment is bound, Step 2 creates an expansion action and applies the action with Φ_{Multi} to the elements of the strategic proof plan on the proof blackboard. Afterwards, step 3 adds a new strategy-application record to the history on the proof blackboard. The execution message of this record entry depends on whether exp-segment is bound or not. When exp-segment is bound Expcreates a success message, otherwise Expcreates a failure message.

5.5.7 The BackTrack Algorithm

BackTrack is an algorithm that removes the actions introduced by other algorithms of Multi from a strategic proof plan. BackTrack adds no own actions but only history entries. When to backtrack and which actions to backtrack is not hard-wired in the Multi algorithm but is subject of the different strategies of BackTrack and the guidance by reasoning at the strategy-level. A strategy of BackTrack specifies a function that selects the set of actions in the current strategic proof plan that should be deleted. When Multi invokes a BackTrack strategy, then BackTrack removes all actions explicitly selected by this function as well as all actions that depend from these actions. Thus, the backtracking in Multi is dependency-directed in the sense discussed in section 3. We described a strategy of BackTrack in section 4.1.

Before we give a pseudo-code description of the BackTrack algorithm we shall introduce the notion of dependency among actions and when an action is deletable. Both notions are extensions of the concepts introduced for PLAN in section 3.3. When an action is introduced into a strategic proof plan, then it modifies the elements of the strategic proof plan. Other actions introduced later on may depend on these modifications. For instance, when a method action introduces a new proof line, which is used later on by another action, then the second action is not possible without the first action. In the following definition, we shall define for the different kinds of strategic actions and for method actions which other actions in an action sequence depend on them.

Definition Let A⃗ be a sequence of actions with

A⃗=[A_{1}, …, A_{i−1}, A_{i}, A_{i+1}, …, A_{n}].

The set of actions in A⃗, which depend on A_{i} is defined for the different kinds of actions in Multi as follows.

Method Action: Let A_{i} be a method action with the ⊖ conclusions ⊖Concs, the ⊕ conclusions ⊕Concs, and the ⊕ premises ⊕P rems. If A_{i} contains some binding constraints, then {A_{i+1}, …, A_{n}} depend on A_{i}. Otherwise, A_{j} ∈ {A_{i+1}, …, A_{n}} depends on A_{i} if:

1. A_{j} is a method action whose sets of conclusions or premises contains a proof line of ⊕Concs or ⊕P rems (which are the new proof lines introduced by A_{i}),

2. A_{j} is an InstMeta action, which tackles an instantiation-task whose meta-variable is introduced by A_{i},

3. A_{j} is an Exp action, which tackles an expansion-task whose proof line is in ⊖Concs or ⊕Concs (the proof lines closed by A_{i}),

4. A_{j} is an ATPaction, which tackles a line-task that contains either as support or as conclusion a proof line of ⊕Concs or ⊕P rems, 5. A_{j} is a PPlanner or CPlanner action, which contains an action that depends

on A_{i}.

InstMeta Action: Let A_{i} be an InstMeta action. Then {A_{i+1}, …, A_{n}} depend on A_{i}.

ATPAction: Let A_{i} be an ATPaction. A_{j} ∈ {A_{i+1}, …, A_{n}} depends on A_{i} if A_{j} is an Exp action, which tackles the expansion-task with the proof line closed by A_{i}.

ExpAction: Let A_{i} be an Expaction with the set L_{new} of new proof lines in the proofsegment. Let T = L|^{Exp} be the task of A_{i}. Then A_{j} ∈ {A_{i+1}, …, A_{n}} depends on A_{i} if

1. A_{j} is a method action, which contains either as conclusion or as premise a proof line of L_{new}, or which contains L as ⊖ conclusion,^{28}

2. A_{j} is an InstMeta action, which tackles an instantiation-task whose meta-variable is introduced by A_{i},

3. A_{j} is an Expaction, which tackles an expansion-task whose proof line is in L_{new},

4. A_{j} is an ATPaction, which tackles a line-task that contains a proof line of L_{new} either as support or as goal, or which tackles a line-task whose goal is L,^{28}

5. A_{j} is a PPlanner or CPlanner action, which contains an actions that depends on A_{i}.

CPlanner or PPlanner Action: Let A_{i} be a CPlanner or a PPlanner action whose sequence of actions is [A′_{1}, …, A′_{m}]. Then A_{j} ∈ {A_{i+1}, …, A_{n}} depends on A_{i} if there

is an action A′_{k} ∈ [A′_{1}, …, A′_{m}] such that A_{j} depends on A′_{k}.

Finally, we have to define which actions of an action sequence depend on an action that is contained within a CPlanner or PPlanner action: Let A_{i} be a CPlanner or PPlanner action with action sequence:

[A′_{1}, …, A′_{i−1}, A′_{i}, A′_{i+1}, …, A′_{n}].

Then the set of actions that depend on A′_{i} with respect to A⃗ is the set of actions that depend on A′_{i} with respect to the action sequence [A_{1}, …, A_{i−1}] ∪ [A′_{1}, …, A′_{i−1}, A′_{i}, A′_{i+1}, …, A′_{n}] ∪ [A_{i+1}, …, A_{n}].

Note that with this definition all actions succeeding an action that introduces new bindings (i.e., method actions with bindings and InstMeta actions) depend on this action. We use now the notion of dependency of actions to define when an action is deletable with respect to an action sequence.

Definition Let A⃗ be a sequence of actions with

A⃗=[A_{1}, …, A_{i−1}, A_{del}, A_{i+1}, …, A_{n}].

A_{del} is deletable with respect to A⃗ if the set of actions in A⃗ that depend on A_{del} is empty.

28 If A_{i} opens L again, then L can be closed again later on by another method action.

Next, we define the functions Φ_{Multi}^{−1} and Φ⃗_{Multi}^{−1}, which delete actions.^{29} We give first the general outline of Φ_{Multi}^{−1} and define the recursive Φ⃗_{Multi}^{−1}. Afterwards, we define Φ_{Multi}^{−1} for the different kinds of actions.

Definition The action deletion function Φ_{Multi}^{−1} is a partial function that maps a sequence of actions, an agenda, a PDS, a sequence of binding stores and an action into a sequence of actions, an agenda, a PDS, and a sequence of binding stores, i.e.,

Φ_{Multi}^{−1} : A⃗ × Â × P × B⃗S × A_{del} ↦ A⃗’ × Â’ × P’ × B⃗S’.

The recursive action deletion function Φ⃗_{Multi}^{−1} is a partial function that maps a sequence of actions, an agenda, a PDS, a sequence of binding stores, and a sequence of actions into a sequence of actions, an agenda, a PDS, and a sequence of binding stores, i.e.,

Φ⃗Multi^{−1} : A⃗ × Â × P × B⃗S × A⃗_{del} ↦ A⃗’ × Â’ × P’ × B⃗S’.

Φ⃗_{Multi}^{−1} is recursively defined as follows. Let A⃗ be a sequence of actions, Â an agenda, P a PDS, B⃗S a sequence of binding stores, and A⃗_{del} a sequence of actions.

1. If A⃗_{del} is empty, then Φ⃗_{Multi}^{−1}(A⃗, Â, P, B⃗S, A⃗_{del}) := (A⃗, Â, P, B⃗S).

2. Otherwise let A_{del} := first(A⃗_{del}) and A⃗’_{del} := rest(A⃗_{del}). If A_{del} is in A⃗ or part of a CPlanner or PPlanner action in A⃗ and A_{del} is deletable with respect to A⃗, then Φ⃗_{Multi}^{−1}(A⃗, Â, P, B⃗S, A⃗_{del}) := Φ⃗_{Multi}^{−1}(Φ_{Multi}^{−1}(A⃗, Â, P, B⃗S, A_{del}), A⃗’_{del}).

In the single definitions of the function Φ_{Multi}^{−1} for the different kinds of actions we describe the modifications of the sequence of actions, the agenda, the PDS, and the sequence of binding stores caused by the deletion of a respective action. Although the notion of deletability of an action is only defined with respect to a sequence of actions, we assume that the agenda, the PDS, and the sequence of binding stores are not arbitrary, but created by this sequence of actions (in particular, by the action that should be deleted).

We start with the definition of Φ_{Multi}^{−1} for method actions. Since in Multi the action sequences consist only of strategic actions, a method action can occur only within a PPlanner or CPlanner action. Hence, the following definition describes the deletion of a method action within a PPlanner or CPlanner action.

Definition Let A⃗ be a sequence of actions and let A_{del} be a method action, which is in an PPlanner or CPlanner action A_{planner} in A⃗, i.e., A⃗=[A_{1}, …, A_{i−1}, A_{planner}, A_{i+1}, …, A_{n}]. Let B⃗S be a sequence of bindings stores, P a PDS, and Â an agenda. Moreover, let ⊕Concs be the ⊕ conclusions, ⊖Concs the ⊖ conclusions, ⊕P rems the ⊕ premises, ⊖P rems the ⊖ premises, and BP rems the blank premises of A_{del}. Let T = L ◀ SUPPS_{L} be the task of A_{del} and let σ be the binding constraints of A_{del}. P rems:=⊕P rems ∪ ⊖P rems ∪ BP rems, Concs:=⊕Concs ∪ ⊖Concs Lines-T o-Remove:=⊕Concs ∪ ⊕P rems Old-Line-T asks:=[L′ ◀ SUPPS_{L′} | L′ ∈ ⊕P rems]. Old-Inst-T asks:=[mv|^{Inst} | mv ∈ New-Lines and nowhere else in P]. Old-Exp-T asks:=[C|^{Exp} | C in Concs]. T asks-T o-Remove:= Old-Line-T asks ∪ Old-Inst-T asks ∪ Old-Exp-T asks. New-Inst-T asks:=[mv|^{Inst} | mv bound inσ]. New-T asks:=[T] ∪ New-Inst-T asks.

29Since action deletion is conceptually the inverse operation of action introduction we call these functions ΦMulti^{−1} and Φ⃗Multi^{−1} although technically they are not the inverse functions of Φ_{Multi} and Φ⃗_{Multi}.

If A_{del} is deletable with respect to A⃗ and if Â, P, and B⃗S resulted from the introduction of A⃗ (to some agenda, PDS, and sequence of binding stores), then the result (A⃗’, Â’, P’, B⃗S’) of Φ_{Multi}^{−1}(A⃗, Â, P, B⃗S, A_{del}) is defined by:

• A⃗’:= [A_{1}, …, A_{i−1}, A′_{planner}, A_{i+1}, …, A_{n}] where A′_{planner} results from A_{planner} by removing A_{del} from the sequence of actions of A_{planner}.

• Â’:= New-T asks ∪ (Â − T asks-T o-Remove).

• P’ results from P by

1. removing the lines Lines-T o-Remove and

2. justifying the proof lines ⊖Concs with Open, respectively.

• If σ is empty, then B⃗S’:=B⃗S, otherwise B⃗S’:=B⃗S − last(B⃗S).^{30}

Definition Let A⃗ be a sequence of actions and let A_{del} be an InstMeta action in A⃗. Let B⃗S be a sequence of bindings stores, P a PDS, and Â an agenda.

If A_{del} is deletable with respect to A⃗ and if Â, P, and B⃗S resulted from the introduction of A⃗ (to some agenda, PDS, and sequence of binding stores), then the result (A⃗’, Â’, P’, B⃗S’) of Φ_{Multi}^{−1}(A⃗, Â, P, B⃗S, A_{del}) is defined by:

• A⃗’:=A⃗ − A_{del}.

• Â’:=Â ∪ [T] where T is the task of A_{del}.

• P’:=P.

• B⃗S’:=B⃗S − last(B⃗S).

30If σ is not empty, then the last binding store in B⃗S has to be the binding store resulting from the introduction of A_{del} since otherwise A_{del} would not be deletable. Thus, when A_{del} is deleted, then the last binding store has to be removed.

Definition Let A⃗ be a sequence of actions and let A_{del} be an ATPaction in A⃗. Let B⃗S be a sequence of bindings stores, P a PDS, and Â an agenda. Let T = L ◀ SUPPS_{L} be the task of A_{del}.

If A_{del} is deletable with respect to A⃗ and if Â, P, and B⃗S resulted from the introduction of A⃗ (to some agenda, PDS, and sequence of binding stores), then the result (A⃗’, Â’, P’, B⃗S’) of Φ_{Multi}^{−1}(A⃗, Â, P, B⃗S, A_{del}) is defined by:

• A⃗’:=A⃗ − A_{del}.

• Â’:=(Â ∪ [T]) − L|^{Exp}.

• P’ results from P by opening the line L.

• B⃗S’:=B⃗S.

Definition Let A⃗ be a sequence of actions and let A_{del} be an Expaction in A⃗. Let B⃗S be a sequence of bindings stores, P a PDS, and Â an agenda. Moreover, let T = L|^{Exp} be the task of A_{del} and (J P_{1} … P n) the justification of L at the next higher level of abstraction (i.e., the justification of L before A_{del} was performed). Lines-T o-Remove:={L′|L′ ∈ expansion-segment of A_{del}} − {L, P_{1}, …, P_{n}}. New-T asks:=[T]. Old-Open-Lines:={L′|L′ ∈ open-lines ofA_{add}}. Old-Line-T asks:=[L′ ◀ SUPPS_{L′} | L′ in Old-Open-Lines]. Old-Inst-T asks:=[mv|^{Inst} | mv ∈ Lines-T o-Remove and nowhere else in PDS]. Old-Exp-T asks:=

[L′|^{Exp} |(L′ ∈ Lines-T o-Remove or L′ = L) and L′ closed by tactic].

T asks-T o-Remove:= Old-Line-T asks ∪ Old-Inst-T asks ∪ Old-Exp-T asks.

If A_{del} is deletable with respect to A⃗ and if Â, P, and B⃗S resulted from the introduction of A⃗ (to some agenda, PDS, and sequence of binding stores), then the result (A⃗’, Â’, P’, B⃗S’) of Φ_{Multi}^{−1}(A⃗, Â, P, B⃗S, A_{del}) is defined by:

• A⃗’:=A⃗ − A_{del}.

• Â’:= New-T asks ∪ (Â − T asks-T o-Remove).

• P’ results from P by

1. removing the current justification from L and setting (J P_{1} … P n) as the current one, and

2. removing the proof lines in New-Lines.

• B⃗S’:=B⃗S.

Definition Let A⃗ be a sequence of actions and let A_{del} be a CPlanner or a PPlanner action in A⃗. Let B⃗S be a sequence of bindings stores, P a PDS, and Â an agenda. Moreover, let [A_{1}, …, A_{n}] be the action-sequence of A_{del}. (A⃗_{rec}, Â_{rec}, P_{rec}, B⃗S_{rec}) := Φ⃗_{Multi}^{−1}(A⃗, Â, P, B⃗S, [A_{n}, …, A_{1}])

If A_{del} is deletable with respect to A⃗ and if Â, P, and B⃗S resulted from the introduction of A⃗ (to some agenda, PDS, and sequence of binding stores), then the result (A⃗’, Â’, P’, B⃗S’) of Φ_{Multi}^{−1}(A⃗, Â, P, B⃗S, A_{del}) is defined by:

• A⃗’:= A⃗_{rec} − [A_{del}].^{31}

• Â’:= Â_{rec}.

• P’:= P_{rec}.

• B⃗S’:=B⃗S_{rec}.

With these definitions at our disposal, we can now describe the BackTrack algorithm. Figure 32 contains a pseudo-code description of BackTrack. BackTrack obtains two arguments. First, a pair (S, T), which consists of a BackTrack strategy S and a task T. Second, the list of all alternative job offers on the control blackboard, when the BackTrack strategy was invoked. BackTrack returns no specific output but updates the content of the proof blackboard.

Step 1 applies the computation function of the strategy S to the task T. This returns a sequence of actions that BackTrack should delete, and BackTrack binds the algorithm variable A⃗_{del} to this action sequence. Moreover, BackTrack writes a backtrack-start entry with this information to the history.

The steps 2-5 are essentially a while-loop, which is passed through until A⃗_{del} is empty. First, Step 2 checks whether A⃗_{del} is empty. If this is the case, it creates a success message,^{32} writes a backtrack-stop entry with this message to the history, and terminates. Otherwise, step 3 picks the first action from A⃗_{del} and stores it in the algorithm variable A_{del}. A_{del} is then either deleted in step 5 or step 4 extends A⃗_{del} depending on A_{del}. Step 4 first checks whether A_{del} is deletable with respect to the sequence of actions on the proof blackboard. If this is not the case, then there are actions which depend on A_{del} and step 4 adds these actions, which are computed by the function dependend-actions , in front of A⃗_{del}. If A_{del} is deletable, then step 4 checks next whether it is an action of PPlanner or CPlanner whose action-sequence is not empty. If this holds, then it adds the action sequence of A_{del} in front of A⃗_{del}. Otherwise, step 5 is reached, which uses Φ_{Multi}^{−1} to delete A_{del} and to update the action sequence, the agenda, the PDS, and the sequence of binding stores on the proof blackboard. Moreover, it adds an action-deletion entry to the history and removes A_{del} from A⃗_{del}.

If the deleted action A_{del} belongs to a terminated PPlanner or CPlanner strategy execution (this is checked by the function action-of-terminated-strategy), then a re-invocation

31When all actions in A_{del} are deleted, then A_{del} remains with an empty action sequence. Here A_{del} itself is deleted from the action sequence.

32Note that BackTrack is not supposed to fail (except of hopefully not occurring programming errors).

Input: (1) a pair (S, T) where S is a BackTrack strategy and T is a task, (2) the list of all alternative job offers J.

Output: No output, only changes of the blackboards.

Algorithm: BackTrack((S, T), J)

1. Compute Actions To Be Deleted Let A⃗_{del}:=apply(compute-del-actions-function (S), T). add-backtrack-start-record-to-history(J , A⃗_{del}).

2. Terminate

If A⃗_{del}=∅

then Let message:=create-success-message (S, T). add-backtrack-stop-record-to-history(message). Terminate.

3. Select Action Let A_{del}:=first(A⃗_{del}).

4. Extend Actions

If A_{del} is not deletable wrt. the sequence of actions on PB

then A⃗_{del}:=dependend-actions (A_{del}) ∪ A⃗_{del}. Goto step 3.

If A_{del} is CPlanner or PPlanner action, whose action-sequence is not empty

then A⃗_{del}:=action-sequence (A_{del}) ∪ A⃗_{del}. Goto step 3.

5. Delete Action PB:=Φ_{Multi}^{−1}(A_{del}, P B). add-action-del-record (A_{del}). Let A⃗_{del}:=A⃗_{del} − [A_{del}]. If action-of-terminated-strategy(A_{del})

then

write-to-memory(get-tasktag(A_{del}), ∅). Goto step 2.

Figure 32: The BackTrack algorithm.

of this strategy execution should be enabled again. BackTrack re-activates the strategy execution by writing an entry to the memory consisting of the task tag of the strategy execution (which is computed by the function get-tasktag from the history) and an empty set of demand pointers. From this memory entry the terminated strategy execution can be re-invoked.

Note that BackTrack could apply Φ_{Multi}^{−1} directly to actions of PPlanner and CPlanner that are not empty (since we did define Φ_{Multi}^{−1} for such actions in definition 5.5.7). However, BackTrack first successively deletes the action sequence of an action of PPlanner and CPlanner before it deletes the “empty” PPlanner or CPlanner action. This guarantees that detailed history information for each deleted action is created (i.e, for each action, which is in the action-sequence of an action of PPlanner or CPlanner as well as for the PPlanner or CPlanner action itself).

5.6 Remarks

5.6.1 Representing the Search with Trees

The check for dependency among actions as well as the changes caused by backtracking of an action are complex operations as described in the previous section. The problem is that the PDS, which is the central data structure in the current implementation of Ωmega and Multi, is a complex data structure difficult to maintain. In the ongoing re-implementation of the Ωmega system on top of the CORE system [4] we suggest an agenda as the (only) central data structure. Moreover, we suggest additional data structures to considerably simplify the backtracking of actions.

The introduction of an action into a strategic proof plan reduces a task to a set of tasks, which can be empty. The introduced actions and the resulting tasks could be stored in a tree, a so-called task-action-tree, whose nodes are labeled with the tasks and whose edges are labeled with the actions.^{33} Figure 33 depicts such a task-action-tree. The root node of the tree is labeled with the initial task. If this tree is constructed during the strategic proof planning process, then the current agenda consists always of the tasks of the leave nodes of the tree.

With a task-action-tree the dependency among actions could be formulated as follows: An action A_{i} depends on another action A_{j} if the path from the root node to A_{i} contains A_{j}. The changes caused by the backtracking of an action could also be stated simpler than currently: If a deletable action A is backtracked, then the children tasks of the action A are removed and the parent task is introduced again into the agenda.

5.6.2 Creating Different Kinds of Solution Proof Plans

In section 5.3, we defined three different notions of strategic solution proof plans, namely method-level solution proof plans, instantiated method-level solution proof plans, and full solution proof plans. In order to produce a method-level solution proof plan Multi can ignore the instantiation tasks and the expansion-tasks; to produce an instantiated methodlevel solution proof plans Multi can ignore only the expansion-tasks; to create a full solution proof plan Multi has to tackle all kinds of tasks.

The simplest possibility to make Multi search for a particular kind of solution proof plan is to prohibit some strategies. For instance, if there are no strategies of Exp, then

33Actually, we use multi-edges that connect one parent node with several children nodes.

Figure 33: A task-action-tree.

expansion-tasks will be ignored and Multi will search for an instantiated method-level solution proof plan. In the case studies it turned out that this approach has the drawback that expansion-tasks are created although they are ignored later on. Therefore, we avoid the creation of not desired expansion-tasks. The user can declare methods or tactics whose applications he wants to be expanded by Multi as not-reliable. Multi creates expansiontasks only for such proof lines L whose justification (J P_{1} … P_{N}) uses a not-reliable method or tactic J.

5.6.3 Cooperation with Constraint Solvers

So far, the only constraint solver connected with Multi is CoSIE. Multi communicates directly with CoSIE by interfaces in methods and strategies. When a method action is introduced that contains constraints for CoSIE, then these constraints are passed to CoSIE. Moreover, the two strategies InstIfDetermined and ComputeInstFromCS employ CoSIE to obtain new bindings. If several constraint solvers should be connected with Multi, then a direct communication is not sufficient anymore. First, constraints should be passed to all connected constraint solvers for which they are relevant. Second, several constraint solvers should be able to directly exchange results without involving Multi.

As possible solution we suggest a constraint solver coordination module, which handles all communication and which stores all constraints and results. Each constraint solver that should be connected has to register by the coordination module. Multi passes new constraints to this module. Then, the module asks the connected constraints solvers whether this constraint is relevant for them and passes it to the relevant constraint solvers. The module performs the same distribution, if a constraint solver produces an intermediate result (i.e., when CoSIE detects that the instantiation of meta-variable mv is already determined by its current constraints). When Multi backtracks and deletes some method actions with constraints, then the coordination module has also to organize the deletion of the constraints in the affected constraint solvers and the deletion of intermediate that depend on these constraints.

The module handles and distributes also queries of Multi. Multi passes queries (e.g., is the instantiation of meta-variable mv already determined?) only to the coordination module. Either the coordination module can answer the query directly (e.g., if an result passed by a connected constraint solver was already a unique instantiation for mv) or it distributes the query to the connected constraint solvers and passes the answer back to Multi.

5.6.4 Dependencies in Backtracking

When the BackTrack algorithm removes an action, then it also removes all actions that depend on this action (see section 5.5.7). The notion of dependency for actions used by BackTrack (see definition 5.5.7) is strict and therefore BackTrack may removes more actions than necessary. In particular, the deletion of an InstMeta action causes the deletion of all actions following this action in the current action sequence. We decided for this approach since a more detailed analysis of which following actions actually depend on a new binding is difficult and is still open.

Nevertheless, there are also dependencies between actions that are not covered by the dependency notion in definition 5.5.7. In particular, there can be various dependencies between actions that involve cooperation with constraint solvers (e.g., CoSIE). For instance, if the current constraints (e.g., mv ≤ t and mv ≥ t) in CoSIE determine the instantiation t for a meta-variable mv, then the strategy InstIfDetermined is applicable with respect to mv and introduces the binding mv:=^{b} t into the strategic proof plan. Other actions can rely on this binding. When a method action that contains constraints for CoSIE is backtracked, then mv may is not longer determined with respect to the resulting constraint store (e.g., if the constraint mv ≤ t is removed). In this case, the action of InstIfDetermined, which binds mv to t, has to be removed. Since this is not a problem of strategies of InstMeta in general but of ComputeInstFromCS in particular, we did not implement such a dependency analysis into the BackTrack algorithm (i.e., it is not contained in the dependency notion introduced in definition 5.5.7). Rather we suggest to check such particular dependencies in strategic control rules that cause further backtracking.

The described situation is handled by the strategic control rule check-det-insts. check-det-insts checks whether the last strategy execution was a BackTrack step and whether it removed some method actions with constraints for CoSIE. If this is the case, it checks whether all actions of InstIfDetermined in the current sequence of actions are still valid in the sense that the meta-variables that they bind are still determined in CoSIE. Then, check-det-insts prefers backtracking for each action of InstIfDetermined that is no longer valid.

5.6.5 Failure Information in Execution Messages

When a strategy execution fails, then its algorithm creates a failure message. If possible the algorithm can attach information to a failure message, which can also be used by the control rules. For instance, PPlanner can create and attach information why no applicable action could be found. This functionality affects many single steps in PPlanner and in the procedures ChooseAction and ChooseActionAll , which compute and select the next action to be applied. Hence, for the sake of simplicity and clarity, we did not describe this functionality in the algorithms themselves but give an informal description here.

That the procedures ChooseAction and ChooseActionAll fail to to provide an action for a line-task T and a method M can be caused by three reasons:

Failed matching of proof lines The ⊖ conclusions of M do not match with the task line of T or the blank and ⊖ premises of M do not match with the supports of T.

Failed application conditions The evaluation of the application conditions of M can fail with respect to the substitution resulting from a successful matching of the proof lines of M with the task line and the supports of T.

Rejected actions Actions can be rejected by control rules or because they were already applied and then backtracked later on.

These tests are performed successively in ChooseAction and ChooseActionAll in this order. Each time such a test fails, the function that performs the test creates an information record. For instance, when the function eval-appl-conds finds that the application condition App_{c} of method M fails with respect to the incomplete action A (which resulted from the successful matching of the proof lines of M with the proof lines of the given task), then eval-appl-conds creates the information record applcondfailure(App_{c}, M, A). ChooseAction and ChooseActionAll collect these information records and return them to PPlanner. If there is no applicable action, then PPlanner attaches the set of information records to the created failure message. Sample applications of Multi that make use of such failure information are given in [35].

6 Conclusion

We presented the technical concepts underlying proof planning in the Ωmega system and gave detailed descriptions of the two proof planners in Ωmega, the simple proof planner PLAN and the multi-strategy proof planner Multi. As sample application we discussed the application of both planners to the LIM+ example from the limit domain.

Since the LIM+ example can be solved by both planners it does not point out the advantages of proof planning with multiple-strategies as opposed to simple proof planning. We refer the interested reader to [34, 35] for a discussion of problems of the limit domain that cannot be solved by PLAN but by Multi. The reason is that Multi enables the flexible combination of different proof plan refinements (in particular flexible backtracking and meta-variable instantiation) guided by meta-reasoning. For further discussion of the application of PLAN to the limit domain see in the master thesis of Jürgen Zimmer [65] as well as in [42, 41, 45].

Further case studies performed with Multi include applications to residue class problems [39, 36, 37, 38], to permutation group problems [13], and to the \sqrt{2}-is-irrational problem and similar problem [57]. A recent application of Multi is its incorporation into the tutor system ActiveMath [43] where it serves as the module to teach mathematical theorem proving [40]. In this application Multi is not used as automated component (as in the other listed applications) but as mixed-initiative component that communicates with the user and incorporates the user to take decisions, i.e., which proof plan refinement to perform next.

91

A ChooseActionAll Algorithm

Input: (1) a task T, (2) a history H⃗, (3) a list of methods M, (4) a list of control rules C.

Output: Either a pair of an action and a list of actions or fail.

Algorithm: ChooseActionAll(T,H⃗,M,C) Let T =L_{open} ◀ SUPPS_{L_{open}}.

1. Order Methods Methods:= evalcrules-methods (M,C,T). Let Methods = [M_{1}, …, M_{n}]. When Methods empty then terminate and return fail. Actions_{1}:=initial-action-set(T, M_{1}).

⋮

Actions_{n}:=initial-action-set(T, M_{n}).

2. Handle Task, Supports, Parameters, and Appl. Conditions For i = 1 to n:

(a) Match Task Line Let ⊖Concs_{i} the ⊖ conclusions of M_{i}. Actions_{i}:=match-task-line(L_{open},⊖Concs_{i},Actions_{i}).

(b) Select and Match Supports and Parameters Let ⊖P rems_{i} and BP rems_{i} the ⊖ premises and blank premises of M_{i}. Let P arams_{i} the parameter variables of M_{i}. Supps+P arams_{i}:=evalcrules-s+p (SUPPS_{L_{open}},C,T,M_{i},Actions_{i}). Actions_{i}:= match-s+p (Supps+P arams_{i},⊖P rems_{i} ∪ BP rems_{i},

P arams_{i},Actions_{i}).

(c) Evaluate Application Conditions Actions_{i}:=eval-appl-conds (Actions_{i},M_{i}).

Actions:=Actions_{1} ∪ … ∪ Actions_{n}. When Actions empty then terminate and return fail.

3. Outline Computations eval-outline-computations(Actions). complete-outline (Actions).

4. Choose Action Actions:=remove-backtracked (Actions,H⃗). Actions:=evalcrules-actions (Actions,C). If Actions = ∅

then Terminate and return fail.

else Terminate and return first(Actions).

Figure 34: The ChooseActionAll algorithm.

B Lim+ Example

Lim_{f}. Lim_{f}  ⊢ lim_{x→a} f(x) = l_{f}  (Hyp)
Lim_{g}. Lim_{g} ⊢ lim_{x→a} g(x) = l_{g}  (Hyp)

L_{2}. Lim_{f} ⊢ ∀ϵ_{1} (0 < ϵ_{1} ⇒ ∃δ_{1} (0 < δ_{1} ∧ ; ∀x_{1} (|x_{1}−a| < δ_{1}∧|x_{1}−a| > 0 ; ⇒ |f(x_{1}) − l_{f}| < ϵ_{1}))) (DefnUnfold-F Lim_{f})

L_{3}. Lim_{g} ⊢ ∀ϵ_{2} (0 < ϵ_{2} ⇒ ∃δ_{2} (0 < δ_{2} ∧ ; ∀x_{2} (|x_{2}−a| < δ_{2}∧|x_{2}−a| > 0 ; ⇒ |g(x_{2}) − l_{g}| < ϵ_{2}))) (DefnUnfold-F Lim_{g})

L_{17}.  Lim_{f}  ⊢ 0 < mv_{ϵ_{1}} ⇒ ∃δ_{1} (0 < δ_{1} ∧ ; ∀x_{1} (|x_{1}−a| < δ_{1}∧|x_{1}−a| > 0 ; ⇒ |f(x_{1}) − l_{f}| < mv_{ϵ_{1}})) (∀E-F L_{2})
L_{18}.  H_{3}  ⊢ 0 < mv_{ϵ_{1}}  (TellCS-B)
L_{20}.  H_{3}  ⊢ ∃δ_{1} (0 < δ_{1} ∧ ∀x_{1} (|x_{1} − a| < δ_{1} ; ∧ |x_{1} − a| > 0 ⇒ |f(x_{1}) − l_{f}| < ; mv_{ϵ_{1}})) (⇒_{E} L_{18} L_{17})
L_{21}.  L_{21}  ⊢ 0 < c_{δ_{1}} ∧ ∀x_{1} (|x_{1} − a| < c_{δ_{1}} ∧ |x_{1} − ; a| > 0 ; ⇒ |f(x_{1}) − l_{f}| < mv_{ϵ_{1}}) (Hyp)
L_{23}.  L_{21}  ⊢ 0 < c_{δ_{1}}  (∧E-F L_{21})
L_{24}.  L_{21}  ⊢ {∀x_{1} (|x_{1} − a| < c_{δ_{1}} ∧ |x_{1} − a| > 0 \atop ⇒ |f(x_{1}) − l_{f}| < mv_{ϵ_{1}})} (∧E-F L_{21})
L_{25}.  L_{21}  ⊢ {|mv_{x_{1}} − a| < c_{δ_{1}} ∧ |mv_{x_{1}} − a| > 0 \atop ⇒ |f(mv_{x_{1}}) − l_{f}| < mv_{ϵ_{1}}))} (∀E-F L_{24})
L_{38}.  Lim_{g} ⊢ 0 < mv_{ϵ_{2}} ⇒ ∃δ_{2} (0 < δ_{2} ∧ ; ∀x_{2} (|x_{2}−a| < δ_{2}∧|x_{2}−a| > 0 ; ⇒ |g(x_{2}) − l_{g}| < mv_{ϵ_{2}})) (∀E-F L_{3})
L_{39}.  H_{3}  ⊢ 0 < mv_{ϵ_{2}}  (TellCS-B)
L_{41}.  H_{3}  ⊢ {∃δ_{2} (0 < δ_{2} ∧ ∀x_{2} (|x_{2} − a| < δ_{2} \atop ∧|x_{2}−a| > 0 ⇒ |g(x_{2})−l_{g}| < mv_{ϵ_{2}}))} (⇒_{E} L_{39} L_{38})
L_{42}.  L_{42}  ⊢ 0 < c_{δ_{2}} ∧ ∀x_{2} (|x_{2} − a| < c_{δ_{2}} ∧ |x_{2} − ; a| > 0 ; ⇒ |g(x_{2}) − l_{g}| < mv_{ϵ_{2}}) (Hyp)
L_{44}.  L_{42}  ⊢ 0 < c_{δ_{2}}  (∧E-F L_{42})
L_{45}.  L_{42}  ⊢ {∀x_{2} (|x_{2} − a| < c_{δ_{2}} ∧ |x_{2} − a| > 0 \atop ⇒ |g(x_{2}) − l_{g}| < mv_{ϵ_{2}})} (∧E-F L_{42})
L_{46}.  L_{42}  ⊢ {|mv_{x_{2}} − a| < c_{δ_{2}} ∧ |mv_{x_{2}} − a| > 0 \atop ⇒ |g(mv_{x_{2}}) − l_{g}| < mv_{ϵ_{2}}))} (∀E-F L_{45})
L_{11}.  L_{11}  ⊢ |c_{x} − a| > 0 ∧ |c_{x} − a| < mv_{δ}  (Hyp)
L_{14}.  L_{11}  ⊢ |c_{x} − a| > 0  (∧E-F L_{11})
L_{13}.  L_{11}  ⊢ |c_{x} − a| < mv_{δ}  (∧E-F L_{11})
L_{5}.  L_{5}  ⊢ 0 < c_{ϵ}  (Hyp)
L_{61}.  H_{1}  ⊢ 0 ≤ 0  (AskCS-B)
L_{59}.  H_{1}  ⊢ mv_{δ} ≤ c_{δ_{1}}  (TellCS-B)
L_{57}.  H_{2}  ⊢ 0 ≤ 0  (AskCS-B)
L_{55}.  H_{2}  ⊢ mv_{δ} ≤ c_{δ_{2}}  (TellCS-B)
L_{52}.  H_{2}  ⊢ mv_{x_{2}} = c_{x}  (TellCS-B)

L_{53}.  H_{2}  ⊢ mv_{ϵ_{2}} ≤ \frac{1}{2} ∗ c_{ϵ}  (TellCS-B)
L_{50}.  H_{2}  ⊢ |mv_{x_{2}} − a| < c_{δ_{2}}  (Solve*-B L_{13} L_{55})
L_{51}.  H_{2}  ⊢ |mv_{x_{2}} − a| > 0  (Solve*-B L_{14} L_{57})
L_{47}.  H_{2}  ⊢ |mv_{x_{2}} − a| < c_{δ_{2}} ∧ |mv_{x_{2}} − a| > 0  (∧I-B L_{50} L_{51})
L_{49}.  H_{2}  ⊢ |g(mv_{x_{2}}) − l_{g}| < mv_{ϵ_{2}}  (⇒_{E} L_{47} L_{46})
L_{48}.  H_{2}  ⊢ |g(c_{x}) − l_{g}| < \frac{1}{2} ∗ c_{ϵ}  (Solve*-B L_{49} L_{52} L_{53})
L_{43}.  H_{2}  ⊢ |g(c_{x}) − l_{g}| < \frac{1}{2} ∗ c_{ϵ}  (⇒E-F L_{47} L_{46} L_{48})
L_{40}.  H_{1}  ⊢ |g(c_{x}) − l_{g}| < \frac{1}{2} ∗ c_{ϵ}  (∃E-F L_{41} L_{43})
L_{37}.  H_{1}  ⊢ |g(c_{x}) − l_{g}| < \frac{1}{2} ∗ c_{ϵ}  (⇒E-F L_{39} L_{38} L_{40})
L_{31}.  H_{1}  ⊢ |1| ≤ mv  (TellCS-B)
L_{32}.  H_{1}  ⊢ mv_{ϵ_{1}} ≤ \frac{c_{ϵ}}{2∗mv}  (TellCS-B)

L_{33}. H_{1} ⊢ |g(c_{x}) − l_{g}| < \frac{c_{ϵ}}{2} (Simplify-B L_{37})

L_{34}.  H_{1}  ⊢ 0 < mv  (TellCS-B)
L_{35}.  H_{1}  ⊢ mv_{x_{1}} = c_{x}  (TellCS-B)
L_{29}.  H_{1}  ⊢ |mv_{x_{1}} − a| < c_{δ_{1}}  (Solve*-B L_{13} L_{59})
L_{30}.  H_{1}  ⊢ |mv_{x_{1}} − a| > 0  (Solve*-B L_{14} L_{61})
L_{26}.  H_{1}  ⊢ |mv_{x_{1}} − a| < c_{δ_{1}} ∧ |mv_{x_{1}} − a| > 0  (∧I-B L_{29} L_{30})
L_{28}.  H_{1}  ⊢ |f(mv_{x_{1}}) − l_{f}| < mv_{ϵ_{1}}  (⇒_{E} L_{26} L_{25})

L_{27}.

H_{1} ⊢

|((f(c_{x}) + g(c_{x})) − l_{f}) − l_{g}| < c_{ϵ}

(ComplexEstimate-B

L_{28} L_{31} L_{32} L_{33} L_{34} L_{35})

L_{22}.  H_{1}  ⊢ |((f(c_{x}) + g(c_{x})) − l_{f}) − l_{g}| < c_{ϵ}  (⇒E-F L_{26} L_{25} L_{27})
L_{19}.  H_{3}  ⊢ |((f(c_{x}) + g(c_{x})) − l_{f}) − l_{g}| < c_{ϵ}  (∃E-F L_{20} L_{21})
L_{16}.  H_{3}  ⊢ |((f(c_{x}) + g(c_{x})) − l_{f}) − l_{g}| < c_{ϵ}  (⇒E-F L_{18} L_{17} L_{19})

L_{12}. H_{3} ⊢ |(f(c_{x}) + g(c_{x})) − (l_{f} + l_{g})| < c_{ϵ} (Simplify-B L_{16})

L_{10}.  H_{4}  ⊢ {|c_{x} − a| < mv_{δ} ∧ |c_{x} − a| > 0 \atop ⇒ |(f(c_{x}) + g(c_{x})) − (l_{f} + l_{g})| < c_{ϵ}} (⇒I-B L_{12})
L_{9}.  H_{4}  ⊢ {∀x (|x − a| < mv_{δ} ∧ |x − a| > 0 \atop ⇒ |(f(x) + g(x)) − (l_{f} + l_{g})| < c_{ϵ})} (∀I-B L_{10})
L_{8}.  H_{4}  ⊢ 0 < mv_{δ}  (TellCS-B)
L_{7}.  H_{4}  ⊢ 0 < mv_{δ}∧∀x (|x−a| < mv_{δ}∧|x−a| > ; 0 ; ⇒ |(f(x) + g(x)) − (l_{f} + l_{g})| < c_{ϵ}) (∧I-B L_{8} L_{9})

L_{6}.  H_{4}  ⊢ {∃δ (0 < δ∧∀x (|x−a| < δ∧|x−a| > 0 \atop ⇒ |(f(x) + g(x)) − (l_{f} + l_{g})| < c_{ϵ}))} (∃I-B L_{7})
L_{4}.  Lim_{f} , Lim_{g}⊢ 0 < c_{ϵ} ⇒ ∃δ (0 < δ ∧ ; ∀x (|x − a| < δ ∧ |x − a| > 0 ; ⇒ |(f(x) + g(x)) − (l_{f} + l_{g})| < c_{ϵ})) (⇒I-B L_{6})

L_{1}.  Lim_{f} , Lim_{g}⊢ ∀ϵ (0 < ϵ ⇒ ∃δ (0 < δ ∧ ; ∀x (|x − a| < δ ∧ |x − a| > 0 ; ⇒ |(f(x) + g(x)) − (l_{f} + l_{g})| < ϵ))) (∀I-B L_{4})

LIM+.

Lim_{f} , Lim_{g}⊢

lim_{x→a}(f(x) + g(x)) = l_{f} + l_{g}

(DefnUnfold-B L_{1})

H_{1} = {Lim_{f} , Lim_{g}, L_{5}, L_{11}, L_{21}}, H_{2} = {Lim_{f} , Lim_{g}, L_{5}, L_{11}, L_{21}, L_{42}} H_{3} = {Lim_{f} , Lim_{g}, L_{5}, L_{11}}, H_{4} = {Lim_{f} , Lim_{g}, L_{5}}

References

[1] A.J. Aho, J. Hopcroft, and J. Ullman, editors. Data Structures and Algorithms. Addison-Wesley, 1983.

[2] P.B. Andrews. Transforming Matings into Natural Deduction Proofs. In W. Bibel and R.A. Kowalski, editors, Proceedings of the 5th Conference on Automated Deduction (CADE–5), volume 87 of LNCS, pages 281–292, Les ArcsFrance, June7–9 1980. Springer VerlagGermany.

[3] P.B. Andrews, M. Bishop, S. Issar, D. Nesmith, F. Pfenning, and H. Xi. TPS: A Theorem Proving System for Classical Type Theory. Journal of Automated Reasoning, 16(3):321–353, 1996.

[4] S. Autexier. Hierarchical Contextual Rewriting. PhD thesis, Fachbereich Informatik, Universität des Saarlandes, Saarbrücken, 2003. To appear.

[5] P. Baumgartner and U. Furbach. PROTEIN, A PROver with a Theory INterface. In A. Bundy, editor, Proceedings of the 12th International Conference on Automated Deduction (CADE–12), volume 814 of LNAI, pages 769–773, NancyFrance, June26– July1 1994. Springer VerlagGermany.

[6] C. Benzmüller, M. Bishop, and V. Sorge. Integrating TPS and OMEGA. Journal of Universal Computer Science, 5:188–207, 1999.

[7] W.W. Bledsoe. Challenge Problems in Elementary Analysis. Journal of Automated Reasoning, 6:341–359, 1990.

[8] W.W. Bledsoe, R.S. Boyer, and W.H. Henneman. Computer Proofs of Limit Theorems. Artificial Intelligence, 3(1):27–60, 1972.

[9] A. Bundy. The Use of Explicit Plans to Guide Inductive Proofs. In E.L. Lusk and R.A. Overbeek, editors, Proceedings of the 9th International Conference on Automated Deduction (CADE–9), volume 310 of LNCS, pages 111–120, Argonne, Illinois, USA, 1988. Springer VerlagGermany.

[10] J.G. Carbonell. Derivational Analogy: A Theory of Reconstructive Problem Solving and Expertise Acquisition. In R.S. Michalsky, J.G. Carbonell, and T.M. Mitchell, editors, Machine Learning: An Artificial Intelligence Approach, pages 371–392. Morgan Kaufmann Publ., Los Altos, 1986.

[11] L. Cheikhrouhou and J. Siekmann. Planning Diagonalization Proofs. In F. Giunchiglia, editor, Artificial Intelligence: Methodology, Systems and Applications, Proceedings of the of the 8th International Conference (AIMSA’98), volume 1480 of LNAI, pages 167–180, Sozopol, Bulgaria, September21–23 1998. Springer VerlagGermany.

[12] L. Cheikhrouhou and V. Sorge. PDS — A Three-Dimensional Data Structure for Proof Plans. In Proceedings of the International Conference on Artificial and Computational Intelligence for Decision, Control and Automation in Engineering and Industrial Applications (ACIDCA’2000), Monastir, Tunisia, March22–24 2000.

[13] A. Cohen, S. Murray, M. Pollet, and V. Sorge. Certifying solutions to permutation group problems. In F. Baader, editor, Proceedings of the 19th International Conference on Automated Deduction (CADE–19), number 2741 in LNAI, Miami Beach, Fl, USA, 2003. Springer VerlagGermany.

[14] R.L. Constable, S.F. Allen, H.M. Bromley, R. Cleaveland, J.F. Cremer, R.W. Harper, D.J. Howe, T.B. Knoblock, N.P. Mendler, P. Panangaden, J.T. Sasaki, and S.F. Smith. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, Englewood Cliffs, NJ, USA, 1986.

[15] Coq Development Team. The Coq Proof Assistant Reference Manual. INRIA.

[16] H. de Nivelle. The Bliksem Theorem Prover, Version 1.12. Max-Plank-Institut, Im Stadtwald, Saarbruecken, Germany, October1999. available http://www.mpi-sb.mpg.

de/~bliksem/manual.ps.

[17] M. Drummond. On precondition achievement and the computational economics of automatic planning. In C. Bäckström and E. Sandwall, editors, Current Trends in AI Planning. IOS Press, 1994.

[18] R. Engelmore and T. Morgan, editors. Blackboard Systems. Addison-Wesley, 1988.

[19] L.D. Erman, P. London, and S. Fickas. The Design and an Example Use of HEARSAY-III. In B. Buchanan, editor, Proceedings of the 6th International Joint Conference on Artificial Intelligence (ICJAI), pages 409–415, Tokyo, Japan, August20–23 1979. Morgan Kaufmann.

[20] R.E. Fikes, P.E. Hart, and N.J. Nilsson. Some New Directions in Robot Problem Solving. Machine Intelligence, 7, 1971.

[21] R.E. Fikes and N.J. Nilsson. STRIPS: A New Approach to the Application of Theorem Proving to Problem Solving. Artificial Intelligence, 2:189–208, 1971.

[22] H. Ganzinger, editor. Proceedings of the 16th International Conference on Automated Deduction (CADE–16), volume 1632 of LNAI, Trento, Italy, July7–10, 1999. Springer VerlagGermany.

[23] G. Gentzen. Untersuchungen über das Logische Schließen I und II. Mathematische Zeitschrift, 39:176–210, 405–431, 1935.

[24] M.L. Ginsberg. Dynamic Backtracking. Journal of Artificial Intelligence Research, 1:25—46, 1993.

[25] M.J.C. Gordon and T.F. Melham. Introduction to HOL. Cambridge University Press, Cambridge, UK, 1993.

[26] B. Hayes-Roth. A Blackboard Architecture for Control. Artificial Intelligence, 25:251– 321, 1985.

[27] T. Hillenbrand, A. Jaeger, and B. Löchner. System Description: Waldmeister, Improvements in Performance and Ease of Use. In Ganzinger [22], pages 232 – 236.

[28] S. Kambhampati. Formalizing Dependency Directed Backtracking and Explanationbased Learning in Refinement Search. In W.J. Clancey and D. Weld, editors, Proceedings of the Thirteenth National Conference on Artificial Intelligence (AAAI-96) and Eighth Innovative Applications of Artificial Intelligence Conference (IAAI-96), pages 757–762, Portland, Oregon, USA, August4–8 1996. AAAI Press, Menlo Park, CA, USA.

[29] H. Kirchner and C. Ringeissen, editors. Proceedings of Third International Workshop on Frontiers of Combining Systems (FROCOS 2000), volume 1794 of LNCS, NancyFrance, March22–24 2000. Springer VerlagGermany.

[30] U. Kühler. A Tactic-Based Inductive Theorem Prover for Data Types with Partial Operations. PhD thesis, Sankt Augustin, 2000.

[31] W. McCune. Otter 3.0 Reference Manual and Guide. Technical Report ANL-94-6, Argonne National Laboratory, Argonne, Illinois 60439, USA, 1994.

[32] W. McCune. Solution of the Robbins Problem. Journal of Automated Reasoning, 19(3):263–276, 1997.

[33] A. Meier. Tramp: Transformation of Machine-Found Proofs into Natural Deduction Proofs at the Assertion Level. In D. McAllester, editor, Proceedings of the 17th International Conference on Automated Deduction (CADE–17), volume 1831 of LNAI, pages 460–464, Pittsburgh, PA, USA, June17–20 2000. Springer VerlagGermany.

[34] A. Meier. Multi – Proof Planning with Multiple Strategies. PhD thesis, Fachbereich Informatik, Universität des Saarlandes, Saarbrücken, 2004.

[35] A. Meier and E. Melis. Proof planning limit problems with multiple strategies. Seki Report SR-2004-04, Fachbereich Informatik, Universität des Saarlandes, Saarbrücken, Germany, 2004.

[36] A. Meier, M. Pollet, and V. Sorge. Classifying Isomorphic Residue Classes. In R. Moreno-Díaz, B. Buchberger, and J.L. Freire, editors, Proceedings of the 8th International Workshop on Computer Aided Systems Theory (EuroCAST 2001), volume 2178 of LNCS, pages 494–508, Las Palmas de Gran Canaria, Spain, February19–23 2001. Springer Verlag, Germany.

[37] A. Meier, M. Pollet, and V. Sorge. Classifying Residue Classes – Results of a Case Study. Seki Report SR-01-01, Fachbereich Informatik, Universität des Saarlandes, Saarbrücken, Germany, 2001.

[38] A. Meier, M. Pollet, and V. Sorge. Comparing Approaches to Explore the Domain of Residue Classes. Journal of Symbolic Computation, Special Issue on the Integration of Automated Reasoning and Computer Algebra Systems, 34(4):287–306, 2002. S. Linton and R. Sebastiani, eds.

[39] A. Meier and V. Sorge. Exploring Properties of Residue Classes. In M. Kerber and M. Kohlhase, editors, Symbolic Computation and Automated Reasoning – The CALCULEMUS-2000 Symposium, pages 175–190, St. Andrews, UK, August6–7, 2000 2001. AK Peters, Natick, MA, USA.

[40] Andreas Meier, Erica Melis, and Martin Pollet. Adaptable mixed-initiative proof planning for educational interaction. Electronic Notes in Theoretical Computer Science, 2004. To appear.

[41] E. Melis. AI-Techniques in Proof Planning. In H. Prade, editor, Proceedings of of the 13th European Conference on Artifical Intelligence, pages 494–498, Brighton, UK, August23–28 1998. John Wiley & Sons, Chichester, UK.

[42] E. Melis. The “Limit” Domain. In R. Simmons, M. Veloso, and S. Smith, editors, Proceedings of the Fourth International Conference on Artificial Intelligence Planning Systems (AIPS-98), pages 199–206, Pittsburgh, PEN, USA, June7–10 1998. AAAI Press, Menlo Park, CA, USA.

[43] E. Melis, J. Buedenbender, E. Andres, A. Frischauf, G. Goguadse, P. Libbrecht, M. Pollet, and C. Ullrich. ActiveMath: A generic and adaptive web-based learning environment. Artificial Intelligence and Education, 12(4):385–407, 2001.

[44] E. Melis and A. Meier. Proof Planning with Multiple Strategies. In J. Loyd, V. Dahl, U. Furbach, M. Kerber, K. Lau, C. Palamidessi, L.M. Pereira, and Y. Sagivand P. Stuckey, editors, First International Conference on Computational Logic (CL-2000), volume 1861 of LNAI, pages 644–659, London, UK, 2000. Springer-Verlag.

[45] E. Melis and J. Siekmann. Knowledge-Based Proof Planning. Artificial Intelligence, 115(1):65–105, 1999.

[46] E. Melis and C. Ullrich. Flexibly Interleaving Processes. In K.-D. Althoff and R. Bergmann, editors, International Conference on Case-Based Reasoning, volume 1650 of LNAI, pages 263–275. Springer VerlagGermany, 1999.

[47] E. Melis, J. Zimmer, and T. Müller. Integrating Constraint Solving into Proof Planning. In Kirchner and Ringeissen [29], pages 32–46.

[48] R. Milner. The use of machines to assist in rigorous proof. In C.A.R. Hoare and J.C. Shepherdson, editors, Mathematical Logic and Programming Languages, pages 77–88. Prentice-Hall, 1984.

[49] S. Minton. Explanation-Based Learning: A Problem Solving Perspective. Artificial Intelligence, 40:63–118, 1989.

[50] A. Newell and H.A. Simon. GPS: a Program that Simulates Human Thought. In E.A. Feigenbaum and J. Feldmann, editors, Computers and Thought. McGraw-Hill, 1963.

[51] L. Paulson. Isabelle: A Generic Theorem Prover. Number 828 in LNCS. Springer VerlagGermany, 1994.

[52] D. Redfern. The Maple Handbook: Maple V Release 5. Springer VerlagGermany, 1999.

[53] E. Rich and K. Knight, editors. Artificial Intelligence. McGraw-Hill, 1991.

[54] S. Russell and P. Norvig. Artificial Intelligence - A Modern Approach. Prentice Hall, Englewood Cliffs, 1995.

[55] S. Scholl. Hierarchische Analogie im Beweisplanen. Master’s thesis, Fachbereich Informatik, Universität des Saarlandes, Saarbücken, 2003.

[56] J. Siekmann, C. Benzmüller, V. Brezhnev, L. Cheikhrouhou, A. Fiedler, A. Franke, H. Horacek, M. Kohlhase, A. Meier, E. Melis, M. Moschner, I. Normann, M. Pollet, V. Sorge, C. Ullrich, C.P. Wirth, and J. Zimmer. Proof Development with OMEGA. In A. Voronkov, editor, Proceedings of the 18th International Conference on Automated Deduction (CADE–18), number 2392 in LNAI, pages 144–149, Kopenhagen, Denmark, 2002. Springer VerlagGermany.

[57] J. Siekmann, C. Benzmüller, A. Fiedler, A. Meier, I. Normann, and M. Pollet. Proof Development in OMEGA: The Irrationality of Square Root of 2. In Fairouz Kamareddine, editor, Thirty Five Years of Automating Mathematics, Kluwer Applied Logic series. Kluwer Academic Publishers, 2003. In Print.

[58] V. Sorge. Non-Trivial Symbolic Computations in Proof Planning. In Kirchner and Ringeissen [29], pages 121–135.

[59] R.M. Stallmann and G.J. Sussmann. Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis. Artificial Intelligence, 9(2), 1977.

[60] A. Tate. Generating Project Networks. In R. Reddy, editor, Proceedings of the 5th International Joint Conference on Artificial Intelligence (ICJAI), pages 888–893, Cambridge, MA, USA, August22–25 1977. Morgan Kaufmann, San Mateo, CA, USA.

[61] C. Ullrich. Analogie im Beweisplanen. Master’s thesis, Fachbereich Informatik, Universität des Saarlandes, Saarbücken, 2000.

[62] M.M. Veloso, J. Carbonell, M.A. Perez, D. Borrajo, E. Fink, and J. Blythe. Integrating Planning and Learning: The Prodigy Architecture. Journal of Experimental and Theoretical Artificial Intelligence, 7(1):81–120, 1995.

[63] C. Weidenbach, B. Afshordel, U. Brahm, C. Cohrs, Th. Engel, E. Keen, C. Theobalt, and D. Topic. System Description: Spass Version 1.0.0. In Ganzinger [22], pages 378–382.

[64] D.S. Weld. An Introduction to Least Commitment Planning. AI Magazine, 15(4):27– 61, 1994.

[65] J. Zimmer. Constraintlösen für Beweisplanung. Master’s thesis, Fachbereich Informatik, Universität des Saarlandes, Saarbrücken, 2000.