1
% This Prover9 input doesn't do anything meaningful. It simply contains
2
% some list-processing functions and relations, and it shows how they
7
formulas(demodulators).
9
% Relations and Properties
12
member(x,[y:z]) <-> if(x == y, $T, member(x,z)).
15
subset([x:y], z) <-> member(x,z) & subset(y,z).
18
is_set([x:y]) <-> -member(x,y) & is_set(y).
23
set([x:y]) = if(member(x,y), set(y), [x:set(y)]).
26
append([x:y], z) = [x:append(y,z)].
28
intersect([], x) = [].
29
intersect([x:y],z) = if(member(x,z),[x:intersect(y,z)],intersect(y,z)).
32
union([x:y], z) = if(member(x,z),union(y,z),[x:union(y,z)]).
35
diff([x:y], z) = if(member(x,z),diff(y,z),[x:diff(y,z)]).
37
reverse(x) = rev_app(x,[]).
39
rev_app([x:y],z) = rev_app(y,[x:z]).
41
quick_sort([]) = []. % naive quicksort
42
quick_sort([x:y]) = append(quick_sort(le_list(x,y)),
43
[x:quick_sort(gt_list(x,y))]).
46
le_list(z,[x:y]) = if(x @<= z,[x:le_list(z,y)], le_list(z,y)).
49
gt_list(z,[x:y]) = if(x @> z, [x:gt_list(z,y)], gt_list(z,y)).
53
formulas(assumptions).
55
% We're simply going to test some of the function and relations written
56
% above. The assumptions here will be rewritten by the rules above,
57
% and the results will appear in the output just after the line
58
% "Clauses after input processing:".
60
% Test functions, we can simply use a dummy predicate.
63
Test2(reverse(union([a,b,c],[d,b,f]))).
64
Test3(quick_sort([r,e,g,d,f,w,x,c,e,d,r,y,i,b,j,h,v,x,e,d,d,e,t])).
65
Test4(diff([a,b,c,d,e],[c,d,e,f,g])).
66
Test5(set([a,b,a,b,b,c])).
68
% Testing relations and properties is awkward, because if a literal
69
% rewrites to $T (true), the clause becomes a tautology and disappears;
70
% if a literal rewrites to $F (false), the literal disappears. We can
71
% use implications as follows.
73
member(b,[a,b,c]) -> Member_test_true.
74
-member(b,[a,b,c]) -> Member_test_false.
76
is_set([a,b,c,a,d]) -> Set_test_true.
77
-is_set([a,b,c,a,d]) -> Set_test_false.
added
removed
list.in
