In this talk I shall present an agent based approach to automated and interactive reasoning. The approach is motivated by the discrepancy of the flexible problem solving behavior of human mathematicians on the one hand and the control determination of automated reasoning systems on the other hand. Depending on the specific nature of a challenging problem in real mathematics or engineering different specialists may have to cooperate and bring in their expertise to effectively tackle a problem. Even a single mathematician possesses a large repertoire of often very specialized reasoning and problem solving techniques. But instead of applying them in a fixed structure, a mathematician uses own experience and intuition to flexibly combine them in an appropriate way.
Although classical automated theorem provers and proof planners have reached an impressive power and do already outperform humans in particular problem domains, these systems often perform poorly when applied to new domains. Especially proof planning has a problem if accurate method and/or control knowledge for the new domain is lacking. Cross domain problems also provide a good example as they typically require the combination of quite heterogeneous reasoning techniques. In extreme cases the required spectrum reaches from different theorem proving strategies to symbolic computation or model generation.
A recent trend in the automated reasoning community therefore is to integrate specialized external reasoning systems in a central theorem proving environment. However, in traditional theorem proving as well as proof planning external reasoning systems are integrated in a quite hard-wired fashion making a flexible, reactive interplay impossible. Instead the control mechanismen of the central prover typically precisely determines when external systems are applied and how they cooperate. Furthermore, the adaptation of these static control mechanisms at run-time is rarely possible. As a consequence, for instance, proof subgoals that could be automatically solved by an integrated external reasoner within seconds may remain undetected simply because appropriate control knowledge is not available in the core system. This clearly contradicts with the intuitive or unconscious handling of different proof strategies of human mathematicians.
In contrast to hard-wired integrations our approach provides a flexible integration framework for machine-oriented theorem proving, tactical theorem proving, proof planning, and computation. It encapsulates proof rules, tactics, methods, and external systems in single reasoning agents and uses state of the art distribution techniques to decentralize and spread them over the internet. The approach particularly supports cooperative proofs between reasoning agents which are strong in different applications areas, e.g., higher-order and first-order theorem provers, and computer algebra systems. Nevertheless, the integration approach is a skeptical one and assumes that the contributions of external systems can be translated in a central proof object (based on a higher-order variant of Gentzen's natural deduction calculus), where they can be verified at fully expanded calculus level or investigated by the user at a more user friendly abstract level.
Our approach particularly allows a number of heterogeneous proof search attempts to be executed in parallel. This includes tackling a goal with different integrated theorem provers as well as checking for counterexamples with an integrated model generator. If these reactive proof attempts fail, the integrated reasoners may cooperate by exchanging interesting partial results via the central proof object. Resource management is employed to distribute available resources amongst the available reasoning agents in order to determine their maximum reasoning time and to prevent them from a quick consumption of all available resources. Generally our approach supports parallelization of reasoning tasks on term level, inference level, and proof search level and external systems can not only be employed to support object level proof search but also to support meta-level reasoning, for instance, by checking complicate application conditions of inference rules.
Additional advantages of our approach consist in the close integration of automation and interaction and the potentiality to add, delete, or modify reasoning agents and control information at run-time. These features are based on the special characteristics of the Omega-ants blackboard mechanism forming the core of our system. The task of the Omega-ants agents (the knowledge sources of the blackboards) is to test the applicability of rules, tactics, methods, and external reasoners in a given proof state and to suggest appropriate parameter instantiations for them. The resulting suggestions are offered for execution to the interactive user and the automated prover simultaneously.
The system has been successfully applied to different problems about sets and currently also to prove the equivalence of different group definitions. The set examples are successfully classified in valid and invalid statements in a reactive interplay of natural deduction proof search, higher-order and first-order resolution style theorem proving, computation, and refutation with a model generator. Thereby the system demonstrated a resource adapted proof search behavior. However, the main bottleneck for obtaining large proofs is the translation between the different systems involved, in particular, of large clause sets.
The system is realized in the Saarbrücken Omega proof environment, and implemented in concurrent, object-oriented Lisp. However, conceptually it does not depend on this framework. We belief that it is even independent of the theorem proving context and may be adapted to other rule based reasoning systems.
The agent-based reasoning framework is joint work with my colleagues Volker Sorge (Saarland University), Manfred Kerber, and Mateja Jamnik (The University of Birmingham).
The contents of this web page are not covered by the AISB Creative Commons Licence.