The method of synthesis of derivability conditions for Horn formulas and some other formulas

A method is given for synthesis of derivability conditions for formulas whose negations can be represented as Horn-type or as disjunctions of Horn-type formulas. These conditions are generated as solutions of the logical equation and are necessary if the process of inference and synthesis is finite and if the synthesis is applied only when the inference cannot be continued. The method restricts the combinatorial space of theorem synthesis by logical equations which bring substantial reduction of combinatorics. Special conditions of mutual compatibility between known members of the equation need not be satisfied a priori. Sufficiently pithy conditions satisfying some compromise between the criteria of deductive unimprovability (necessity) and simple verification of satisfiability are obtained. This paper also has some interrelations with inductive logic programming, which is defined as the method of extending the set of axioms of a particular theory such that the extended theory would be able to explain an assigned set of examples