Proceedings 6èmes Journées Bases de Données Avancées, 25. - 28.09.1990, Montpellier.
Over the recent years, several proposals
were made to enhance database systems with automated
reasoning. In this article we analyze two such enhancements
based on meta-interpretation. We consider on the
one hand the theorem prover Satchmo, on the other hand
the Alexander and Magic Set methods. Although they achieve
different goals and are based on distinct reasoning
paradigms, Satchmo and the Alexander or Magic Set
methods can be similarly described by upside-down
meta-interpreters, i.e., meta-interpreters implementing one
reasoning principle in terms of the other. Upside-down
meta-interpretation gives rise to simple and efficient implementations,
but has not been investigated in the past.
This article is devoted to studying this technique. We show
that it permits one to inherit a search strategy from an
inference engine, instead of implementing it, and to combine
bottom-up and top-down reasoning. These properties
yield an explanation for the efficiency of Satchmo and a
justification for the unconventional approach to top-down
reasoning of the Alexander and Magic Set methods.