This repository has been archived on 2023-08-20. You can view files and clone it, but cannot push or open issues or pull requests.
yap-6.3/Logtalk/examples/logic/translator.lgt
pmoura 9f1b358c04 Logtalk 2.26.2 files.
git-svn-id: https://yap.svn.sf.net/svnroot/yap/trunk@1486 b08c6af1-5177-4d33-ba66-4b1c6b8b522a
2005-12-24 18:00:21 +00:00

371 lines
8.1 KiB
Plaintext

:- object(translator).
:- info([
version is 1.0,
date is 2004/6/8,
author is 'Paulo Moura',
comment is 'Translator of logic propostions to clauses in conjunctive normal form.',
source is 'Code partially based on an example found on the Clocksin and Mellish Prolog book.']).
:- public(translate/2).
:- mode(translate(+nonvar, -list), zero_or_one).
:- info(translate/2, [
comment is 'Translates a proposition to a list of clauses.',
argnames is ['Propostion', 'Clauses']]).
:- public(step_by_step/2).
:- mode(step_by_step(+nonvar, -list), zero_or_one).
:- info(step_by_step/2, [
comment is 'Translates a proposition to a list of clauses, printing the result of each translation step.',
argnames is ['Propostion', 'Clauses']]).
:- dynamic(gensym_counter_/1).
:- op(10, fy, ~ ). % negation
:- op(20, yfx, & ). % conjunction
:- op(30, yfx, v ). % disjunction
:- op(40, xfx, =>). % implication
:- op(40, xfx, <=>). % equivalence
translate(P, Cs) :-
remove_implications(P, P2),
distribute_negation(P2, P3),
remove_existential_quantifiers(P3, P4),
convert_to_prenex_normal_form(P4, P5),
remove_universal_quantifiers(P5, P6),
convert_to_conjunctive_normal_form(P6, P7),
convert_to_clauses(P7, Cs),
print_clauses(Cs).
step_by_step(P, Cs) :-
nl, write('Processing proposition: '), write(P), nl, nl,
write(' 1. Remove implications: '),
remove_implications(P, P2),
write(P2), nl,
write(' 2. Distribute negation: '),
distribute_negation(P2, P3),
write(P3), nl,
write(' 3. Remove existential quantifiers: '),
remove_existential_quantifiers(P3, P4),
write(P4), nl,
write(' 4. Convert to prenex normal form: '),
convert_to_prenex_normal_form(P4, P5),
write(P5), nl,
write(' 5. Remove universal quantifiers: '),
remove_universal_quantifiers(P5, P6),
write(P6), nl,
write(' 6. Convert to conjunctive normal form: '),
convert_to_conjunctive_normal_form(P6, P7),
write(P7), nl,
write(' 7. Convert to clauses: '),
convert_to_clauses(P7, Cs),
write(Cs), nl, nl,
write('Clauses in Prolog-like notation:'), nl,
print_clauses(Cs).
remove_implications(all(X, P), all(X, P2)) :-
!,
remove_implications(P, P2).
remove_implications(exists(X, P), exists(X, P2)) :-
!,
remove_implications(P, P2).
remove_implications(P <=> Q, P2 & Q2 v ~P2 & ~Q2) :-
!,
remove_implications(P, P2),
remove_implications(Q, Q2).
remove_implications(P => Q, ~P2 v Q2) :-
!,
remove_implications(P, P2),
remove_implications(Q, Q2).
remove_implications(P & Q, P2 & Q2) :-
!,
remove_implications(P, P2),
remove_implications(Q, Q2).
remove_implications(P v Q, P2 v Q2) :-
!,
remove_implications(P, P2),
remove_implications(Q, Q2).
remove_implications(~P, ~P2) :-
!,
remove_implications(P, P2).
remove_implications(P, P).
distribute_negation(all(X, P), all(X, P2)) :-
!,
distribute_negation(P, P2).
distribute_negation(exists(X, P), exists(X, P2)) :-
!,
distribute_negation(P, P2).
distribute_negation(P & Q, P2 & Q2) :-
!,
distribute_negation(P, P2),
distribute_negation(Q, Q2).
distribute_negation(P v Q, P2 v Q2) :-
!,
distribute_negation(P, P2),
distribute_negation(Q, Q2).
distribute_negation(~P, P2) :-
!,
apply_negation(P, P2).
distribute_negation(P, P).
apply_negation(all(X, P), exists(X, P2)) :-
!,
apply_negation(P, P2).
apply_negation(exists(X, P), all(X, P2)) :-
!,
apply_negation(P, P2).
apply_negation(P & Q, P2 v Q2) :-
!,
apply_negation(P, P2),
apply_negation(Q, Q2).
apply_negation(P v Q, P2 & Q2) :-
!,
apply_negation(P, P2),
apply_negation(Q, Q2).
apply_negation(~P, P2) :-
!,
distribute_negation(P, P2).
apply_negation(P, ~P).
remove_existential_quantifiers(P, P2) :-
remove_existential_quantifiers(P, P2, []).
remove_existential_quantifiers(all(X, P), all(X, P2), Vars) :-
!,
remove_existential_quantifiers(P, P2, [X| Vars]).
remove_existential_quantifiers(exists(X, P), P2, Vars) :-
!,
gensym(f, F),
X =.. [F| Vars],
remove_existential_quantifiers(P, P2, Vars).
remove_existential_quantifiers(P & Q, P2 & Q2, Vars) :-
!,
remove_existential_quantifiers(P, P2, Vars),
remove_existential_quantifiers(Q, Q2, Vars).
remove_existential_quantifiers(P v Q, P2 v Q2, Vars) :-
!,
remove_existential_quantifiers(P, P2, Vars),
remove_existential_quantifiers(Q, Q2, Vars).
remove_existential_quantifiers(P, P, _).
convert_to_prenex_normal_form(P, P2) :-
collect_vars(P, P1, [], Vars),
add_vars_at_front(Vars, P1, P2).
collect_vars(all(X, P), P2, Acc, Vars) :-
!,
collect_vars(P, P2, [X| Acc], Vars).
collect_vars(P & Q, P2 & Q2, Acc, Vars) :-
!,
collect_vars(P, P2, Acc, Acc2),
collect_vars(Q, Q2, Acc2, Vars).
collect_vars(P v Q, P2 v Q2, Acc, Vars) :-
!,
collect_vars(P, P2, Acc, Acc2),
collect_vars(Q, Q2, Acc2, Vars).
collect_vars(P, P, Vars, Vars).
add_vars_at_front([], P, P).
add_vars_at_front([X| Vars], P, P2) :-
add_vars_at_front(Vars, all(X, P), P2).
remove_universal_quantifiers(all(_, P), P2) :-
!,
remove_universal_quantifiers(P, P2).
remove_universal_quantifiers(P & Q, P2 & Q2) :-
!,
remove_universal_quantifiers(P, P2),
remove_universal_quantifiers(Q, Q2).
remove_universal_quantifiers(P v Q, P2 v Q2) :-
!,
remove_universal_quantifiers(P, P2),
remove_universal_quantifiers(Q, Q2).
remove_universal_quantifiers(P, P).
convert_to_conjunctive_normal_form(P v Q, R) :-
!,
convert_to_conjunctive_normal_form(P, P2),
convert_to_conjunctive_normal_form(Q, Q2),
distribute_disjunction(P2 v Q2, R).
convert_to_conjunctive_normal_form(P & Q, P2 & Q2) :-
!,
convert_to_conjunctive_normal_form(P, P2),
convert_to_conjunctive_normal_form(Q, Q2).
convert_to_conjunctive_normal_form(P, P).
distribute_disjunction(P & Q v R, P2 & Q2) :-
!,
convert_to_conjunctive_normal_form(P v R, P2),
convert_to_conjunctive_normal_form(Q v R, Q2).
distribute_disjunction(P v Q & R, P2 & Q2) :-
!,
convert_to_conjunctive_normal_form(P v Q, P2),
convert_to_conjunctive_normal_form(P v R, Q2).
distribute_disjunction(P, P).
convert_to_clauses(P, Cs) :-
convert_to_clauses(P, [], Cs).
convert_to_clauses(P & Q, Acc, Cs) :-
!,
convert_to_clauses(Q, Acc, Acc2),
convert_to_clauses(P, Acc2, Cs).
convert_to_clauses(P, Acc, [cl(Pos, Negs)| Acc]) :-
convert_to_clauses(P, [], Pos, [], Negs),
!.
convert_to_clauses(_, Cs, Cs).
convert_to_clauses(P v Q, AccPos, Pos, AccNegs, Negs) :-
!,
convert_to_clauses(Q, AccPos, AccPos2, AccNegs, AccNegs2),
convert_to_clauses(P, AccPos2, Pos, AccNegs2, Negs).
convert_to_clauses(~P, Pos, Pos, AccNegs, [P| AccNegs]) :-
!,
not_member_of(P, Pos).
convert_to_clauses(P, AccPos, [P| AccPos], Negs, Negs) :-
!,
not_member_of(P, Negs).
/*
convert_to_clauses(P & Q, {P2, Q2}) :-
!,
convert_to_clauses(P, P2),
convert_to_clauses(Q, Q2).
convert_to_clauses(P v Q, R) :-
!,
convert_to_clause(P v Q, R).
convert_to_clauses(P, {P}).
convert_to_clause(P & Q, R) :-
!,
convert_to_clauses(P & Q, {R}).
convert_to_clause(P v Q, {P2, Q}) :-
!,
convert_to_clause(P, P2).
convert_to_clause(P, P).
*/
not_member_of(P, [P| _]) :-
!,
fail.
not_member_of(P, [_| Ps]) :-
!,
not_member_of(P, Ps).
not_member_of(_, []).
print_clauses([]) :-
nl.
print_clauses([cl(Pos, Negs)| Cs]) :-
print_clause(Pos, Negs), nl,
print_clauses(Cs).
print_clause(Pos, []) :-
!,
print_disjunctions(Pos), write(' :- .').
print_clause([], Negs) :-
!,
write(':- '), print_conjunctions(Negs), write('.').
print_clause(Pos, Negs) :-
!,
print_disjunctions(Pos), write(' :- '),
print_conjunctions(Negs), write('.').
print_disjunctions([P]) :-
!,
write(P).
print_disjunctions([P| Ps]) :-
!,
write(P), write('; '),
print_disjunctions(Ps).
print_conjunctions([P]) :-
!,
write(P).
print_conjunctions([P| Ps]) :-
!,
write(P), write(', '),
print_conjunctions(Ps).
gensym_counter_(0).
gensym(Base, Atom) :-
retract(gensym_counter_(Counter)),
Counter2 is Counter + 1,
number_codes(Counter2, Codes2),
atom_codes(Number, Codes2),
atom_concat(Base, Number, Atom),
assertz(gensym_counter_(Counter2)).
:- end_object.