INDUCTIVE INFERENCE OF FORMAL SYSTEMS FROM POSITIVE DATA

A formal system, we deal with in this paper, is a set of formulas of the form $ P_1(t_1) leftarrow P_2(t_2) \binampersand cdots \binampersand P_n(t_n) $, where $ P_1, P_2, cdots, P_n $ are predicate symbols and $ t_1, t_2, cdots, t_n $ are strings of constant symbols and variable symbols. The language defined by a formal system $ E $ is a set of constant strings $ t $ such that $ P_i(t) $ is provable from $ E $ by using rules of modus ponens and substitutions of constant strings for variable symbols. We restrict formal systems so as to contain only two formulas of a predicate, and also restrict substitutions not to map any variable to empty string. The class of languages defined by our restricted formal systems is a natural extension of Angluin\u27s pattern languages. We show that the class is inferable from positive data