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

370 lines
8.0 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.']).
:- 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.