Assertion Application in Theorem Proving and Proof Planning

1 Proof planning at the assertion level

Due to Huang [6], the notion of assertion comprises mathe­ matical knowledge from a mathematical knowledge base KB such as axioms, definitions, and theorems. Huang argues that an assertion-based representation, i.e. assertion level, is just the right level for machine generated proofs to be transformed into 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 [7].

We are convinced that by planning directly on the asser­ tion level it will be possible to overcome at least some of the identified limitations and problems of proof planning as dis­ cussed in [3; 5]- in particular, those, that are caused by an unfortunate intertwining of proof planning and calculus level theorem proving. The perspective we therefore motivate is to consider the assertion level as a well chosen borderline be­ tween proof planning and machine oriented methods. De­ termining the logical consequences of assertions in a proof context is the task of machine oriented methods (in our case generalized resolution). The tasks on top of this level - for instance, an domain dependent containment of the initial as­ sertions to be considered, the heuristic selection of the most promising among the computed logical consequences, the in­ troduction, 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 resulted proof plans and also facilitate better user interaction.

The development of our ideas revolves around the math­ ematical assistant system OMEGA [8] and the current initiative in this project to rebuild the system on top of the proof representation framework in [1; 2]. We furthermore employ OMEGA's agent-based search mechanism OANTS [4] 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 Assertion Application via Generalized Resolution

Depending on the proof context there may be several ways in which an assertion can be used. For instance, the assertion

vsl, s2 : Set.(Sl ~ s2 {:::> Vx: Element.(x E sl =>X E S2))

allows us to derive: (1) a E V from a E U and U ~ V, (2) U ~ V from a E U and a fl. V, (3) Vx : Element.(x E U => x E V) from U ~ V, (4) etc.

Traditional theorem provers or proof planners that operate on 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. We propose an algorithm Assertion Application based on a generalized form of resolution in order to achieve such conclusions in one step for arbitrary assertions and proof contexts at hand. The algorithm, which is described in [9], is based on:

1. The representation of formulas as signed formula trees (SFT); see also [1; 2]. This way we achieve access to the literals of the formulas without breaking them apart.
2. The lifting of the resolution idea to directly operate on complementary and unifiable literals in SFTs instead of working on (unintuitive) normal forms .
3. The exhaustive application of (2) to the SFTs generated for the assertion and the formulas of the proof context.

3 Modeling Assertion Agents

In our implementation of mediator M we model assertion ap­ plication in form of distributed search processes employing the OANTS approach [4]. This agent based formalism is the driving force behind distributed proof search in OMEGA.

The general application scenario we have in mind is a the­ orem prover TP that is connected to an independent math­ ematical knowledge base KB. TP is focusing a proof task T consisting of the formula TP has to prove, viz. the theorem H , and a set of assumptions it can use to prove H . TP can deter­ mine the relevant parts, i.e. the related theories Th, from KB and hand them over to our assertion module M. The task of M is to compute with respect to proof task T all possible logical consequences of the available assertions B; taken from T h.

We propose to create for each assertion B; one associated instance AQ a, of a generic assertion agent AQ. The generic assertion agent AQ is based on our algorithm AssertionAppli­ cation. 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 AssertionAp­ plication . Each assertion agent instance AQ B, computes and suggest the logical consequences of B; for proof task T to our module M which passes them further to TP.

Depending on the size of KB there could be too many ap­ plicable assertions passed to M and also too many ways an assertion can be applied. One possibility is to restrict the search space by imposing prerequisites for assertion retrieval. For instance, a proof planner may employ its domain specific meta knowledge to formulate and pass respective context sen­ sitive syntactical filter criteria to the mediator for an efficient preselection by syntactic means.

Proof planning, however, has developed more sophisti­ cated ways to guide and constrain possible the possible in­ stantiations and applications of assertions. The investigation on how these techniques can optimally be employed on top of our assertion application module Mare further work.

4 An application: The DIALOG project

Our approach to assertion application is motivated by an ap­ plication in the DIALOG project as part of the Collaborative Research Center on Resource adaptive cognitive processes at Saarland University. The goal of this research project is (i) to empirically investigate flexible dialogue management strategies in complex mathematical tutoring dialogues, and (ii) to develop an experimental prototype system gradually embodying the empirical findings. The experimental system will engage in a dialogue in natural language (and perhaps other modes of communication) and help a student to under­ stand and produce mathematical proofs. It is important that such a system is supported by a human oriented mathematical proof development environment and the OMEGA system with its advanced proof presentation and proof planning facilities is a suitable answer to this requirement.

The overall scenario for DIALOG is: A student user is first taking an interactive course on some mathematical domain (e.g., naive set theory) within a web-based learning environ­ ment. When finishing some sections the student is asked by the system to test his learning progress by actively applying the studied lesson material by performing an interactive proof exercise. Since the learning environment is equipped with user monitoring and modeling facilities a user model is main­ tained and dynamically updated containing information on the axioms, definitions, and theorems (hence the assertions) the student has studied so far. Also a tutor model is available for each exercise containing information on the mathematical material that should be employed and tested by it.

In this scenario we expect the mathematical assistant systern to be capable of (i) stepwise-interactive and/or (ii) auto­ mated proof construction at a human oriented level of granu­ larity for the proof exercise at hand using exactly the mathe­ matical information specified in the (a) tutor model or (b) user model. The proofs constructed for (a) reflect what we want to teach and the proofs for (b) what the system expects the user to be capable of. For interactive tutorial dialog the sup­ port for a stepwise proof construction with the mathematical assistant system is of course important, while fully automati­ cally generated proofs are needed to be able to also give away complete solutions or to initially generate a discourse struc­ ture for the dialog on the chosen exercise. We want to stress that the user model may be updated also during an exercise, 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 applica­ tion 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.

5 Conclusion

Mediating mathematical knowledge between (web-based) mathematical knowledge bases, mathematical reasoning sys­ tems and human users is a mathematical knowledge manage­ ment task of increasing importance. We sketched a flexible and distributed solution for the subtasks of suggesting the logical consequences of assertions at an intuitive reasoning level.