Automated reasoning with a constraint-based metainterpreter

AbstractUsing 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