Automated Reasoning with a Constraint-Based Metainterpreter

Using constraint logic techniques, it is made possible to use a wellknown 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.

• Type: Journal
• Year: 1998
• Where: JLP
• Authors: Henning Christiansen
• Keywords: Automated Reasoning, Constraint Logic Techniques, JLP 1998, Reasoning