An Algorithm that Infers Theories from Facts

Abstract

A framework for inductive inference in logic is presented: a Mode/Inference Problem is defined, and it is shown that problems of machine learning and program synthesis from examples can be formulated naturally as model inference problems. A general. incremental inductive inference algorithm for solving model inference problems is developed. This algorithm is based on Popper's methodology of conjectures and refutations [II]. The algorithm can be shown to identify in the limit [3] any model in a family of complexity classes of models. is most powerful of its kind, and is flexible enough to have been successfully implemented for several concrete domains . The Model Inference System is a Prolog implementation of this algorithm, specialized to infer theories in Horn form . It can infer axiomatizations of concrete models from a small number of facts in a practical amount of time.