Automated reasoning with a constraint-based metainterpreter

Henning Christiansen
Department of Computer Science
Roskilde University, P.O.Box 260, DK-4000 Roskilde, Denmark


Using constraint logic techniques, it is made possible to use a well-known metainterpreter backwards as a device for generating programs. A metainterpreter is developed, which provides a sound and complete implementation of the binary demo predicate. Based on it, a general methodology for automated reasoning is proposed and it turns out that a wide range of reasoning tasks, normally requiring different systems, can be defined in a concise manner in this framework. Examples are shown of abductive and inductive reasoning in the usual first-order setting as well as in contexts of default reasoning and linear logic. Furthermore, examples of diagnosis and natural language analysis are shown.

See pdf.


Journal of Logic Programming, vol. 37, pp. 213-253, 1998.