Small is Beautiful: A Brute-Force Approach to Learning First-Order Formulas

Book One

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 12

Automated Reasoning

We describe a method for learning formulas in first-order logic using a brute-force, smallest-first search. The method is exceedingly simple. It generates all irreducible well-formed formulas up to a fixed size and tests them against a set of examples. Although the method has some obvious limitations due to its computational complexity, it performs surprisingly well on some tasks. This paper describes experiments with two applications of the method in the MULTI-TAC sys- tem, a program synthesizer for constraint satisfaction problems. In the first application, axioms are learned, and in the second application, search control rules are learned. We describe these experiments, and consider why searching the space of small formulas makes sense in our applications.