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/SCRIPT
pmoura 9fe4d26c59 Logtalk 2.27.0 files.
git-svn-id: https://yap.svn.sf.net/svnroot/yap/trunk@1539 b08c6af1-5177-4d33-ba66-4b1c6b8b522a
2006-02-10 17:44:05 +00:00

99 lines
2.7 KiB
Plaintext

=================================================================
Logtalk - Object oriented extension to Prolog
Release 2.27.0
Copyright (c) 1998-2006 Paulo Moura. All Rights Reserved.
=================================================================
% start by loading the example:
| ?- logtalk_load(logic(loader)).
...
% translate a single logic proposition:
| ?- translator::translate((p v ~q) => (r & k), Cs).
r :- p.
k :- p.
q; r :- .
q; k :- .
Cs = [cl([r],[p]),cl([k],[p]),cl([q,r],[]),cl([q,k],[])]
yes
% translate a single logic proposition printing each translation step:
| ?- translator::step_by_step((p v ~q) => (r & k), Cs).
Processing proposition: p v ~q=>r&k
1. Remove implications: ~ (p v ~q) v r&k
2. Distribute negation: ~p&q v r&k
3. Remove existential quantifiers: ~p&q v r&k
4. Convert to prenex normal form: ~p&q v r&k
5. Remove universal quantifiers: ~p&q v r&k
6. Convert to conjunctive normal form: (~p v r)&(~p v k)&((q v r)&(q v k))
7. Convert to clauses: [cl([r],[p]),cl([k],[p]),cl([q,r],[]),cl([q,k],[])]
Clauses in Prolog-like notation:
r :- p.
k :- p.
q; r :- .
q; k :- .
Cs = [cl([r],[p]),cl([k],[p]),cl([q,r],[]),cl([q,k],[])]
yes
% translate a single logic proposition printing each translation step:
| ?- translator::step_by_step(all(X, exists(Y, p(X) v ~q(X) => r(X, Y))), Cs).
Processing proposition: all(X, exists(Y, p(X)v~q(X)=>r(X, Y)))
1. Remove implications: all(X, exists(Y, ~ (p(X)v~q(X))v r(X, Y)))
2. Distribute negation: all(X, exists(Y, ~p(X)&q(X)v r(X, Y)))
3. Remove existential quantifiers: all(X, ~p(X)&q(X)v r(X, f1(X)))
4. Convert to prenex normal form: all(X, ~p(X)&q(X)v r(X, f1(X)))
5. Remove universal quantifiers: ~p(X)&q(X)v r(X, f1(X))
6. Convert to conjunctive normal form: (~p(X)v r(X, f1(X)))& (q(X)v r(X, f1(X)))
7. Convert to clauses: [cl([r(X, f1(X))], [p(X)]), cl([q(X), r(X, f1(X))], [])]
Clauses in Prolog-like notation:
r(X, f1(X)) :- p(X).
q(X); r(X, f1(X)) :- .
X = X
Y = f1(X)
Cs = [cl([r(X, f1(X))], [p(X)]), cl([q(X), r(X, f1(X))], [])]
yes
% translate a single logic proposition printing each translation step:
| ?- translator::step_by_step(all(X, men(X) => mortal(X)), Cs).
Processing proposition: all(X, men(X)=>mortal(X))
1. Remove implications: all(X, ~men(X)v mortal(X))
2. Distribute negation: all(X, ~men(X)v mortal(X))
3. Remove existential quantifiers: all(X, ~men(X)v mortal(X))
4. Convert to prenex normal form: all(X, ~men(X)v mortal(X))
5. Remove universal quantifiers: ~men(X)v mortal(X)
6. Convert to conjunctive normal form: ~men(X)v mortal(X)
7. Convert to clauses: [cl([mortal(X)], [men(X)])]
Clauses in Prolog-like notation:
mortal(X) :- men(X).
X = X
Cs = [cl([mortal(X)], [men(X)])]
yes