1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
|
%%----- normalize(+Wff,-NormalClauses) ------
normalize(Wff,NormalClauses) :-
conVert(Wff,[],S),
cnF(S,T),
flatten_and(T,U),
make_clauses(U,NormalClauses).
%%----- make a sequence out of a conjunction -----
flatten_and(X /\ Y, F) :-
!,
flatten_and(X,A),
flatten_and(Y, B),
sequence_append(A,B,F).
flatten_and(X,X).
%%----- make a sequence out of a disjunction -----
flatten_or(X \/ Y, F) :-
!,
flatten_or(X,A),
flatten_or(Y,B),
sequence_append(A,B,F).
flatten_or(X,X).
%%----- append two sequences -------------------------------
sequence_append((X,R),S,(X,T)) :- !, sequence_append(R,S,T).
sequence_append((X),S,(X,S)).
%%----- separate into positive and negative literals -----------
separate((A,B),P,N) :-
!,
(A = ~X -> N=[X|N1],
separate(B,P,N1)
;
P=[A|P1],
separate(B,P1,N) ).
separate(A,P,N) :-
(A = ~X -> N=[X],
P = []
;
P=[A],
N = [] ).
%%----- tautology ----------------------------
tautology(P,N) :- some_occurs(N,P).
some_occurs([F|R],B) :-
occurs(F,B) | some_occurs(R,B).
occurs(A,[F|_]) :-
A == F,
!.
occurs(A,[_|R]) :-
occurs(A,R).
make_clauses((A,B),C) :-
!,
flatten_or(A,F),
separate(F,P,N),
(tautology(P,N) ->
make_clauses(B,C)
;
make_clause(P,N,D),
C = [D|R],
make_clauses(B,R) ).
make_clauses(A,C) :-
flatten_or(A,F),
separate(F,P,N),
(tautology(P,N) ->
C = []
;
make_clause(P,N,D),
C = [D] ).
make_clause([],N, false :- B) :-
!,
make_sequence(N,B,',').
make_clause(P,[],H) :-
!,
make_sequence(P,H,'|').
make_clause(P,N, H :- T) :-
make_sequence(P,H,'|'),
make_sequence(N,T,',').
make_sequence([A],A,_) :- !.
make_sequence([F|R],(F|S),'|') :-
make_sequence(R,S,'|').
make_sequence([F|R],(F,S),',') :-
make_sequence(R,S,',').
write_list([F|R]) :-
write(F), write('.'), nl,
write_list(R).
write_list([]).
|
