diff options
| author | Joshua Peek <josh@joshpeek.com> | 2012-08-20 10:48:36 -0500 |
|---|---|---|
| committer | Joshua Peek <josh@joshpeek.com> | 2012-08-20 10:48:36 -0500 |
| commit | d2de997fcc9e28358223d5ffeb5b4e70cc50372e (patch) | |
| tree | 54c45fc52f34235a18e441a9bdfc50faf973a7a7 /samples/Prolog/normal_form.pl | |
| parent | b8711f8ccf6945226b82997cc29a13f5dcbc60ea (diff) | |
Add more Prolog samples
Closes #233
Diffstat (limited to 'samples/Prolog/normal_form.pl')
| -rw-r--r-- | samples/Prolog/normal_form.pl | 94 |
1 files changed, 94 insertions, 0 deletions
diff --git a/samples/Prolog/normal_form.pl b/samples/Prolog/normal_form.pl new file mode 100644 index 0000000..808e522 --- /dev/null +++ b/samples/Prolog/normal_form.pl @@ -0,0 +1,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([]). |
