1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
|
=================================================================
Logtalk - Object oriented extension to Prolog
Release 2.27.1
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
|
