Proof planning is an application of AI-planning in mathematical do- mains. One of its strengths comes from the usage of mathematical knowledge that heuristically restricts the search space. We investigate problem classes for which little or no heuris tic control knowledge is available and test the usage of randomization and restart techniques for "search control". This approach does not rely on domain-specific con trol knowledge but takes advantage of the surprising diversity of proofs in ter ms of the size and style.

Often user interfaces of theorem proving systems focus on assisting particularly trained and skilled users, i.e., proof experts. As a result, the systems are difficult to use for non-expert users. This paper describes a paper and pencil HCI experiment, in which (non-expert) students were asked to make suggestions for a GUI for an interactive system for mathematical proofs. They had to explain the usage of the GUI by applying it to construct a proof sketch for a given theorem. The evaluation of the experiment provides insights for the interaction design for non-expert users and the needs and wants of this user group.

We present some novel classification results in quasigroup and loop theory. For quasigroups up to size 5 and loops up to size 7, we describe a unique property which determines the isomorphism (and in the case of loops, the isotopism) class for any example. These invariant properties were generated using a variety of automated techniques --- including machine learning and computer algebra --- which we present here. Moreover, each result has been automatically verified, again using a variety of techniques --- including automated theorem proving, computer algebra and satisfiability solving --- and we describe our bootstrapping approach to the generation and verification of these classification results.

We extend our previous study of the automatic construction of isomorphic classification theorems for algebraic domains by considering the isotopy equivalence relation. Isotopism is an important generalisation of isomorphism, and is studied by mathematicians in domains such as loop theory. This extension was not straightforward, and we had to solve two major technical problems, namely, generating and verifying isotopy invariants. Concentrating on the domain of loop theory, we have developed three novel techniques for generating isotopic invariants, by using the notion of universal identities and by using constructions based on subblocks. In addition, given the complexity of the theorems that verify that a conjunction of the invariants form an isotopy class, we have developed ways of simplifying the problem of proving these theorems. Our techniques employ an interplay of computer algebra, model generation, theorem proving, and satisfiability-solving methods. To demonstrate the power of the approach, we generate isotopic classification theorems for loops of size 6 and 7, which extend the previously known enumeration results. This work was previously beyond the capabilities of automated reasoning techniques.

The classification of mathematical structures plays an important role for research in pure mathematics. It is, however, a meticulous task that can be aided by using automated techniques. Many automated methods concentrate on the quantitative side of classification, like counting isomorphism classes for certain structures with given cardinality. In contrast, we have devised a bootstrapping algorithm that performs qualitative classification by producing classification theorems that describe unique distinguishing properties for isomorphism classes. In order to fully verify the classification it is essential to prove a range of problems, which can become quite challenging for classical automated theorem provers even in the case of relatively small algebraic structures. But since the problems are in a finite domain, employing Boolean satisfiability solving is possible. In this paper we present the application of satisfiability solvers to generate fully verified classification theorems in finite algebra. We explore diverse methods to efficiently encode the arising problems both for Boolean SAT solvers as well as for solvers with built-in equational theory. We give experimental evidence for their effectiveness, which leads to an improvement of the overall bootstrapping algorithm.

Proof planning is an application of AI-planning in mathematical domains. In particular, the incorporation and use of domain knowledge in the planning process has enabled the derivation of mathematical theorems that lay outside the scope of purely logic-based theorem proving systems (such as resolution provers). So far, exist ing applications often benefit from the existence of domain knowledge whose usage leads to very restricted search spaces. This facilitates the proving process for problems whose proofs are in a restricted search space but it excludes many problems and restricts the kinds of proofs that can be found for a given problem instance. Moreover, acquiring appropriate domain knowledge has proven to be quite challenging. Our proposal, supported by an empirical evaluation, is to make the proof planning process more general and more robust with regard to domain specific knowledge. Our work extends knowledge-based proof planning by incorporating a set of randomization rules into the planning process. Such an approach does not rely on finely tuned domain-specific control knowledge and is hence successful in domains that lack strong control information. Rather the approach takes advantage of the surprising diversity in terms of the size and style of possible proofs.

In a problem solving process, a step may not result in the expected progress or may not be applicable as expected. Hence, knowledge how to overcome and react to impasses and other failures is an important ingredient of successful mathematical problem solving. To employ such knowledge in a proving system requires a variety of behaviors and a flexible control. Multi-strategy proof planning is a knowledge-based theorem proving approach that provides a variety of strategies and knowledge-based guidance for search at different levels. This paper introduces reasoning about impasses as a natural ingredient of meta-reasoning at a strategic level and illustrates the use of knowledge about failure handling in the proof planner multi.

A practically useful mathematical assistant system requires the sophisticated combination of interaction and automation. Central in such a system is the proof data structure, which has to maintain the current proof state and which has to allow the flexible interplay of various components including the human user. We describe a parameterized proof data structure for the management of proofs, which includes our experience with the development of two proof assistants. It supports and bridges the gap between abstract level proof explanation and low-level proof verification. The proof data structure enables, in particular, the flexible handling of lemmas, the maintenance of different proof alternatives, and the representation of different granularities of proof attempts.

Monitoring a solution process and applying the right action at the right moment are at the heart of intelligent problem solving by humans. This includes the analysis of failure events and the development of “recommendations” to overcome typical failures. In this article, we present how meta-reasoning on failures is used in multiple-strategy proof planning with the Multi system. Multi allows for a flexible traversal of the search space and a flexible construction of the proof plan guided by mathematically motivated heuristics. Because of the flexible control in Multi failures can be exploited to guide subsequent proof plan manipulations and refinements. The failure reasoning cannot only ease the derivation of a solution proof plan but is required for some problems to find a solution at all.

Ωmega is a mixed-initiative system with the ultimate purpose of supporting theorem proving in main-stream mathematics and mathematics education. The current system consists of a proof planner and an integrated collection of tools for formulating problems, proving subproblems, and proof presentation.

The CASC competitions among automated theorem provers show that there is no single system that outperforms all other systems in all domains. One reaction to this observation is the combination of several systems in a competitive (e.g., the SSCPA system) or cooperative manner (e.g., the CSSCPA and TECHS systems). Thereby, general-purpose heuristics select promising systems to be executed and promising intermediate results to be exchanged. Typically, exchanged results are restricted to clauses or equations that are accepted by all systems. The use of particular domain-specific services for particular subtasks such as the construction of mathematical objects and their flexible cooperation with other services guided by mathematically motivated control knowledge is not possible.

We propose a new benchmark set consisting of problems generated during the construction of classification theorems for quasigroups. It extends and generalises the domain of quasigroup existence problems, to which SAT solvers have been applied successfully in the past, to a rich class of benchmarks of varying difficulty.

Often user interfaces of theorem proving systems focus on assisting particularly trained and skilled users, i.e., proof experts. As a result, the systems are dicult to use for non-expert users. This paper describes a paper and pencil experiment, in which (non-expert) students were asked to make suggestions for a GUI for an interactive system for mathematical proofs. They had to explain the usage of the GUI by applying it to construct a proof sketch for a given theorem. The evaluation of the experiment provides insights for the interaction design for non-expert users and the needs and wants of this user group.

Mathematical tools such as computer algebra systems and interactive and automated theorem provers are complex systems and can perform difficult computations. Typically, such tools are used by a (small) group of particularly trained and skilled users to assist in mathematical problem solving. They can also be used as back-engines for interactive exercises in learning environments. This, however, suggests the adaptation of the choice of functionalities of the tool to the learner. This paper addresses the adaptive usage of the proof planner MULTI for the learning environment ACTIVEMATH. The proof planner is a back-engine for interactive proof exercises. We identify different dimensions in which the usage of such a service system can be adapted and investigate the architecture realizing the adaptive access to MULTI.

The classification of mathematical structures is a driving f orce in pure mathematics. A first step in producing algebraic classificat on theorems is to determine for which sizes certain algebras exist. Computatio n l approaches to solving such existence problems using constraint satisfaction and model generation approaches have had much success. We look here at the questio n of distributing the model generation process using Grid technology. We pres ent a novel distribution approach which involves using the HR machine learnin g program to intelligently suggest specialisations of the problem which are g iv n to separate processors. Using the MACE, FINDER and SEM model generators, we demonstrate how this approach provides greater efficiency over a singleprocess approach for a series of quasigroup existence problems. We compare sever al approaches for the production and choice of specialisations, including th e generation of proved classification theorems for algebraic structures of small s izes. We discuss how this approach could be used for more general problems.

Classifying finite algebraic structures has been a major motivation behind much research in pure mathematics. Automated techniques have aided in this process, but this has largely been at a quantitative level. In contrast, we present a qualitative approach which produces verified theorems, which classify algebras of a particular type and size into isomorphism classes. We describe both a semi-automated and a fully automated bootstrapping approach to building and verifying classification theorems. In the latter case, we have implemented a procedure which takes the axioms of the algebra and produces a decision tree embedding a fully verified classification theorem. This has been achieved by the integration (and improvement) of a number of automated reasoning techniques: we use the Mace model generator, the HR and C4.5 machine learning systems, the Spass theorem prover, and the Gap computer algebra system to reduce the complexity of the problems given to Spass. We demonstrate the power of this approach by classifying loops, groups, monoids and quasigroups of various sizes.

Today, most theorem proving systems are either used by their developers or by a (small) group of particularly trained and skilled users. In order to make theorem proving functionalities useful for a larger clientele we have to ask \What does an envisioned group of users need? For educational purposes a theorem prover can be used in dieren t scenarios and can serve students with dieren t needs. Therefore, the user interface as well as the choice of functionalities of the underlying prover have to be adapted to the context and the learner. In this paper, we present proof planning as back-engine for interactive proof exercises as well as an interaction console, which is part of our graphical user interface. Based on the proof planning situation, the console oers suggestions for proof steps to the learner. These suggestions can dynamically be adapted, e.g., to the user and to pedagogical criteria using pedagogical knowledge on the creation and presentation of suggestions.