The following is a trace of Progol learning to multiply two numbers.
The trace was generated at verbosity level 1, which makes Progol
slightly more talkative than is usual. It shows various intermediate
steps in theory construction, enclosed within "[" and "]". In
the search, this trace shows every clause tried by Progol.
Each clause is preceded by 4 numbers. These are, in turn,

f = Number of positive examples covered - Number of negative examples covered - Number of literals in body of clause - Optimistic estimate of literals needed p = Number of positive examples covered n = Number of negative examples covered h = Optimistic estimate of literals needed

*
BEGINNING OF PROGOL TRACE
*

CProgol Version 4.1 [:- modeb(1,dec(+int,-int))? - Time taken 0.00s] [:- modeb(1,plus(+int,+int,-int))? - Time taken 0.00s] [:- modeb(1,inc(+int,-int))? - Time taken 0.00s] [:- modeb(1,mult(+int,+int,-int))? - Time taken 0.00s] [:- modeb(1,plus(+int,+int,-int))? - Time taken 0.02s] [:- modeh(1,plus(+int,+int,-int))? - Time taken 0.00s] [:- modeh(1,mult(+int,+int,-int))? - Time taken 0.00s] [:- determination(plus/3,dec/2), determination(plus/3,inc/2), determination(plus/3,plus/3)? - Time taken 0.02s] [:- determination(mult/3,dec/2), determination(mult/3,plus/3), determination(mult/3,mult/3)? - Time taken 0.00s] [:- commutative(mult/3), commutative(plus/3)? - Time taken 0.00s] [:- set(c,3)? - Time taken 0.00s] [Testing for contradictions] [No contradictions found] [Generalising plus(4,X,Y) :- inc(X,U), inc(U,V), inc(V,W), inc(W,Y).] [Most specific clause is] plus(A,B,C) :- dec(A,D), inc(B,E), dec(D,F), plus(D,B,G), plus(D, E,C), inc(D,A), inc(E,H), dec(F,I), plus(F,B,H), plus(F, E,G), plus(F,F,A), plus(F,H,C), inc(F,D), inc(G,C), inc(H, G). [C:-2,6,5,3 plus(A,B,C).] [C:-3,4,4,2 plus(A,B,C) :- dec(A,D).] [C:-3,4,4,1 plus(A,B,C) :- dec(A,D), inc(B,E).] [C:1,4,0,0 plus(A,B,C) :- dec(A,D), inc(B,E), plus(D,E,C).] [C:-3,5,5,2 plus(A,B,C) :- inc(B,D).] [5 explored search nodes] [f=1,p=4,n=0,h=0] [Result of search is] plus(A,B,C) :- dec(A,D), inc(B,E), plus(D,E,C). [4 redundant clauses retracted] [Generalising plus(0,X,X).] [Most specific clause is] plus(A,B,B) :- plus(A,A,A). [C:-1,1,2,0 plus(A,B,B).] [C:-2,3,5,0 plus(A,B,C).] [2 explored search nodes] [f=-1,p=1,n=2,h=0] [No compression] [Generalising plus(X,0,X).] [Most specific clause is] plus(A,B,A) :- plus(B,B,B). [C:0,1,1,0 plus(A,B,A).] [C:-2,3,5,0 plus(A,B,C).] [2 explored search nodes] [f=0,p=1,n=1,h=0] [No compression] plus(0,X,X). plus(X,0,X). plus(A,B,C) :- dec(A,D), inc(B,E), plus(D,E,C). [Total number of clauses = 3] [Time taken 0.398s] [Generalising mult(4,X,Y) :- plus(X,X,Z), plus(X,Z,Z1), plus(X,Z1,Y).] [Most specific clause is] mult(A,B,C) :- dec(A,D), plus(B,B,E), dec(D,F), plus(B,E,G), mult(D,B,G), dec(F,H), plus(B,G,C), plus(F,F,A), mult(F, B,E), mult(F,F,A). [C:-19,5,21,3 mult(A,B,C).] [C:-19,4,20,2 mult(A,B,C) :- dec(A,D).] [C:-13,4,14,1 mult(A,B,C) :- dec(A,D), mult(D,B,E).] [C:1,4,0,0 mult(A,B,C) :- dec(A,D), mult(D,B,E), plus(B,E,C).] [4 explored search nodes] [f=1,p=4,n=0,h=0] [Result of search is] mult(A,B,C) :- dec(A,D), mult(D,B,E), plus(B,E,C). [4 redundant clauses retracted] [Generalising mult(0,X,0).] [Most specific clause is] mult(A,B,A) :- plus(A,A,A), plus(A,B,B), mult(A,A,A). [C:-1,1,2,0 mult(A,B,A).] [C:-19,2,21,0 mult(A,B,C).] [2 explored search nodes] [f=-1,p=1,n=2,h=0] [No compression] mult(0,X,0). mult(A,B,C) :- dec(A,D), mult(D,B,E), plus(B,E,C). [Total number of clauses = 2] [Time taken 0.498s]

*
*
The final output from Progol are the following clauses:

plus(0,X,X). plus(X,0,X). plus(A,B,C) :- dec(A,D), inc(B,E), plus(D,E,C). mult(0,X,0). mult(A,B,C) :- dec(A,D), mult(D,B,E), plus(B,E,C).

Back to Progol page.

Home Page