An Approach to Assertion Application via Generalised Resolution

Quoc Bao Vo^{1}, Christoph Benzmüller^{1} and Serge

Autexier^{1,2}

1FR Informatik, Universität des Saarlandes, 66041

Saarbrücken, Germany

        {bao,chris}@ags.uni-sb.de

2DFKI GmbH, 66123 Saarbrücken, Germany

            autexier@dfki.de

SEKI Report SR–2003–01

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

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

An Approach to Assertion Application via Generalised Resolution

Quoc Bao Vo^{1}, Christoph Benzmüller^{1} and Serge Autexier^{1,2} 1FR Informatik, Universität des Saarlandes, 66041 Saarbrücken, Germany

               {bao,chris}@ags.uni-sb.de

2DFKI GmbH, 66123 Saarbrücken, Germany

                   autexier@dfki.de

July 22, 2003

Abstract

In this paper we address assertion retrieval and application in theorem proving systems or proof planning systems for classical first-order logic. Due to Huang the notion of assertion comprises mathematical knowledge such as definitions, theorems, and axioms. We propose a distributed mediator module between a mathematical knowledge base KB and a theorem proving system T P which is independent of the particular proof representation format of T P and which applies generalised resolution in order to analyze the logical consequences of arbitrary assertions for a proof context at hand.

Our approach is applicable also to the assumptions which are dynamically created during a proof search process. It therefore realises a crucial first step towards full automation of assertion level reasoning. We discuss the benefits and connection of our approach to proof planning and motivate an application in a project aiming at a tutorial dialogue system for mathematics.

1 Introduction

Mathematical assistant systems provide users with tools that support them in constructing proofs. Thereby it is an important issue that the constructed proof fragments are presented in a format that is easy to understand for human users. This is the central problem of proof presentation and explanation. On the other hand, sophisticated proofs for real mathematical problems have now been constructed in mathematical assistant systems (either automatically or interactively) at different levels of granularity^{1}. In some of the employed approaches, most low level logical operations are abstracted away and mainly domain specific mathematical knowledge is used to guide the construction of the proofs.

1There is a ongoing debate whether level of abstraction, level of detail, or level of granularity is the most appropriate notion to use. In this paper we will use the term level of granularity, since we address abstraction on logical derivations and proof operators and not, for instance, abstraction of the object representation language.

The area is known as proof planning and such domain specific mathematical knowledge comes in as the strategies or proof methods which are made available to the proof planner (cf. [9] and [17, 21, 20] and the references therein).

The assertion level introduced by Huang [16] is argued to be just the right level to which machine generated proofs should be transformed before being presented to (human) users. In this paper we argue further that the assertion level can also serve as one of those levels of granularity on which knowledge-based proof planning should be based. This viewpoint is also taken by Autexier [3], which provides a proof representation framework subsuming the assertion level. However, proof automation of the framework, i.e. the heuristically guided choice of the assertions to apply, is still a challenge and not tackled in this paper.

Huang [16] achieves proofs at the assertion level by reconstructing machine generated proofs. This process basically involves clustering several proof steps of the input proof into segments. >From the outside, each segment can be viewed as one (assertion level) proof step. While this partly solves the problem of proof presentation as each assertion level proof step can be mapped naturally to single statements of the natural language presentation of the proof, it has not been investigated yet how the proof planning process may directly benefit from such a representation level. We are convinced that by planning directly on the assertion level it will be possible to overcome at least some of the identified limitations and problems of proof planning (see [5, 10])— in particular, those, that are caused by an unfortunate intertwining of proof planning and calculus level theorem proving. The perspective we therefore motivate in this paper is to consider the assertion level as a well chosen borderline between proof planning and machine oriented methods. Determining the logical consequences of assertions in a proof context is the task of machine oriented methods (in our case generalised resolution). The tasks on top of this level — for instance, a domain-dependent collection of the initial assertions to be considered, the heuristic selection of the most promising among the computed logical consequences, the introduction, constraining and handling of meta-variables, etc. — belong to the scope of domain specific proof planning.

In summary, instead of reconstructing natural deduction (ND) proofs to obtain assertion level proofs as suggested by Huang, we propose to directly plan for proofs at the assertion level. This should improve the quality of the resulting proof plans and also facilitate better user interaction. In contrast to tactical theorem proving, we do not want each assertion associated with a particular tactic but aim at one general module which works for arbitrary assertions and computes their consequences in arbitrary proof contexts. These consequences are then suggested to the user and/or the automated prover. Note that this is different from proposing intermediate subgoals and then verifying them with the help of tactics as done by systems like Mizar (http://www.mizar.org/).

The development of our ideas revolves around the mathematical assistant system Omega [27] and the current initiative in this project to rebuild the system on top of the proof representation framework in [3]. We furthermore employ Omega’s agent-based search mechanism Oants [7] for a distributed modeling of our framework and we motivate an application of the approach in a project aiming at a tutorial dialogue system for mathematics.

2 Proof planning at the assertion level

A brief review on the assertion level.

This part is reproduced from [16] for completeness. Consider the problem of presenting machine generated proofs. Assume that the target formalism is natural deduction which is a common practice for many existing proof transformation systems. In contrast to proofs found in mathematical textbooks, proofs constructed by these systems are composed of derivations from elementary logic, where the focus of attention is on syntactic manipulations rather than on the underlying semantical ideas. The problem seems to come from the lack of intermediate structures in ND proofs that allow atomic justifications at a higher level of abstraction. Huang then went on to introduce the following three levels of justifications:

• Logic level justifications are simply verbalizations of the ND inference rules, such as the rule of Modus Ponens.

• Assertion level justifications account for derivations in terms of the application of an axiom, a definition or a theorem (collectively called an assertion). For instance, an extract from a textbook proof may read:

“since e is a member of the set A, and A is a subset of B, according to the definition of subset, e is a member of B”.

• Proof level justifications are at a yet higher level. For instance, a proof can be suppressed by resorting to its similarity to a previous proof.

Assertion level and proof planning.

Scrutinizing the above example for the assertion level justifications, it seems just the right level for proof plans to be carried out. Rather than having to work around with ND inference rules, the proof planner simply goes straight to the intended conclusion, viz. e is a member of B, from the given premises, viz. e is a member of A and A ⊆ B, and the assertion, viz. the definition of subset. This would in the first place save the proof planner from exploding its own search space. Furthermore, it should fit better to the structural mechanisms of other high level proof methods such as analogy, induction, diagonalization, etc. and in particular island proof planning, cf. [19]. It should also fit well to the framework of incremental proof planning proposed by Gerberding and Pientka [15] in which assertion application can be considered as a special form of meta-rules.

Now let’s consider an assertion A. As pointed out by Huang, there may be several ways in which this assertion can be used depending on the proof situation to which this assertion is introduced. For instance, let A be the assertion from our running example:

∀S_{1}, S_{2} : Set.(S_{1} ⊆ S_{2} ⇔ ∀x : Element.(x ∈ S_{1} ⇒ x ∈ S_{2}))

This assertion allows us to derive: (1) a ∈ V from a ∈ U and U ⊆ V, (2) U ⊈ V from a ∈ U and a ∉ V, (3) ∀x : Element.(x ∈ U ⇒ x ∈ V) from U ⊆ V, (4) etc.

A theorem prover/proof planner that operates on the calculus level can only achieve such conclusions after a number of proof steps to eliminate the quantifiers and other connectives such as implication and conjunction. On the other hand, most human mathematicians would be satisfied having those conclusions derived in one step from the assertion.

Huang [16] overcomes this problem by introducing different inference rules to allow all possible applications of such an assertion. These inference rules are called assertion level inference rules or macro-rules by their nature of being “pseudo inference rules” which actually stand for sequences of more elementary inference rules, called compound proof segments. While the more elementary rules (of ND) are chunked into macro-rules (at the assertion level), this in turn potentially introduces an exploded set of inference rules. Therefore, it may not work too well for a proof search mechanism that is required to be efficient. For instance, for the above assertion from our running example, at least seven (7) different macro-rules can be generated (cf. [16].)

Formalization of the problem.

We take as the starting point for our approach the proof development environment Omega [27] whose core consists of a proof planner together with a hierarchical plan data structure (PDS). The proof format in Omega is based on the natural deduction calculus. A linearised version of ND proofs as introduced by Andrews [1] is employed. In this formalism [17], an ND proof is a sequence of proof lines , each of them is of the form:

Label  Δ ⊢ derived-formula  (Rule premise-lines)

where Rule is a rule of inference in ND or a method, which justifies the derived-formula using the knowledge from in the premise-lines. Rule and premise-lines together are called the justification of a line. Δ is a finite set of formulae which are the hypotheses the derived formula depends on.

A problem of proof planning consists of a theorem and the assumptions to be used to prove the theorem. A proof planner operates on a set of methods to be used to construct a proof plan. The theorem and assumptions are expressed as deduction lines in a PDS where all the assumptions are marked as closed and the theorem is marked as open. The proof planner then uses the methods to come up with actions to update the PDS. The aim of the proof planning process is to reach a closed PDS, that is one without open lines.

As application of lemmata lies at heart of most (non-trivial) mathematical proofs, it is important that this issue be addressed in a realization of any proof planner.

In Omega, a proof planning process starts with a task, a data structure designed to encapsulate a complete (sub-)problem. Formally, a task is a pair ⟨SP_{L_{open}}, L_{open}⟩ consisting of an open line of the PDS, L_{open}, and a set of lines from the PDS, SP_{L_{open}}. L_{open} is called the task line whose formula is called task formula. Members of SP_{L_{open}} are called the support lines or supports for the task line L_{open}.

Now consider the situation in which the prover is confronting a list of tasks, called an agenda in the Omega system, that it needs to solve in order to prove the intended theorem. Among the available strategies/methods, the prover could possibly ponder whether there is a definition/axiom or some previously proved result which it can use in the current proof situation to (i) either obtain further closed lines serving as intermediate steps for solving one of the tasks; (ii) or reduce a goal task (on some open line) to some subtasks which can be resolved by further proof steps.

\begin{matrix}α & α_{1} & α_{2} \\ (φ ∨ ψ)^{⊕} & φ^{⊕} & ψ^{⊕} \\ (φ ⇒ ψ)^{⊕} & φ^{⊖} & ψ^{⊕} \\ (φ ∧ ψ)^{⊖} & φ^{⊖} & ψ^{⊖} \\ (¬φ)^{⊕} & φ^{⊖} & − \\ (¬φ)^{⊖} & φ^{⊕} & − \end{matrix}  \begin{matrix}β & β_{1} & β_{2} \\ (φ ∧ ψ)^{⊕} & φ^{⊕} & ψ^{⊕} \\ (φ ∨ ψ)^{⊖} & φ^{⊖} & ψ^{⊖} \\ (φ ⇒ ψ)^{⊖} & φ^{⊕} & ψ^{⊖} \end{matrix}  \begin{matrix}(γ, x) & γ_{0}(x) \\ (∀_{x}φ)^{⊖} & φ^{⊖} \\ (∃_{x}φ)^{⊕} & φ^{⊕} \end{matrix} ; \begin{matrix}(δ, x) & δ_{0}(sko)^{(∗)} \\ (∀_{x}φ)^{⊕} & φ[sko/x]^{⊕} \\ (∃_{x}φ)^{⊖} & φ[sko/x]^{⊖} \end{matrix}

(∗)sko is a Skolem term.

Figure 1: Analyzing signed formulae

It now boils down to the question of how tasks and assertions are to be handled without having to generate all the possible macro-rules as suggested by Huang. And we, of course don’t want to sacrifice any possible outcome from applications of assertions.

We follow a representation framework employed by Wallen [29] and Autexier [3] using the concept of polarities and uniform notation (cf. [12, 13, 29]) to represent the formulae the proof planner has to deal with.

Signed formulae:

Each formula is assigned a polarity which is either positive (⊕) or negative (⊖). A set of formulae Γ is assigned a polarity p iff each member of Γ is assigned p. The polarity (⊖, ⊕) of a signed formula is just another representation of of the succedent/antecedent made by Gentzen [14] wrt. the sequent calculus. In the sequent calculus, all formulae which occur in the antecedent would be annotated with negative (⊖) polarity while formulae occurring in the succedent are of positive (⊕) polarity. In the linearised version of the Natural Deduction calculus employed by Omega, if a deduction line Δ ⊢ φ is marked closed (in a PDS) then Δ is assigned ⊕ and φ ⊖. If Δ ⊢ φ is marked open then Δ is assigned ⊖ and φ ⊕. Intuitively, a signed formula φ^{⊕} is something the prover wishes to prove while φ^{⊖} is something given.

We introduce further notations for technical considerations:

(i) form(φ^{p}) {def \atop =} φ and polarity(φ^{p}) {def \atop =} p; and

(ii) the operator − : {⊖, ⊕} → {⊖, ⊕} such that −⊖ = ⊕ and −⊕ = ⊖.

Signed formula trees: Using the rules from Fig. 1, a signed formula can be represented in the form of a tree whose sub-trees represent its signed sub-formula, these trees are called signed formula trees, or SFTs. In such a tree, each node has a natural interpretation as a signed formula, and we shall speak of nodes and signed formulae as if they were one and the same (e.g., a “node” (φ ∨ ψ)^{⊕} is one labelled with (φ ∨ ψ)^{⊕} and having arcs to nodes φ^{⊕} and ψ^{⊕}.)

Example:^{2}

The following is the signed formula tree of the formula A given as ∀_{S_{1},S_{2}}(S_{1} ⊆ S_{2} ⇔ ∀_{x}(x ∈ S_{1} ⇒ x ∈ S_{2})). Thereby we assume that assumptions are initially assigned with the polarity ⊖. (In our tree F abbreviates the formula ∀_{x}(x ∈ S_{1} ⇒ x ∈ S_{2})).

2We choose to suppress all references to sorts for the sake of readability.

(∀_{S_{1},S_{2}}(S_{1} ⊆ S_{2} ⇔ ∀_{x}(x ∈ S_{1} ⇒ x ∈ S_{2})))_{(γ,S_{1},S_{2})}^{⊖} ; \begin{matrix}(S_{1} ⊆ S_{2} ⇔ F)_{α}^{⊖} \\ \begin{matrix}(S_{1} ⊆ S_{⇒}F)_{β}^{⊖} \\ (S_{1} ⊆ S_{2})^{⊕} & (F)_{(γ,x)}^{⊖} ; \begin{matrix}(x ∈ S_{1} ⇒ x ∈ S_{2})_{β}^{⊖} \\ (x ∈ S_{1})^{⊕} & (x ∈ S_{2})^{⊖} \end{matrix} \end{matrix} & (F ⇒ S_{1} ⊆ S_{2})_{β}^{⊖} ; (F)_{(δ,x)}^{⊕} ; \begin{matrix}(sko(S_{1}, S_{2}) ∈ S_{1} ⇒ sko(S_{1}, S_{2}) ∈ S_{2})_{α}^{⊕} \\ (sko(S_{1}, S_{2}) ∈ S_{1})^{⊖} & (sko(S_{1}, S_{2}) ∈ S_{2})^{⊕} \end{matrix} ; (S_{1} ⊆ S_{2})^{⊖} \end{matrix}

Now we can go back to our problem. Assume that a task ⟨SP_{L_{open}}, L_{open}⟩ together with an assertion A are currently under consideration. As the goal is to come up with a desirable conclusion derivable from the assertion A (relative to ⟨SP_{L_{open}}, L_{open}⟩), the following computational process revolves around the signed formula tree of A, called T_{A}. Using unification-based algorithms we unify the signed atoms at the leaves of the signed formula trees from the task ⟨SP_{L_{open}}, L_{open}⟩ with the (signed) atoms at the leaf nodes of T_{A}.

Secondly, we will need the following notation to talk about the interrelations between formulae: Given a signed formula φ^{p},

• if an α-rule is applicable to φ^{p} then its children are said to be directly α-related, e.g. the two sub-formulae φ^{⊕} and ψ^{⊕} of (φ ∨ ψ)^{⊕} are α-related;

• if a β-rule is applicable to φ^{p} then its children are said to be directly β-related, e.g. the two sub-formulae φ^{⊕} and ψ^{⊕} of (φ ∧ ψ)^{⊕} are β-related;

A signed formula φ is α (resp. β) -related to ψ if and only if either φ or one of its ancestors is directly α (resp. β) -related to ψ.^{3}

s-unifiable and complementary:

Two nodes φ^{p} and ψ^{q} are s-unifiable iff p ≠ q and φ and ψ are unifiable. φ^{p} and φ^{q} are complementary iff p ≠ q.

Notation: We will liberally use the notions applicable to logical formulae and apply them to signed formulae by absorbing them through the polarities of signed formulae. E.g., given a signed formula τ and a substitution θ, we write τθ to denote the signed formula (form(τ)θ)^{polarity(τ)}.

We also observe that it is possible to reconstruct formulae from an SFT in such a way that the semantics is preserved. And because all information is conveyed from a node to its children, it is possible to reconstruct a formula from the leaf nodes of its SFT together with the α and β -relations between the subtrees without having to trace back through all of the internal nodes.

3Note that the notions of α and β-related formulae are more general than the notions of conjunction and disjunction as the α (resp. β)-relations can refer to both conjunctions and disjunctions depending on whether they occur in the antecedent or the succedent of a sequent.

Now we come up with the algorithm for manipulating SFTs in order to obtain desirable conclusions from an assertion (in relation to other given assumptions or open goal tasks). The idea generalises Robinson’s resolution principle [25] and in particular reminds to path resolution [23] and the connection graph principle [18, 2, 8]. In much the same way that an arbitrary formula can be reduced to the normal form which contains a set of clauses, i.e. disjunctions of literals, we observe that a given signed formula tree can be reduced to a set of SFTs whose members don’t have any α-related pair of sub-formulae.

As with resolution, the idea is to replace a literal in a clause (correspondingly, a leaf node of an SFT) by the information entailed by it that comes from another clause (correspondingly, another SFT). However, unlike resolution theorem proving formalism where the focus is on a refutation procedure in order to establish the unsatisfiability of a set of formulae, our focus of attention is on the derivation of new formulae (be it new assumptions or new subgoals) from the existing ones. Therefore, we won’t transform every signed formula (or equivalently, SFT) to the normal form which contains only β-related subtrees as in resolution theorem proving, but rather we delay that until as late as possible. The idea is: instead of normalizing all formulae to the normal form, we just need to take out from the formulae to be resolved the relevant parts when resolution is carried out. For instance, consider a set of formulae S = {(A ∧ B) ∨ (C ∧ D), ¬A ∨ E}, we can just take out the relevant formula A ∨ (C ∧ D) from (A ∧ B) ∨ (C ∧ D) and resolve it using ¬A ∨ E. This result in the following new set of formulae: S′ = {(A ∧ B) ∨ (C ∧ D), ¬A ∨ E, (C ∧ D) ∨ E}.

Now we can go back to the more sophisticated representation of SFTs. >From the above example with resolution, it is important to know how the so-called relevant parts can be computed. While it is not so clear how this can be done with logical formulae, it is interesting that SFTs contain structures supporting such operations: Instead of resolving complementary pairs of literals from clauses, we resolve s-unifiable pairs of leaf nodes (or, atomic signed formulae) from SFTs. We therefore term our inference principle generalised resolution, or GR.

We observe that in addition to the leaf nodes of SFTs on which we perform GR, the structure of SFTs, i.e. the internal nodes and links between nodes, also plays an important part in GR inferences.^{4}

The algorithm:

The following algorithm takes as input two SFTs τ_{1} and τ_{2} with τ_{1} being updated by the information from τ_{2} by performing resolution on the two leaf nodes η_{1} and η_{2} from τ_{1} and τ_{2}, resp., under the substitution θ.

GR(τ_{1}: SFT, η_{1}: leaf_node; τ_{2}: SFT, η_{2}: leaf_node; θ: substitution) begin If η_{1}θ and η_{2}θ are complementary then

4Given a pair of s-unifiable leaf nodes φ^{p} and ψ^{−p} on two SFTs τ_{1} and τ_{2}, respectively: the results of resolving φ^{p} on τ_{1} by ψ^{−p} from τ_{2} and resolving ψ^{−p} on τ_{2} by φ^{p} from τ_{1}, in general lead to two syntactically different, albeit logically equivalent, SFTs.

1. Instantiate all variables in τ_{1} and τ_{2} with the substitution θ;

2. For i = 1, 2, prune all α-related subtrees wrt. η_{i} on τ_{i};

3. Replace the leaf node η_{2} in τ_{2} by (⊥)^{⊖} (resp. (⊤)^{⊕}) if polarity(η_{2}) = ⊖ (resp. ⊕);

4. Replace the formula at each ancestor of η_{2} in τ_{2} with a question mark (?) while retaining the polarity and the rule originally applied there;

5. Reconstruct the formulae at the internal nodes of τ_{2} currently marked (?) using the formula(e) from their child(ren) and the polarity/rule at those nodes;

6. Replace the formula at each ancestor of η_{1} in τ_{1} with a question mark (?) while retaining the polarity and the rule originally applied there;

7. If polarity(τ_{2}) = polarity(η_{1}) then: Replace the leaf node η_{1} on τ_{1} by τ_{2} else: Replace the leaf node η_{1} on τ_{1} by ¬form(τ_{2})^{polarity(η_{1})};

8. Reconstruct the formulae at the internal nodes of τ_{1} currently marked (?) using the formula(e) from their child(ren) and the polarity/rule at those nodes;

9. Return the new τ_{1}; else

{ Do nothing } end;

All the above operations should be clear except the reconstruction of the SFTs. Consider an internal node τ = (φ)_{r}^{p} of an SFT. After a subtree of τ is modified during the execution of GR(), the formula at τ, viz. φ, is replaced by a question mark (?). Once all children of τ have been reconstructed, we can proceed to reconstruct the formula at τ:

1. Special treatment is due when at least one of τ’s children is (⊥)^{⊖} or (⊤)^{⊕}:

(a) Case r = β: let υ be the other child of τ. If polarity(τ) =polarity(υ) then τ and υ are collapsed into one node; otherwise, (?) is replaced by ¬form(υ).

(b) otherwise: the question mark (?) is replaced by (⊥)^{⊖} or (⊤)^{⊕} depending on polarity(τ).

2. Case r = α:

• Case α_{2} = nil: the question mark (?) is replaced by ¬form(α_{1}).

• Case α_{2} ≠ nil: the question mark (?) is replaced by form(α_{1}) ∧ form(α_{2}) if p = ⊖,

and by form(α_{1}) ∨ form(α_{2}), otherwise.

3. Case r = β: similar to the second case above and according to the table for β-rule.

4. Case r = (γ, x): Attention must be taken to avoid clash of variables. If x is a bound variable in form(γ_{0}(x)) then it must be renamed to a variable name that does not clash with any other variable in form(γ_{0}(x)). Then, (?) is replaced by ∀_{x}form(γ_{0}(x)) if p = ⊖, and by ∃_{x}form(γ_{0}(x)), otherwise.

5. Case r = (δ, x): the question mark (?) is replaced by form(δ_{0}(τ, sko)).

Correctness of algorithm GR together with other related results are established in the Appendix.

Now we are in the position to apply GR on the assertion A and all the relevant formulae coming from an agenda D. We are fortunate not having to perform proof search, we only have to find out derivable information (which can be new assumptions, i.e. closed lines, or new subgoals, i.e. open lines) from A using the information provided in D. That is, we have to resolve the leaf nodes of T_{A} by the s-unifiable leaf nodes on other SFTs. To simplify the presentation, we assume that our algorithm takes as input the SFT of A, viz. T_{A}, and a set of SFTs representing the current reasoning context RC so that we don’t have to worry about other details such as closed/open lines, assumptions, goals, etc. The algorithm also employs the on-the-fly skolemization whenever generalised resolution is performed.

Assertion Application(T_{A}: SFT; RC: set_of_SFTs) begin

1. All_results ← ∅;

2. P rocessed ← ∅;

3. For each leaf node s of T_{A} do:

While there is a leaf node t of an SFT τ ∈ RC ∪ {T_{A}} such that s and t are s-unifiable and (s, t, θ) ∉ P rocessed do:

(a) C_{T_{A}} ← T_{A}; { Create a working copy of T_{A} }

(b) p ← polarity(root(τ));

(c) Repeat: i. current_resolved ← s; ii. current_resolver ← t; iii. θ ← mgu(form(s), form(t)); iv. P rocessed ← P rocessed ∪ {(s, t, σ)}; v. Repeat:

A. τ ← GR(C_{T_{A}}, current_resolved, τ, current_resolver, θ); B. If there is a s-unifiable pair of leaf nodes s′ and t′ from C_{T_{A}} and τ, respec-

tively, then

– current_resolved ← s′;

– current_resolver ← t′;

– σ ← mgu(form(s′), form(t′));

– θ ← θσ;

– P rocessed ← P rocessed ∪ {(s′, t′, σ)}; else

– current_resolved ← nil;

– current_resolver ← nil; until current_resolved = nil;

vi. If p = ⊕ and polarity(root(τ)) = ⊖ then

C_{T_{A}} ← Negate(τ); else

C_{T_{A}} ← τ; until there is not any further s-unifiable pair of leaf nodes from C_{T_{A}} and any SFT in RC ∪ {T_{A}};

(d) All_results ← All_results ∪ {form(root(C_{T_{A}}))};

4. Return All_results;

end;

In the above algorithm, the function Negate(τ) adds a parent to the root node of the SFT τ. The formula and the polarity at the root node of the new tree are the negations of the formula and the polarity at the root node of τ. We have to carry out that operation because we do not want the outcome of applying an assertion to an open line, i.e. a goal, to be a closed line. For instance, applying the assertion A ⇒ B to a goal B^{⊕} should result in a new subgoal A^{⊕} rather than a conclusion (¬A)^{⊖}.

Example (Forward Reasoning):

Let the following deduction lines be marked closed in the input task:

(1) ⊢ A ⊆ B; and

(2) ⊢ e ∈ A.

By applying the first tree A ⊆ B^{⊖} to C_{T_{A}} which is the same as T_{A} for the moment, we obtain the following updated SFT for C_{T_{A}} (under the substitution θ = {S_{1} ↦ A, S_{2} ↦ B}).

(∀_{x}(x ∈ A ⇒ x ∈ B))_{γ}^{⊖} ; \begin{matrix}(x ∈ A ⇒ x ∈ B)_{β}^{⊖} \\ (x ∈ A)^{⊕} & (x ∈ B)^{⊖} \end{matrix}

Figure 2: The SFT for (∀_{x}(x ∈ A ⇒ x ∈ B))^{⊖}

By applying the second tree e ∈ A^{⊖} to the resulting C_{T_{A}}, we obtain as updated SFT for C_{T_{A}} (under the substitution θ_{1} = {x ↦ e}) the tree e ∈ B^{⊖} which is translated back to the Omega-proof format as a (closed) deduction line (3) ⊢ e ∈ B. This is also is also the desirable logical consequence of assertion A for lines (1) and (2).

Example (Resolve internal nodes):

To see the necessity of the inner iteration, we re-run our example with another task consisting of the following closed deduction line: (4) ⊢ ∀_{x}(x ∈ A ⇒ x ∈ B). This assumption results in the SFT depicted in Figure 2. Applying this tree to T_{A} and assuming that we unify first the two nodes (sko(S_{1}, S_{2}) ∈ S_{1})^{⊖} (on T_{A}) and (x ∈ A)^{⊕} on the above SFT we obtain the updated C_{T_{A}} below (under the substitution θ = {x ↦ sko(S_{1}, S_{2}), S_{1} ↦ A}).

\begin{matrix}(¬sko(S_{1}, S_{2}) ∈ B ⇒ A ⊆ S_{2})_{β}^{⊖} \\ \begin{matrix}(¬sko(S_{1}, S_{2}) ∈ B)_{α}^{⊕} \\ (sko(S_{1}, S_{2}) ∈ B)^{⊖} \end{matrix} & (A ⊆ S_{2})^{⊖} \end{matrix}

Notice how the α-related branches on the SFT and the nodes labelled with the α and γ and δ-rules are pruned away by GR().

Now we try to unify a leaf node on this tree to some leaf node on T_{A} again which is achievable through the unification on the two nodes (sko(S_{1}, S_{2}) ∈ B)^{⊖} on the above SFT and (sko(S_{1}, S_{2}) ∈ S_{2})^{⊕} (on T_{A}).

The updated C_{T_{A}} now becomes the tree displayed to the right (under the substitution θ_{1} = {S_{2} ↦ B})^{5}.

\begin{matrix}(¬A ⊆ B ⇒ A ⊆ B)_{β}^{⊖} \\ \begin{matrix}(¬A ⊆ B)_{α}^{⊕} \\ (A ⊆ B)^{⊖} \end{matrix} & (A ⊆ B)^{⊖} \end{matrix}

This tree translates into the desirable logical consequence of assertion A for line (4) and the closed line (5) ⊢ A ⊆ B is obtained.

Example (Sidewards Reasoning):

We now consider an example in which a goal line (i.e. an open line from the input task) and a closed line is applied. Assume that our current task consists of an open line (6) ⊢ ϵ ∈ B and a closed line (7) ⊢ A ⊆ B, which correspond to the two singleton trees (ϵ ∈ B)^{⊕} and (A ⊆ B)^{⊖} respectively.

Applying the former to T_{A} by unifying it to the leaf node (x ∈ S_{2})^{⊖}, we obtain the following SFT:

(∀_{S_{1}}(S_{1} ⊆ B ⇒ ¬ϵ ∈ S_{1}))_{γ}^{⊖} ; \begin{matrix}(S_{1} ⊆ B ⇒ ¬ϵ ∈ S_{1})_{β}^{⊖} \\ (S_{1} ⊆ B)^{⊕} & \begin{matrix}(¬ϵ ∈ S_{1})_{α}^{⊖} \\ (ϵ ∈ S_{1})^{⊕} \end{matrix} \end{matrix}

5Note that the root node of the computed SFT is: (A ⊆ B)^{⊖} has a different polarity from that of the node it is going to replace, viz. (sko(S_{1}, S_{2}) ∈ S_{2})^{⊕}, on the SFT T_{A}. Therefore, we replace that node with (¬A ⊆ B)^{⊕} instead.

Then we can apply (A ⊆ B)^{⊖} to this SFT by unifying it to the node (S_{1} ⊆ B)^{⊕}, the resulting tree is:

\begin{matrix}(¬ϵ ∈ A)_{α}^{⊖} \\ (ϵ ∈ A)^{⊕} \end{matrix}

This corresponds to a new open line (8) ⊢ ϵ ∈ A, which is the desirable consequence of assertion A for lines (6) and (7).

3 Concurrent search for applicable assertions

In this section we propose a module called M which models assertion application as distributed search processes in the Oants approach [7]. This agent based formalism is the driving force behind a distributed proof search approach in Omega. It enables the distribution of proof search among groups of reasoning agents.

First we briefly sketch the general application scenario that motivates our approach. We assume a scenario where a theorem prover T P is connected to a mathematical knowledge base KB. T P is currently focusing a proof task T = ⟨SP_{L_{open}}, L_{open}⟩ and candidate assertions {B_{i}} are determined in KB and handed over to our assertion module M. The task of M is to compute wrt. proof task T all possible logical consequences of the available assertions B_{i}.

We propose to create for each assertion B_{i} one associated instance AG_{B_{i}} of a generic assertion agent AG. The generic assertion agent AG is based on the algorithm Assertion-Application provided in this paper. Note that this algorithm only depends on the SFT of the focused assertion and a further set of SFTs for the proof context, and both are specified as parameters of AssertionApplication. Each assertion agent instance AG_{B_{i}} computes and suggests the logical consequences of B_{i} in proof context T to our module M which passes them further to T P.

(∀_{S_{1}}(S_{1} ⊆ ℘(C) ⇒ ¬A ∈ S_{1}))_{γ}^{⊖} ; \begin{matrix}(S_{1} ⊆ ℘(C) ⇒ ¬A ∈ S_{1})_{β}^{⊖} \\ (S_{1} ⊆ ℘(C))^{⊕} & \begin{matrix}(¬A ∈ S_{1})_{α}^{⊖} \\ (A ∈ S_{1})^{⊕} \end{matrix} \end{matrix}

Depending on the size of the knowledge base KB there could be too many applicable assertions passed to M and also too many ways an assertion can be applied to be handled in practice (recall the remark above about the number of possible ND inference rules associated with the assertion of our running example). For instance, going back to our running example again, let our current task be ⟨{Δ ⊢ A ⊆ B; Δ ⊢ B ⊆ C; }, A ∈ ℘(C)⟩. The assertion A is applicable in this situation and the outcome of applying our algorithm to this open line is the SFT displayed at the top right corner of this paragraph.

As the root node is non-empty and the input trees include an open line, we have to reproduce the root node to have polarity ⊕, which is (¬∀_{S_{1}}(S_{1} ⊆ ℘(C) ⇒ ¬A ∈ S_{1}))^{⊕}. This corresponds to a new open line: Δ ⊢ ∃_{S_{1}}(S_{1} ⊆ ℘(C) ∧ A ∈ S_{1}) which is, even though logically correct, not a very useful subgoal to be pursued.^{6}

We sum up the above argument by claiming that restricted application of assertion is necessary. One possible and simple restriction is to impose prerequisite(s), such as simple syntactical criteria or domain restrictions, when selecting the candidate assertions that are passed from KB to M. These kind of specific constraints can be realized provided the constraints are encoded in the assertion specification. For instance, regarding our running example, a simple but useful heuristic to prove the membership of an object wrt. a set S using the subset definition is that the task includes a closed line stating that S is a superset of some other set. It is such a heuristically constrained version of assertion application that we are currently employing in the Omega system.

Proof planning, however, has developed more sophisticated ways to guide and constrain possible instantiations and applications of assertions. The investigation on how some of these techniques can optimally be employed on top of our assertion application module M in order to better constrain the search for potential assertion candidates is further work.

Example.

We present a proof constructed in the Omega system using assertion agents. The initial PDS formulating the problem is as follows:

1.  1;  ⊢  symmetric(A)  Hyp ✓
2.  2;  ⊢  symmetric(B)  Hyp ✓
THM  1,2;  ⊢  symmetric(A ∩ B)  (?)

In the above PDS, the lines marked with ✓ are the closed lines and the open line is marked with the question mark (?).

The following proof (produced interactively in Omega) for the above problem uses the definition of the symmetric relation, viz. (Sym-Def): ∀_{R}symmetric(R) ⇔ (∀_{x,y}⟨x, y⟩ ∈ R ⇒ ⟨y, x⟩ ∈ R), and the definition of intersection (on sets), viz. (∩-Def): ∀_{S_{1},S_{2}}∀_{x}x ∈ S_{1} ∩S_{2} ⇔ x ∈ S_{1} ∧ x ∈ S_{2}. The successive order of the constructed proof lines is: ⟨ 1.; 2.; THM; 3.; 4.; 8.; 5.; 6.; 7.; ⟩

1.  1;  ⊢ symmetric(A)  (Hyp) ✓
2.  2;  ⊢ symmetric(B)  (Hyp) ✓
3.  1,2;  ⊢ ∀_{x,y}⟨x, y⟩ ∈ A ⇒ ⟨y, x⟩ ∈ A  (aa(Sym-Def) 1) ✓
4.  1,2;  ⊢ ∀_{x,y}⟨x, y⟩ ∈ B ⇒ ⟨y, x⟩ ∈ B  (aa(Sym-Def) 2) ✓
5.  5;  ⊢ ⟨c_{1}, c_{2}⟩ ∈ A ∧ ⟨c_{1}, c_{2}⟩ ∈ B  (Hyp) ✓
6.  1,2,5; ⊢ ⟨c_{2}, c_{1}⟩ ∈ A  (aa([3])  5) ✓
7.  1,2,5; ⊢ ⟨c_{2}, c_{1}⟩ ∈ B  (aa([4])  5) ✓
8.  1,2;  ⊢ ∀_{x,y}⟨x, y⟩ ∈ A ∩ B ⇒ ⟨y, x⟩ ∈ A ∩ B  (aa(∩-Def)  5,6,7) ✓
THM 1,2;  ⊢ symmetric(A ∩ B)  (aa(Sym-Def) 8) ✓

6In fact, Huang’s [16] framework fails to produce the above inference step. This poses a serious question about the completeness of his approach due to Huang’s proposal of replacing the natural deduction inference rules altogether by the generated macro rules whenever an assertion is applicable.

[Hyp] indicates that the given proof line is a given hypothesis. The scopes of the hypotheses are rendered by the antecedents of the proof lines, i.e. those on the left of ⊢). Rules denoted by aa(assertion) indicate the application of assertion. In particular, on line (6), the assertion is [3] which indicates that the succedent of the sequent on line (3) has been added to the current mathematical database and now serves as a normal assertion. Similar remark can be made for line (7) (and the assertion introduced on line (4)).

While the above proof may be quite intuitive to a mathematician, the proof step on line (8) may be too hard to understand for a student who is trying to learn mathematics (see the Application described below). Observe that the assertion agent has carried out the application of Sym-Def together with ⊃-Introduction and ∀-introduction in that single proof step. However, the Omega system is capable of expanding complex proof steps to yield sub-proofs at lower levels of abstraction. This again emphasises the expressive power of our machinery.

An application: The Dialog project.

We are currently experimenting the assertion agent modules described above in the setting of an intelligent tutoring system for mathematics developed within the Dialog project [4]. The simple proof steps to be presented to the students are automatically generated by the proof assistant system Omega. The assertion agents assists the Omega system to produce these assertion-level proof steps. We want to stress that the student model may be updated during a tutoring session, hence the set of relevant assertions may dynamically change during an interactive session.

It is easy to motivate the design of our assertion application module for this scenario. Its capabilities for assertion application for a dynamically varying set of assertions are crucial for the project. It is also essential that reasoning is facilitated at a human oriented level of granularity, since we do not want the user to puzzle around with the peculiarities of, for instance, logical derivations in sequent or natural deduction calculus.

4 Related Work

Autexier [3], which himself employs ideas from [29, 26], suggests a proof representation and manipulation framework based on the uniform notation idea, while we here only employ it at the heart of an assertion mediator module which can be coupled with arbitrary proof systems.

The generalised resolution algorithm we propose also reminds to ideas employed in the connection graph method [18, 2, 8] and the clause graph method in [24]. However, since it is a crucial concern for us not to break down the structure of the assertions we operate with tree or graph structures generated for arbitrary formulas instead of just clause sets. Works in the literature of automated reasoning that are more closely related to our generalised resolution inference method include Non-clausal (NC)-Resolution introduced by Neil Murray [22] and Nested Resolution introduced by Traugott [28]. Both frameworks also employ the notion of polarity to recognise the unifiable occurrences of atomic formulas in the theory to be resolved. The resolved pair of literals are then simplified away from the formulae containing them. The resolvent is the disjunction of the two simplified formulae.

In their approaches, the structures of the formulae are clearly broken after a sequence of resolution steps.

Benzmüller et al. [6] motivate and also present a mediator between mathematical knowledge bases and theorem provers. A main difference of the approach here is that assertion agents are uniformly modeled; their individual behaviour is only determined by the particular assertion and the proof context they are instantiated with. Further related work is described in [11].

5 Conclusion and Future Work

We argued that the assertion level introduced by Huang [16] is one of the more interesting abstract levels where proof planning should be carried out. Therefore, it is necessary that the proof planner at the assertion level be equipped with an adequate infrastructure to be able to take full advantage of the inferences offered by the assertions. We went on to develop a framework for extracting important information from assertions in accordance to the reasoning context (i.e. the proof situation) in which the assertion is invoked. We describe a distributed modelling for our framework which serves as an assistant for proof search in Omega. This mechanism also reflects the cognitive process human agents employ when performing theorem proving: A skilled mathematician would in general accept conclusions emerged from algorithm AssertionApplication() as a trivial or obvious step and normally not require a detailed (i.e. logic level) explanation of such steps. The research bears immediate fruit through our application in the Dialog project aiming at building an intelligent mathematical tutoring system. The realization of natural language dialog in such a project should take full advantage of the assertion level proofs developed by our formalism.

Future work includes: (i) We want to investigate whether our approach scales to higherorder contexts. Additional problems have to be addressed, such as undecidability of higherorder unification, primitive substitution, etc. In higher-order contexts our distributed modeling will gain impact, since this will provide a flexible basis, for instance, to model iterative deepening over constraints such as a maximal unification depth. (ii) Equational reasoning is not yet addressed in our framework and needs to be investigated. In particular adapting our framework to (extensional) equational reasoning within higher-order logic contexts is a challenge. (iii) We propose to fully integrate automated proof planning with our approach to assertion level reasoning.

References

[1] P. Andrews. Transforming matings into natural deduction proofs. In W. Bibel and R. A. Kowalski, editors, Proc. 5th CADE, pages 281–292. Springer-Verlag, 1980.

[2] P. B. Andrews. Theorem proving via general matings. Journal of the ACM, 28(2):193– 214, 1981.

[3] S. Autexier. A proof-planning framework with explicit abstractions based on indexed formulas. Electronic Notes in Theoretical Computer Science, 58(2), 2001.

[4] C. Benzmüller et al. Tutorial dialogs on mathematical proofs. In Proceedings of IJCAI-03 Workshop on Knowledge Representation and Automated Reasoning for E-Learning Systems, 2003.

[5] C. Benzmüller, A. Meier, E. Melis, M. Pollet, and V. Sorge. Proof planning: A fresh start? In Proceedings of the IJCAR 2001 Workshop: Future Directions in Automated Reasoning, pages 25–37, Siena, Italy, 2001.

[6] C. Benzmüller, A. Meier, and V. Sorge. Bridging theorem proving and mathematical knowledge retrieval. In Festschrift in Honour of Jörg Siekmann, 2002.

[7] C. Benzmüller and V. Sorge. Oants – an open approach at combining interactive and automated theorem proving. In M. Kerber and M. Kohlhase, editors, Symbolic Computation and Automated Reasoning, pages 81–97. A.K.Peters, 2000.

[8] W. Bibel. Matings in matrices. Communications of the ACM, 26:844–852, 1983.

[9] A. Bundy. The use of explicit plans to guide inductive proofs. In Proc. CADE, pages 111–120, 1988.

[10] A. Bundy. A critique of proof planning. In A. C. Kakas and F. Sadri, editors, Computational Logic. Logic Programming and Beyond, volume 2408 of Lecture Notes in Computer Science. Springer, 2002.

[11] I. Dahn, A. Haida, T. Honigmann, and C. Wernhard. Using mathematica and automated theorem provers to access a mathematical library. In Proceedings of the CADE-15 Workshop on Integration of Deductive Systems, 1998.

[12] M. Fitting. Tableau methods of proof for modal logic. Notre Dame Journal of Formal Logic, 13:237–247, 1972.

[13] M. Fitting. First Order Logic and Automated Theorem Proving. Springer, 1990.

[14] G. Gentzen. Untersuchungen über das logische schliessen. Mathematische Zeitschrift, 39(176–210):405–431, 1935.

[15] S. Gerberding and B. Pientka. Structured incremental proof planning. In KI - Kunstliche Intelligenz, pages 63–74. Springer-Verlag, 1997.

[16] X. Huang. Reconstructing proofs at the assertion level. In A. Bundy, editor, Proc. 12th Conference on Automated Deduction, pages 738–752. Springer-Verlag, 1994.

[17] X. Huang, M. Kerber, J. Richts, and A. Sehn. Planning mathematical proofs with methods. J. Information Processing and Cybernetics, EIK, 30(5-6):277–291, 1994.

[18] R. Kowalski. A proof procedure using connection graphs. J. ACM, 22(4):572–595, 1975.

[19] E. Melis. Island planning and refinement. Tech. report, Saarland University, 1996.

[20] E. Melis and A. Meier. Proof planning with multiple strategies. In Proc. CL-2000, volume 1861, pages 644–653, 2000.

[21] E. Melis and J. Siekmann. Knowledge-based proof planning. AIJ, 115(1):65–105, 1999.

[22] N. V. Murray. Completely non-clausal theorem proving. AIJ, 18(1):67–85, 1982.

[23] N. V. Murray and E. Rosenthal. Inference with path resolution and semantic graphs. Journal of the ACM (JACM), 34(2):225–254, 1987.

[24] H. J. Ohlbach and J. H. Siekmann. The Markgraf Karl refutation procedure. In J. L. Lassez and G. Plotkin, editors, Computational Logic, Essays in Honor of Alan Robinson, pages 41–112. MIT Press, 1991.

[25] J. A. Robinson. A machine-oriented logic based on resolution principle. Journal of the ACM, 12(1):23–41, 1965.

[26] K. Schütte. Proof Theory. Springer Verlag, 1977.

[27] J. Siekmann et al. Proof development with Omega. In A. Voronkov, editor, Proc. 18th CADE, LNAI 2392, pages 144–149, Copenhagen, Denmark, 2002.

[28] J. Traugott. Nested resolution. In Jörg Siekmann, editor, Proc. 8th CADE, number 2392 in LNAI, pages 394–402, Copenhagen, Denmark, 1986. Springer.

[29] L. Wallen. Automated proof search in non-classical logics: effcient matrix proof methods for modal and intuitionistic logics. MIT Press series in AI, 1990.

Appendix

We introduce some notations which will be used in the establishments of the results presented in the following.

Model theory

We define the first-order language for the syntax of the calculus of interest in the standard way, cf. e.g. [13]. Let L be a first-order language, a (set-theoretic) structure for L is a pair ⟨D, ı⟩ where D is a non-empty set, the domain of the structure, and ı an interpretation of L in D. The satisfaction relation ⊧ between the set of structures and the wffs from L is also defined as usual.

For a structure M, we define:

M ⊧ φ^{⊖} iff M ⊧ φ

and

M ⊧ φ^{⊕} iff M |̸= φ

The following is an immediate corollary of the above definitions:

Corollary 1 Let M be a structure.

1. Exactly one of M ⊧ φ^{⊖} or M ⊧ φ^{⊕}.

2. M ⊧ α iff M ⊧ α_{1} and M ⊧ α_{2}.

3. M ⊧ β iff M ⊧ β_{1} or M ⊧ β_{2}.

4. M ⊧ (γ, x) iff for every c ∈ D, M ⊧ γ_{0}(x)[c/x].

5. M ⊧ (δ, x) iff for some c ∈ D, M ⊧ δ_{0}(c). In particular, the constant sko chosen by the (δ, x)-rule above is one of those constants c.

Notations

Let an SFT τ be given and η a node of τ, if the rule that is applied to η is an α (resp. β, γ, δ)-rule then η is said to be of type α (resp. β, γ, δ).

We warn the reader that we will systematically abuse our notation:

1. We will refer to an SFT as its root node and vice versa. Hence, we will be able to e.g. talk about the leaf node of a signed formula.

2. We shall also adopt the following practice of using the names of types to denote the formulae they are applied to (possibly with the reference to the formulae). That is:

• If φ is a signed formula of type α then we also refer to φ as α(φ) and its child(ren) as α_{1}(φ) and α_{2}(φ).

• If φ is a signed formula of type β then we also refer to φ as β(φ) and its children as β_{1}(φ) and β_{2}(φ).

• If φ is a signed formula of type (γ, x) then we also refer to φ as γ(φ, x) and its child as γ_{0}(φ, x).

• If φ is a signed formula of type (δ, x) then we also refer to φ as δ(φ, x) and its child as δ_{0}(φ, sko).

Soundness of algorithm GR

Theorem 1 (Soundness of GR) Let two SFTs τ_{1} and τ_{2} be given. For any structure M and any substitution θ, if M is a model of {τ_{1}θ, τ_{2}θ} then M is a model of GR(τ_{1}, η_{1}, τ_{2}, η_{2}, θ), for any pair of leaf nodes η_{1} of τ_{1} and η_{2} of τ_{2}.

The theorem is vacuously true in case η_{1} and η_{2} are not θ-complementary. Thus we only consider the case when they are θ-complementary. We will also assume that the only connectives we have to deal with are negation (¬), conjunction (wedge) and disjunction (vee) together with the first-order quantifiers (∀ and ∃)to simplify the presentation. We first show the following lemma:

Lemma 1 Let τ be an arbitrary SFT and ς a singleton SFT (i.e. ς itself is the only node of ς). For any structure M and any substitution θ, if M is a model of {τθ, ςθ}, M is a model of GR(τ, η, ς, ς, θ), for any leaf node η of τ.

Proof: By induction on the structure of τ.

Base case: τ is a singleton SFT with the only node being τ itself. τ and ς are θcomplementary. In other words, the set of models of {τθ, ςθ} is empty. Therefore, the lemma is vacuously true.

Inductive case:

1. Case τ is of type α:

(a) Case α_{2}(τ) = nil, i.e. τ has only one child α_{1}(τ): Obviously, form(τ) = form(α(τ)) = ¬(form(α_{1}(τ))) and polarity(α_{1}(τ)) = −polarity(α(τ)). For any structure M:

M is a model of {τθ, ςθ} iff M is a model of {α(τ)θ, ςθ} iff M is a model of {α_{1}(τ)θ, ςθ} (from Corollary 1).

Then, M is a model of GR(α_{1}(τ), η, ς, ς, θ) (inductive hypothesis). Therefore, M is a model of GR(τ, η, ς, ς, θ). The justification for the last step in the above proof is based on the reconstruction of the root node GR(τ, η, ς, ς, θ) from its only child GR(α_{1}(τ), η, ς, ς, θ) and from Corollary 1.

(b) Case α_{2}(τ) ≠ nil: For any structure M:

M is a model of {τθ, ςθ} iff M is a model of {α(τ)θ, ςθ} iff M is a model of {α_{1}(τ)θ, ςθ} and M is a model of {α_{2}(τ)θ, ςθ} (from Corol-

lary 1).

• Case η is a leaf node of α_{1}(τ): M is a model of GR(α_{1}(τ), η, ς, ς, θ) (inductive hypothesis) and M is a model of {α_{2}(τ)θ, ςθ}.

• Case η is a leaf node of α_{2}(τ): M is a model of {α_{1}(τ)θ, ςθ} and M is a model of GR(α_{2}(τ), η, ς, ς, θ) (inductive hypothesis).

Therefore, M is a model of GR(τ, η, ς, ς, θ) (from the reconstruction of GR(α(τ), η, ς, ς, θ) from GR(α_{1}(τ), η, ς, ς, θ) and GR(α_{2}(τ), η, ς, ς, θ)).

2. Case τ is of type β:

For any structure M:

M is a model of {τθ, ςθ}

iff M is a model of {β(τ)θ, ςθ}

iff M is a model of {β_{1}(τ)θ, ςθ} or M is a model of {β_{2}(τ)θ, ςθ} (from Corollary 1).

• Case η is a leaf node of β_{1}(τ): then, M is a model of GR(β_{1}(τ), η, ς, ς, θ) (inductive hypothesis). Therefore, M is a model of GR(β(τ), η, ς, ς, θ), from the reconstruction of β(τ)θ from GR(β_{1}(τ), η, ς, ς, θ) and β_{2}(τ)θ;

• Case η is a leaf node of β_{2}(τ): similar to the preceding case, M is a model of GR(β(τ), η, ς, ς, θ).

3. Case τ is of type (γ, x):

For any structure M:

M is a model of {τθ, ςθ}

iff M is a model of {γ(τ, x)θ, ςθ}

iff M is a model of {γ_{0}(τ, x)θ, ςθ} (from Corollary 1).

• Case xθ = x or xθ = y for some free variable y: x (resp. y) is a free variable in γ_{0}(τ, x)θ and form(γ(τ, x)) = ∀x(form(γ_{0}(τ, x))) (resp. form(γ(τ, x)) = ∀x(form(γ_{0}(τ, x))[y/x])). Thus, every model of GR(γ_{0}(τ, x), η, ς, ς, θ) is also a model of GR(γ(τ, x), η, ς, ς, θ) (which is essentially GR(τ, η, ς, ς, θ)). But from the inductive hypothesis, the structure M is a model of GR(γ_{0}(τ, x), η, ς, ς, θ).

• Case xθ = c for some c ∈ D: straightforwardly, γ(τ, x)θ = γ_{0}(τ, x)θ and from the reconstruction of GR(γ(τ, x), η, ς, ς, θ) from GR(γ_{0}(τ, x), η, ς, ς, θ), M is a model of GR(γ(τ, x), η, ς, ς, θ) (inductive hypothesis).

4. Case τ is of type (δ, x):

For any structure M:

M is a model of {τθ, ςθ}

iff M is a model of {δ(τ, x)θ, ςθ}

iff M is a model of {δ_{0}(τ, sko)θ, ςθ} (from Corollary 1).

Then, as δ(τ, x)θ = δ_{0}(τ, sko)θ and from the reconstruction of GR(δ(τ, x), η, ς, ς, θ) from GR(δ_{0}(τ, sko), η, ς, ς, θ), M is a model of GR(δ(τ, x), η, ς, ς, θ) (inductive hypothesis).

□

Proof: (of theorem 1)

As with the above lemma, we prove by induction on the structure of τ_{1}. First, we observe that for an arbitrary SFT τ_{2} and any substitution θ, if the structure M is a model of τ_{2}θ then M is also a model of the SFT obtained by (i) instantiating τ_{2} according to θ, then (ii) removing a leaf node of τ_{2}, and then (iii) reconstructing its internal nodes in the way described in algorithm GR. That result is essentially what has been shown in Lemma 1.

Base case: τ_{1} is a singleton SFT with the only node being τ_{1} itself, i.e. τ_{1} = η_{1}. The theorem holds by the above observation and from the fact that M is a model of φ^{p} if and only if M is a model of (¬φ)^{−p} for any formula φ and any polarity p. Thus it doesn’t matter whether η_{1} is replaced by τ_{2}θ or (¬form(τ_{2}θ))^{polarity(τ_{2}θ)}, the theorem should always hold.

Inductive case: The proof of the inductive case proceeds in the similar way to that for Lemma 1. I.e. we consider different cases on the type of the root node of τ_{1}. In particular, the same argument works for all four different types of the root node of τ_{1}, except for the γ and δ-types where special care must be taken for possible clashes of variables during the reconstruction process. □

When (classical) resolution on a pair of clauses Φ and Ψ is performed, no ordering between Φ and Ψ is necessary. The situation is slightly different for generalized resolution: GR(τ_{1}, η_{1}, τ_{2}, η_{2}, θ) and GR(τ_{2}, η_{2}, τ_{1}, η_{1}, θ) generally output two syntactically different SFTs. So, it is important that they be still logically equivalent. This is a straightforward corollary of the above theorem:

Corollary 2 Let two SFTs τ_{1} and τ_{2} be given. For any structure M and any substitution θ, M is a model of GR(τ_{1}, η_{1}, τ_{2}, η_{2}, θ) if and only if M is a model of GR(τ_{2}, η_{2}, τ_{1}, η_{1}, θ), for any pair of leaf nodes η_{1} of τ_{1} and η_{2} of τ_{2}.

Proof: First, we observe that: If M is a model of GR(τ_{1}, η_{1}, τ_{2}, η_{2}, θ) then

• M is a model of GR(τ_{1}, η_{1}, comp(η_{1}), comp(η_{1}), θ); and

• M is a model of GR(τ_{2}, η_{2}, comp(η_{2}), comp(η_{2}), θ).

where, given a signed formula τ, comp(τ) returns the complementary signed formula of τ. The above observation is immediate from Lemma 1.

Now, to prove that if M is a model of GR(τ_{1}, η_{1}, τ_{2}, η_{2}, θ) then M is a model of GR(τ_{2}, η_{2}, τ_{1}, η_{1}, θ), we can proceed by induction on the structure of τ_{2} with the base case follows from the above observation. Similarly, the inverse direction is proved by induction on the structure of τ_{1}. □

A further remark on algorithm GR():

Remark: Line (2) of algorithm GR() is inessential to the generalized resolution framework presented in this paper, i.e. it can be removed without affecting the correctness of algorithm GR(). This is a form of the inference rules Weakening well known in sequent calculi. This, however, brings out another advantage from the chosen representation: The redundancy that is apparent in the generalized resolution framework without Weakening can be easily eliminated by this line which effectively prunes all the subtrees that are α-related to the resulted resolvent, i.e. the redundant ones.

Resolving a pair of complementary non-atomic formulae

Observe that the framework presented so far in this paper could have been described for this general setting without any modification on the algorithm or the theorems. That will come with a price however. A large number of internal nodes will potentially explode the search space. Moreover, unification on internal nodes is more complex than unification on the leaf nodes only. Nevertheless, we will show that the framework we have proposed is sufficient to achieve such general steps of resolution, even though it could require more than one step of resolution on the leaf nodes.

Theorem 2 Let SFTs τ_{1} and τ_{2} be given. If η_{1} and η_{2} are two nodes of τ_{1} and τ_{2}, respectively, and θ is a substitution such that η_{1} and η_{2} are θ-complementary then the resolution of τ_{1} and τ_{2} over η_{1} and η_{2} can be achieved by repeatedly applying GR() on τ_{1} and τ_{2} and their resulting resolvents a finite number of times.

Proof: By induction on the structure of η_{1}:

Base case: Trivial as η_{1} and η_{2} are the leaf nodes of τ_{1} and τ_{2}.

Inductive case:

1. Case η_{1} is of type α:

(a) Case α_{2}(η_{1}) = nil: η_{1} is of the form (¬φ)^{p} for some polarity p. As η_{1} and η_{2} are θ-complementary, η_{2} must be of the form (¬ψ)^{−p} so that φθ = ψθ. Hence, α_{1}(η_{1}) = (φ)^{−p} and α_{1}(η_{2}) = (ψ)^{p}. Obviously, α_{1}(η_{1}) and α_{1}(η_{2}) are also θ-complementary. From the inductive hypothesis, we can resolve them after repeatedly applying GR() on τ_{1} and τ_{2} and their resulting resolvents k times. Therefore, the resolution of τ_{1} and τ_{2} over η_{1} and η_{2} can also be achieved after k applications of GR() on τ_{1} and τ_{2} and their resulting resolvents.

(b) Case α_{2}(η_{1}) ≠ nil:

• Case polarity(η_{1}) = ⊖: η_{1} is of the form (φ_{1} ∧ φ_{2})^{⊖}. Then η_{2} must be of the form (ψ_{1} ∧ ψ_{2})^{⊕} so that φ_{1}θ = ψ_{1}θ and φ_{2}θ = ψ_{2}θ. Therefore, from the inductive hypothesis, α_{1}(η_{1}) and α_{1}(η_{2}) are resolved after k applications of GR() on τ_{1} and τ_{2} and their resulting resolvents; and α_{2}(η_{1}) and α_{2}(η_{2}) are resolved after l applications of GR() on τ_{1} and τ_{2} and their resulting resolvents. As a consequence, η_{1} and η_{2} can be resolved after k + l applications of GR() on τ_{1} and τ_{2} and their resulting resolvents.

• Case polarity(η_{1}) = ⊕ is also similar.

2. Case η_{1} is of type β: similar to the case η_{1} is of type α and α_{2}(η_{1}) ≠ nil.

3. Case η_{1} is of type (γ, x): η_{1} is of the form (Q_{x}Φ(x))^{p} where Q ∈ {∀, ∃}. Then η_{2} must be of the form (Q_{y}Ψ(y))^{−p} so that Φ(x)(θ ∘ {x ↦ y}) = Ψ(y)θ. Therefore, from the inductive hypothesis, γ_{0}(η_{1}, x) and δ_{0}(η_{2}, sko) are resolved (under the substitution θ′ = θ ∘ {x ↦ sko}) after k applications of GR() on τ_{1} and τ_{2} and their resulting resolvents. As a consequence, η_{1} and η_{2} can be resolved after k applications of GR() on τ_{1} and τ_{2} and their resulting resolvents.

4. Case η_{1} is of type (δ, x): is symmetric to the preceding case, i.e. η_{1} is replaced by η_{2} and vice versa in the above argument.

□