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.