Publication
Organisation, Transformation, and Propagation of Mathematical Knowledge in OMEGA
Serge Autexier; Christoph Benzmueller; Dominik Dietrich; Marc Wagner
In: Manfred Kerber (Hrsg.). Journal Mathematics in Computer Science, Vol. 2, No. 2, Pages 253-277, Birkhäuser, 12/2008.
Abstract
Mathematical assistance systems and proof assistance systems in general have traditionally been developed as large, monolithic systems which are often hard to maintain and extend. In this article we propose a component network architecture as a means to design and implement such systems. Under this view a mathematical assistance system is an integrated knowledge-based system composed as a network of individual, specialized components. These components manipulate and mutually exchange different kinds of mathematical knowledge encoded within different document formats. Consequently, several units of mathematical knowledge coexist throughout the system within these components and this knowledge changes non-monotonically over time. Our approach has resulted in a lean and maintainable system code and makes the system open for extensions. Moreover, it naturally decomposes the global and complex reasoning and truth maintenance task into local reasoning and truth maintenance tasks inside the system components. The interplay between neighboring components in the network is thereby realized by nonmonotonic updates over agreed interface representations encoding different kinds of mathematical knowledge.