pred_def( void/0, [], [], [] ). init_clause(( void :- true )). ex( void, true ). pred_def( iid/2, [ +pl0, -pl0 ], [], [] ). % test PL0 number pred_def( nnum/2, [ +pl0, -pl0 ], [], [] ). % test PL0 addition operators (plus and minus) pred_def( aadd_op/2, [ +pl0, -pl0 ], [], [] ). % test PL0 multiplication operators (times and divide) pred_def( mmul_op/2, [ +pl0, -pl0 ], [], [] ). % test PL0 relational operators (times and divide) pred_def( rrel_op/2, [ +pl0, -pl0 ], [], [] ). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % PL0 expression pred_def( eexpr/2, [ +pl0, -pl0 ], [ eexpr/2, aa_op/2, mmul_op/2, iid/2, nnum/2 ], [] ). ex( eexpr( [ a ], [] ), true ). ex( eexpr( [ 1 ], [] ), true ). ex( eexpr( [ +, b, 3 ], [] ), true ). ex( eexpr( [ -, c, 2 ], [] ), true ). ex( eexpr( [ +, *, d, 6, 7 ], [] ), true ). ex( eexpr( [ /, a, +, c, 2 ], [] ), true ). /* if mis_dcg: eexpr(X,Y):-mmul_op(X,Z),eexpr(Z,U),eexpr(U,Y). eexpr(X,Y):-aadd_op(X,Z),eexpr(Z,U),eexpr(U,Y). eexpr(X,Y):-nnum(X,Y). eexpr(X,Y):-iid(X,Y). */ % L.P. %type_def(pl0,nom,[begin,end,if,then,while,do,call,:=,;,'(',')',+,-,*,/,<,=]). pred_def( eexpr1/2, [ +pl0, -pl0 ], [ eexpr/2, aa_op/2, mm_op/2, iid/2, nnum/2 ], [] ). ex( eexpr1( [ a ], [] ), true ). ex( eexpr1( [ 1 ], [] ), true ). ex( eexpr1( [ b, +, 3 ], [] ), true ). ex( eexpr1( [ c, -, 2 ], [] ), true ). ex( eexpr1( [ d, *, 6, +, 7 ], [] ), true ). ex( eexpr1( [ a, /, c, +, 2 ], [] ), true ). pred_def( aa_op/2, [ +pl0, -pl0 ], [], [] ). aa_op --> ['+']. aa_op --> ['-']. /* eexpr1(X,Y):-iid(X,[/|Z]),iid(Z,[+|U]),nnum(U,Y). eexpr1(X,Y):-iid(X,[*|Z]),nnum(Z,[+|U]),nnum(U,Y). eexpr1(X,Y):-iid(X,Z),aa_op(Z,U),nnum(U,Y). eexpr1(X,Y):-nnum(X,Y). eexpr1(X,Y):-iid(X,Y). */ pred_def( mm_op/2, [ +pl0, -pl0 ], [], [] ). mm_op --> ['*']. mm_op --> ['/']. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Arithmetic: Relation less-or-equal pred_def( aaleq/2, [ +int, +int ], [ aaleq/2 ], [] ). ex( aaleq( 0, s(0) ), true ). ex( aaleq( s(s(s(0))), s(s(s(s(0)))) ), true ). ex( aaleq( s(s(0)), s(0) ), false ). ex( aaleq( s(s(0)), s(s(s(0))) ), true ). ex( aaleq( s(s(0)), s(s(0)) ), true ). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Arithmetic: Addition pred_def( aaplus/3, [ +int, +int, -int ], [ aaplus/3 ], [] ). ex( aaplus( 0, s(0), s(0) ), true ). ex( aaplus( s(0), s(0), s(0) ), false ). ex( aaplus( s(s(0)), s(s(0)), s(s(s(s(0)))) ), true ). ex( aaplus( s(0), s(s(0)), s(s(s(0))) ), true ). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Arithmetic: Multiplication pred_def( aatimes/3, [ +int, +int, -int ], [ aatimes/3, aaplus/3 ], [] ). ex( aatimes( 0, s(0), 0 ), true ). ex( aatimes( s(s(s(0))), s(s(s(0))), s(s(s(s(s(s(s(s(s(0))))))))) ), true ). ex( aatimes( s(s(0)), s(s(s(0))), s(s(s(s(s(s(0)))))) ), true ). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % List Processing: Membership pred_def( mmember/2, [ +x, +xl ], [ mmember/2 ], [] ). ex( mmember( a, [ a ] ), true ). ex( mmember( b, [ a ] ), false ). ex( mmember( a, [ b, a ] ), true ). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % List Processing: Add element to end of list pred_def( cconc/3, [ +xl, +x, -xl ], [ cconc/3 ], [] ). ex( cconc( [], a, [ a ] ), true ). ex( cconc( [ a ], b, [ b, a ] ), false ). ex( cconc( [ a ], b, [ b ] ), false ). ex( cconc( [ a, b ], c, [ a, b, c ] ), true ). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % List Processing: List concatenation pred_def( aappend/3, [ +xl, +xl, -xl ], [ aappend/3 ], [] ). aappend( [], L, L ). aappend( [ X|L1 ], L2, [ X|L3 ] ) :- aappend( L1, L2, L3 ). init_clause((aappend( X, X, X ) :- true)). init_clause((aappend( [ X ], [ X ], [ X, X ] ) :- true)). init_clause((aappend( [], L, L ) :- true)). ex( aappend( [], [ a ], [ a ] ), true ). ex( aappend( [ a ], [ a ], [ a ] ), false ). ex( aappend( [ a, b ], [ c, d ], [ a, b, c, d ] ), true ). ex( aappend( [ b ], [ c, d ], [ b, c, d ] ), true ). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % List Processing: Reverse list pred_def( rreverse/2, [ +xl, -xl ], [ rreverse/2, cconc/3 ], [] ). sys_set( rreverse/2, clause_promising, exact_with_theory ). rreverse( [], [] ). rreverse( [ X|L1 ], L2 ) :- rreverse( L1, L3 ), cconc( L3, X, L2 ). ex( rreverse( [], [] ), true ). ex( rreverse( [ b, a ], [ b, a ] ), false ). ex( rreverse( [ a ], [] ), false ). ex( rreverse( [ a, b, c ], [ c, b, a ] ), true ). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % List Processing: Reverse list (using differnce lists) pred_def( rreverse_dl/3, [ +xl, +xl, -xl ], [ ccons/3, rreverse_dl/3 ], [] ). sys_set( rreverse_dl/3, clause_promising, exact_with_theory ). rreverse_dl( [], L, L ). rreverse_dl( [ X|L1 ], L2, L3 ) :- rreverse_dl( L1, [ X|L2 ], L3 ). ex( rreverse_dl( [], [], [] ), true ). ex( rreverse_dl( [ a, b ], [], [ a, b ] ), false ). ex( rreverse_dl( [ a ], [ b ], [ b ] ), false ). ex( rreverse_dl( [ a ], [ a ], [] ), false ). ex( rreverse_dl( [ a ], [ a ], [ a ] ), false ). ex( rreverse_dl( [ a, b, c ], [], [ c, b, a ] ), true ). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % List Processing: Insertion sort pred_def( iisort/2, [ +xl, -xl ], [ iisort/2, iinsert/3 ], [] ). sys_set( iisort/2, clause_promising, exact_with_theory ). iisort( [], [] ). iisort( [ X|L1 ], L3 ) :- iisort( L1, L2 ), iinsert( X, L2, L3 ). ex( iisort( [], [] ), true ). ex( iisort( [ b, a ], [ b, a ] ), false ). ex( iisort( [ a ], [] ), false ). ex( iisort( [ c, b, a ], [ a, b, c ] ), true ). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % List Processing: Insertion of element in orderd list pred_def( iinsert/3, [ +x, +xl, -xl ], [ ggtr/2, iinsert/3 ], [] ). sys_set( iinsert/3, clause_promising, exact_with_theory ). iinsert( X, [], [ X ] ). iinsert( X, [ Y|L1 ], [ X, Y|L1 ] ) :- \+ ggtr( X, Y ). iinsert( X, [ Y|L1 ], [ Y|L2 ] ) :- ggtr( X, Y ), iinsert( X, L1, L2 ). ex( iinsert( a, [], [ a ] ), true ). ex( iinsert( b, [ a ], [ b, a ] ), false ). ex( iinsert( b, [ a ], [ b ] ), false ). ex( iinsert( a, [ b ], [ a, b ] ), true ). ex( iinsert( c, [ a, b, d ], [ a, b, c, d ] ), true ). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % List Processing: Quick sort pred_def( qqsort/2, [ +xl, -xl ], [ ppartition/4, qqsort/2, ccons/3, aappend/3 ], [] ). /* qqsort( [], [] ). qqsort( [ X|L1 ], L6 ) :- ppartition( L1, X, L2, L3 ), qqsort( L2, L4 ), qqsort( L3, L5 ), aappend( L4, [ X|L5 ], L6 ). */ ex( qqsort( [], [] ), true ). ex( qqsort( [ b, a ], [ b, a ] ), false ). ex( qqsort( [ a ], [] ), false ). ex( qqsort( [ d, f, b, e, c, g, a ], [ a, b, c, d, e, f, g ] ), true ). ex( qqsort( [ b, c, a ], [ a, b, c ] ), true ). ex( qqsort( [ f, e, g ], [ e, f, g ] ), true ). ex( qqsort( [ a, c, b ], [ a, c, b ] ), false ). /* ex( qqsort( [], [] ), true ). ex( qqsort( [ b, a ], [ b, a ] ), false ). ex( qqsort( [ a ], [] ), false ). ex( qqsort( [ d, f, b, e, c, g, a ], [ a, b, c, d, e, f, g ] ), true ). ex( qqsort( [ b, c, a ], [ a, b, c ] ), true ). ex( qqsort( [ f, e, g ], [ e, f, g ] ), true ). ex( qqsort( [ a, c, b ], [ a, c, b ] ), false ). correct solution */ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % List Processing: Quick sort (using difference lists) pred_def( qqsort_dl/3, [ +xl, -xl, +xl ], [ ppartition/4, qqsort_dl/3, ccons/3 ], [] ). qqsort_dl( [], L, L ). qqsort_dl( [ X|L1 ], L4Hd, L4Tl ) :- ppartition( L1, X, L2, L3 ), qqsort_dl( L3, L4Tl1, L4Tl ), qqsort_dl( L2, L4Hd, [ X|L4Tl1 ] ). ex( qqsort_dl( [], [ a ], [ a ] ), true ). ex( qqsort_dl( [ a ], [ a ], [ a ] ), false ). ex( qqsort_dl( [ d, f, b, e, c, g, a ], [ a, b, c, d, e, f, g ], [] ), true ). ex( qqsort_dl( [ f, e, g ], [ e, f, g ], [] ), true ). ex( qqsort_dl( [ b, c, a ], [ a, b, c, d, e, f, g ], [ d, e, f, g ] ), true ). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % List Processing: list partition into two parts according to middle element pred_def( ppartition/4, [ +xl, +x, -xl, -xl ], [ ggtr/2, ppartition/4 ], [] ). sys_set( ppartition/4, clause_promising, exact_with_theory ). ppartition( [], _, [], [] ). ppartition( [ X|L1 ], Y, L2, [ X|L3 ] ) :- ggtr( X, Y ), ppartition( L1, Y, L2, L3 ). ppartition( [ X|L1 ], Y, [ X|L2 ], L3 ) :- \+ ggtr( X, Y ), ppartition( L1, Y, L2, L3 ). ex( ppartition( [], a, [], [] ), true ). ex( ppartition( [ a ], b, [], [ a ] ), false ). ex( ppartition( [ a ], b, [], [] ), false ). ex( ppartition( [ b ], a, [ b ], [] ), false ). ex( ppartition( [ a, b, c, d ], d, [ a, b, c, d ], [] ), true ). ex( ppartition( [ a, b, c, e ], d, [ a, b, c, e ], [] ), false ). ex( ppartition( [ a, d, c, b, e ], c, [ a, c, b ], [ d, e ] ), true ). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Tree Processing: Tree isomorphism pred_def( iisotree/2, [ +tree, +tree ], [ iisotree/2 ], [] ). iisotree( X, X ). iisotree( t( X1, X2 ), t( Y1, Y2 )) :- iisotree( X1, Y1 ), iisotree( X2, Y2 ). iisotree( t( X1, X2 ), t( Y1, Y2 )) :- iisotree( X1, Y2 ), iisotree( X2, Y1 ). ex( iisotree( t(1,1), t(1,1)), true ). ex( iisotree( t(1,1), t(2,1)), false ). ex( iisotree( t(t(1,2),t(3,4)), t(t(4,3),t(2,1)) ), true ). %ex( iisotree( t(t(t(1,0),0),t(1,0)), t(t(0,1),t(0,t(0,1))) ), true ). %ex( iisotree( t(t(1,0),0), t(0,t(0,1)) ), true ). %ex( iisotree( t(1,0), t(0,1) ), true ). %ex( iisotree( t(t(0,t(0,0)),0), t(0,t(t(0,0),0)) ), true ). %ex( iisotree( t(0,t(0,0)),0, 0,t(t(0,0),0)), true ). %ex( iisotree( t(0,t(0,0)),0, 0,t(t(0,0),0)), true ). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Formula Invention pred_def( fformula/5, [ +x, +x, +x, +x, -x ], [ aadd/3, ssub/3, mmul/3, ddiv/3 ], [] ). ex( fformula( 7, 9, 3, 19, 40 ), true ). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % utilities % list constructor pred_def( ccons/3, [ +x, +xl, -xl ], [], [ bad( ccons( X1, _, Y1 ), ccons( X1, Y1, _ )) ] ). ccons( X, Y, [ X|Y ] ). % greater pred_def( ggtr/2, [ +x, +x ], [], [ cond( ggtr( X1, Y1 ), X1 @> Y1 ), cond( \+ ggtr( X2, Y2 ), X2 @> Y2 ) ] ). ggtr( X, Y ) :- nonvar( X ), nonvar( Y ), X @> Y. % addition pred_def( aadd/3, [ +x, +x, -x ], [], [ cond( aadd( X1, Y1, _ ), X1 @> Y1 ) ] ). aadd( X, Y, Z ) :- Z is X + Y. % substraction pred_def( ssub/3, [ +x, +x, -x ], [], [] ). ssub( X, Y, Z ) :- Z is X - Y. % multiplication pred_def( mmul/3, [ +x, +x, -x ], [], [ cond( mmul( X1, Y1, _ ), X1 @> Y1 ) ] ). mmul( X, Y, Z ) :- Z is X * Y. % division pred_def( ddiv/3, [ +x, +x, -x ], [], [] ). ddiv( X, Y, Z ) :- Z is X / Y. % member pred_def( mem/2, [+x, +xl], [mem/2], []). % init_clause((mem(X,[Y|Z]) :- X=Y)). ex( mem(i,[j,k,i]),true). ex( mem(l,[m,l,m]),true). ex( mem(d,[d]),true). ex( mem(e,[f]),false). ex( mem(a,[b,b]), false). ex( mem(c,[c,c]), true). ex( mem(g,[h,g]),true). % cons pred_def( cons/3, [+xl, +x, +xl], [], []). init_clause((cons(L,H,T) :- L=[H|T])). cons(L,H,T) :- L=[H|T]. pred_def( ss/2, [+xl, +xl], [member/2, length/2], []). ex( ss([],[1,2,3]), true). ex( ss([1],[1,2,3]), true). ex( ss([2],[1,2,3]), true). ex( ss([3],[1,2,3]), true). ex( ss([1,1],[1,2,3]), true). ex( ss([1,2],[1,2,3]), true). ex( ss([],[1]), true). ex( ss([],[1]), true). ex( ss([],[1]), true). ex( ss([],[1]), true). ex( ss([],[1]), true). ex( ss([],[1]), true). ex( ss([],[1]), true). ex( ss([2,1],[1]), true). ex( ss([2],[1]), false). ex( ss([1,1,1,1],[1,2,3]), false). ex( ss([1,4],[1,2,3]),false). ex( ss([1,1,2,3],[1,2,3]), false). pred_def( member/2, [+x, +xl], [member/2], []). pred_def( length/2, [+xl, +x], [is/2, length/2], []). pred_def( is/2, [+x,+x], [], [] ). pred_def( mem_all/2, [+x, +xl], [mem_all/2],[]). ex(mem_all(1,[1]),true). ex(mem_all(2,[2]),true). ex(mem_all(3,[3]),true). ex(mem_all(1,[1,1]),true). ex(mem_all(1,[2,1]),true). ex(mem_all(1,[3,1]),true). ex(mem_all(2,[1,2]),true). ex(mem_all(2,[2,2]),true). ex(mem_all(2,[3,2]),true). ex(mem_all(3,[1,3]),true). ex(mem_all(3,[2,3]),true). ex(mem_all(3,[3,3]),true). ex(mem_all(1,[1,1,1]),true). ex(mem_all(1,[1,2,1]),true). ex(mem_all(1,[1,3,1]),true). ex(mem_all(1,[2,1,1]),true). ex(mem_all(1,[2,2,1]),true). ex(mem_all(1,[2,3,1]),true). ex(mem_all(1,[3,1,1]),true). ex(mem_all(1,[3,2,1]),true). ex(mem_all(1,[3,3,1]),true). ex(mem_all(2,[1,1,2]),true). ex(mem_all(2,[1,2,2]),true). ex(mem_all(2,[1,3,2]),true). ex(mem_all(2,[2,1,2]),true). ex(mem_all(2,[2,2,2]),true). ex(mem_all(2,[2,3,2]),true). ex(mem_all(2,[3,1,2]),true). ex(mem_all(2,[3,2,2]),true). ex(mem_all(2,[3,3,2]),true). ex(mem_all(3,[1,1,3]),true). ex(mem_all(3,[1,2,3]),true). ex(mem_all(3,[1,3,3]),true). ex(mem_all(3,[2,1,3]),true). ex(mem_all(3,[2,2,3]),true). ex(mem_all(3,[2,3,3]),true). ex(mem_all(3,[3,1,3]),true). ex(mem_all(3,[3,2,3]),true). ex(mem_all(3,[3,3,3]),true). ex(mem_all(1,[2]),false). ex(mem_all(1,[3]),false). ex(mem_all(1,[2,2]),false). ex(mem_all(1,[2,3]),false). ex(mem_all(1,[3,2]),false). ex(mem_all(1,[3,3]),false). ex(mem_all(1,[2,2,2]),false). ex(mem_all(1,[2,2,3]),false). ex(mem_all(1,[2,3,2]),false). ex(mem_all(1,[2,3,3]),false). ex(mem_all(1,[3,2,2]),false). ex(mem_all(1,[3,2,3]),false). ex(mem_all(1,[3,3,2]),false). ex(mem_all(1,[3,3,3]),false). ex(mem_all(2,[1]),false). ex(mem_all(2,[3]),false). ex(mem_all(2,[1,1]),false). ex(mem_all(2,[1,3]),false). ex(mem_all(2,[3,1]),false). ex(mem_all(2,[3,3]),false). ex(mem_all(2,[1,1,1]),false). ex(mem_all(2,[1,1,3]),false). ex(mem_all(2,[1,3,1]),false). ex(mem_all(2,[1,3,3]),false). ex(mem_all(2,[3,1,1]),false). ex(mem_all(2,[3,1,3]),false). ex(mem_all(2,[3,3,1]),false). ex(mem_all(2,[3,3,3]),false). ex(mem_all(3,[1]),false). ex(mem_all(3,[2]),false). ex(mem_all(3,[1,1]),false). ex(mem_all(3,[1,2]),false). ex(mem_all(3,[2,1]),false). ex(mem_all(3,[2,2]),false). ex(mem_all(3,[1,1,1]),false). ex(mem_all(3,[1,1,2]),false). ex(mem_all(3,[1,2,1]),false). ex(mem_all(3,[1,2,2]),false). ex(mem_all(3,[2,1,1]),false). ex(mem_all(3,[2,1,2]),false). ex(mem_all(3,[2,2,1]),false). ex(mem_all(3,[2,2,2]),false). end.