Synthesizing Proof Planning Methods and Ω-Ants Agents from Mathematical Knowledge

摘要

In this paper we investigate how to extract proof procedural information contained in declarative representations of mathematical knowledge, such as axioms, definitions, lemmas and theorems (collectively called assertions) and how to effectively include it into automated proof search techniques. In the context of the proof planner MULTI and the agent-based reasoning system Ω-ANTS, we present techniques to automatically synthesize proof planning methods and Ω-ANTS-agents from assertions such that they can be actively used by these systems. This in turn enables a user to effectively use these systems without having to know the peculiarities of coding methods and agents.