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

371 lines
8.1 KiB
Plaintext
Raw Normal View History

:- 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.