The Model Inference System

The Model Inference System

Ehud Y. Shapiro'

Department of Computer Science Yale University New Haven . CT 06520

The Model Inference System is an interactive Prolog program [I) that infers theories from facts . It implements the general model inference algorithm. descri bed in [2). speciali7ed to infer theories in Horn form from atomic facts .

·1 he abstract setting in wh.ich the system operates. and from which it derives its name . is the following: the system is initially given some first order language L . There is some unknown modl·l M for L . and an oracle (user) that can supply facts and answer 4ucries on the truth or falsity of ground atoms in M . The goal of the system is to find a finite set of true Horn clauses. which imply all true ground atoms and no false ones.

The user inputs the predicate to he inferred and the tcrrT>s (predicate symhols. function symbols and constants) to he used in the intended axiornatitation of this predicate . After receivi ng the initial input . the system starts prompting the user for new facts . At each stage. the system maintains a set of hypotheses that arc sufficient to derive all true atoms and none of the false atoms supplied so far .

When an inconsistency is discovered between the hypotheses and the facts. the contradiction hack tracing algorithm is invoked . In order to resolve this contradiction. the algorithm may 4uery for the truth of atoms not supplied by the user yet. When the hypothese~ can not derive some atom known to he true . the system adds to the conjcl·turc refinements of previously refuted hypotheses.

The user sees the axiomati7ation as it is developed by the system. When he thinks the system has converged to a correct and sufficient axiomatitation of the predicate . he can terminate the inference process. It is his responsibility to terminate the system. since it is an inherent propert y of an inductive inference algmithm that it can never determine whether it has converged.

Hdow arc examples of the performance of the system. Further examples can he found in [2) . The system runs compiled using the in-core compiler of the Edinburgh Prolog- 10 version J. The computer is a DECsystem-2060. running Prolog-10 under the compatibility package PA 1050. In the following. the running time in CPU seconds measured the time the system took to converge to a correct and sufficient axiomati1.ation of the intended model. Fact., arc the number of facts read therein. and hypothl!.\'l'.\' l(l'lll'rated is the number of hypotheses generated by the refinement operator during the inference. The numbers following an axiom arc its SClJUCntial number as it was generated . and the number of refinement operations needed to generate it.

• Exponentiation: exp(X,Y,Z)- X to theY is Z. 2K CPU seconds. I!! facts. 252 hypotheses generated . (exp(X,O.s(O)) - true). 78. 2

(exp(X.s(Y).Z) -- exp(X,Y,W) ,times(W.X.Z)). 129. 2

(exp(O.s(X) ,O) - true). 148. 2

Member: member(X,Y) - X is a member of the list Y. 2 CPU seconds. 23 facts , IJ hypotheses generated .

(member(X.[YIZ)) - member(X.Z)) . 6. 3

(member(X,(XIYJ)- true). 7, 3

• Subset: subset( X, Y) -X is a subset of Y. 31 CPU seconds. K2 facts . 152 hypotheses generated .

(subset([].X) - true) , 1, 1

(subset(X.[YIX)) - true) . 32,3

(subset(X,[YIZ)) - subset(X.Z)). 34, 3

(subset([X] .[XIY))- true). 97,5

(subset([XIYJ ,[XIZ)) - · subset(Y,Z)) , 103. 5

(subset([>QY] ,Z)- subset(Y.Z) ,member(X.Z)). 113, 3

lnterchangt; int(X.Y) - Y is a list of pairs of X, where the order in each pa ir is interchanged .

19 <M>U seconds. 21 fact s. 110 ~ypothescs generated .

(int([].[]) :-true) . 6, 1

(int([[XIYJIZ].([YIXJIW)) -int(Z,W) .true) . 104, 9

Tree isomorphism: isotree(X.Y)- X is isomorphic toY. 20 CPU sec~mds. 110 facts. 117 hypotheses genera ted .

(isotree(X,X) -true) . 5. 1

(isotree(t(X.Y),t(Y,X))- true), 35, 5

(isotree(t(X,Y) .t(Y,Z))- isotree(X,Z)). 38, 5

(isotree(t(X,Y).t(Z.W))- isotree(Y.Z).isotree(X.W)). 41 ,

(isotree(t(X,Y),t(Z,X))- isotree(Y.Z)). 44, 5

(isotree(t(X.Y).t(Z.Y))- isotree(X,Z)). 103, 5

(isotree(t(X,Y).t(Z.W))- isotree(Y,W).isotree(X.Z)) . 108