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]END OF PROGOL TRACE
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).
Home Page