1 %
2 % Another attempt.
3 %
4 % This time, I'm using the ax2 style of sticking to rdf(_,_,_)
5 % (which happens to keep the axioms in LX) and clausal form (or
6 % nearly so), to reduce un-thought-of consequences.
7 %
8 % I'm also starting with just negation and our truth predicate, so I
9 % can see if I've got that truth predicate right.
10 %
11
12 set(prolog_style_variables).
13 formula_list(usable).
14
15 % needed for tests 1 and 2:
16
17 all T S P O DenS DenP DenO (
18 rdf(T, rdf_type, lx_TrueSentence) &
19 rdf(T, lx_subjectTerm, S) &
20 rdf(T, lx_predicateTerm, P) &
21 rdf(T, lx_objectTerm, O) &
22 rdf(S, lx_denotation, DenS) &
23 rdf(P, lx_denotation, DenP) &
24 rdf(O, lx_denotation, DenO)
25 ->
26 rdf(DenS, DenP, DenO)
27 ).
28
29 % the <- form is also true, if you move the unconstrained terms
30 % inside, but we don't need that yet.
31
32
33 % needed for test 3:
34
35 all F N (
36 rdf(F, lx_negated, N) &
37 rdf(F, rdf_type, lx_TrueSentence)
38 ->
39 -rdf(N, rdf_type, lx_TrueSentence)
40 ).
41
42 all T S P O DenS DenP DenO (
43 -rdf(T, rdf_type, lx_TrueSentence) &
44 rdf(T, lx_subjectTerm, S) &
45 rdf(T, lx_predicateTerm, P) &
46 rdf(T, lx_objectTerm, O) &
47 rdf(S, lx_denotation, DenS) &
48 rdf(P, lx_denotation, DenP) &
49 rdf(O, lx_denotation, DenO)
50 ->
51 -rdf(DenS, DenP, DenO)
52 ).
53
54 % needed for 4:
55
56 all F N (
57 rdf(F, lx_negated, N)
58 ->
59 rdf(N, lx_negated, F)
60 ).
61
62 all F N (
63 rdf(F, lx_negated, N) &
64 -rdf(F, rdf_type, lx_TrueSentence)
65 ->
66 rdf(N, rdf_type, lx_TrueSentence)
67 ).
68
69 % others we might want:
70
71 % all reified relations between objects exist; they may or may
72 % not be true...
73
74 % Manually Skolemized Form (see ax4.lemma1.otter)
75
76 (all DenS DenP DenO (
77 rdf(triple(symFor(DenS), symFor(DenP), symFor(DenO)),
78 lx_subjectTerm, symFor(DenS)) &
79 rdf(triple(symFor(DenS), symFor(DenP), symFor(DenO)),
80 lx_predicateTerm, symFor(DenP)) &
81 rdf(triple(symFor(DenS), symFor(DenP), symFor(DenO)),
82 lx_objectTerm, symFor(DenO)) &
83 rdf(symFor(DenS), lx_denotation, DenS) &
84 rdf(symFor(DenP), lx_denotation, DenP) &
85 rdf(symFor(DenO), lx_denotation, DenO)
86 )).
87
88
89 % the negation of every reified triple exists (whether true or not)
90
91 % Manually Skolemized Form (see ax4.lemma2.otter)
92
93 (all T (
94 (exists S (
95 rdf(T, lx_subjectTerm, S)
96 ))
97 ->
98 rdf(T, lx_negated, negation(T))
99 )).
100
101 % even add falsehood....
102
103 all T S P O DenS DenP DenO (
104 rdf(T, rdf_type, lx_FalseSentence) &
105 rdf(T, lx_subjectTerm, S) &
106 rdf(T, lx_predicateTerm, P) &
107 rdf(T, lx_objectTerm, O) &
108 rdf(S, lx_denotation, DenS) &
109 rdf(P, lx_denotation, DenP) &
110 rdf(O, lx_denotation, DenO)
111 ->
112 -rdf(DenS, DenP, DenO)
113 ).
114
115 all T S (
116 rdf(T, lx_subjectTerm, S)
117 ->
118 (
119 rdf(T, rdf_type, lx_FalseSentence)
120 |
121 rdf(T, rdf_type, lx_TrueSentence)
122 )
123 ).
124
125 % A *description* of the sentence "this is false" is itself false,
126 % but even though the descriptions of all triple-sentence exist, the
127 % FOL sense of "all" there does not include self-referencing ones (see
128 % "occurs check").
1
2 set(auto).
3 clear(control_memory).
4 assign(max_mem, 768000).
5 set(prolog_style_variables).
6 formula_list(usable).
7
8
9 -(
10
11 % Manually Skolemized Form
12 (all DenS DenP DenO (
13 rdf(triple(symFor(DenS), symFor(DenP), symFor(DenO)), lx_subjectTerm, symFor(DenS)) &
14 rdf(triple(symFor(DenS), symFor(DenP), symFor(DenO)), lx_predicateTerm, symFor(DenP)) &
15 rdf(triple(symFor(DenS), symFor(DenP), symFor(DenO)), lx_objectTerm, symFor(DenO)) &
16 rdf(symFor(DenS), lx_denotation, DenS) &
17 rdf(symFor(DenP), lx_denotation, DenP) &
18 rdf(symFor(DenO), lx_denotation, DenO)
19 ))
20
21 ->
22
23 % Pretty form
24 (all DenS DenP DenO (
25 exists T S P O (
26 rdf(T, lx_subjectTerm, S) &
27 rdf(T, lx_predicateTerm, P) &
28 rdf(T, lx_objectTerm, O) &
29 rdf(S, lx_denotation, DenS) &
30 rdf(P, lx_denotation, DenP) &
31 rdf(O, lx_denotation, DenO)
32 )
33 ))
34
35
36 ).
1
2 set(auto).
3 clear(control_memory).
4 assign(max_mem, 768000).
5 set(prolog_style_variables).
6 formula_list(usable).
7
8
9 -(
10
11 % Manually Skolemized Form
12 (all T (
13 (exists S (
14 rdf(T, lx_subjectTerm, S)
15 ))
16 ->
17 rdf(T, lx_negated, negation(T))
18 ))
19
20 ->
21
22 % Pretty form
23 (all T (
24 (exists S (
25 rdf(T, lx_subjectTerm, S)
26 ))
27 ->
28 (exists N (
29 rdf(T, lx_negated, N)
30 ))
31 ))
32
33
34 ).
1
2
3 set(auto).
4 clear(control_memory).
5 assign(max_mem, 768000).
6 set(prolog_style_variables).
7
8 include('ax4.otter').
1 %
2 % Given
3 % l2 says rdf(a,b,c) is true.
4 % 1. are we satisfiable?
5 % 2. can we prove rdf(a,b,c)?
6 %
7
8 set(auto).
9 clear(control_memory).
10
11 include('ax4.otter').
12
13 formula_list(usable).
14
15 rdf(l2, rdf_type, lx_TrueSentence).
16 rdf(l2, lx_subjectTerm, l2s).
17 rdf(l2, lx_predicateTerm, l2p).
18 rdf(l2, lx_objectTerm, l2o).
19 rdf(l2s, lx_denotation, a).
20 rdf(l2p, lx_denotation, b).
21 rdf(l2o, lx_denotation, c).
22
23 % GOAL (be sure to terminate with SOS-empty when this is commented out)
24 -rdf(a,b,c).
1 %
2 % Given
3 % l1 says l2 is true.
4 % l2 says rdf(a,b,c) is true.
5 % 1. are we satisfiable?
6 % 2. can we prove rdf(a,b,c)?
7 %
8
9 set(auto).
10 clear(control_memory).
11
12 include('ax4.otter').
13
14 formula_list(usable).
15
16 rdf(l1, rdf_type, lx_TrueSentence).
17 rdf(l1, lx_subjectTerm, l1s).
18 rdf(l1, lx_predicateTerm, l1p).
19 rdf(l1, lx_objectTerm, l1o).
20 rdf(l1s, lx_denotation, l2).
21 rdf(l1p, lx_denotation, rdf_type).
22 rdf(l1o, lx_denotation, lx_TrueSentence).
23
24 % don't reify l2, just it's truth (above). if we did, we'd be saying
25 % l1 says (l2 is true and l2 says rdf(a,b,c) is true)
26
27 rdf(l2, lx_subjectTerm, l2s).
28 rdf(l2, lx_predicateTerm, l2p).
29 rdf(l2, lx_objectTerm, l2o).
30 rdf(l2s, lx_denotation, a).
31 rdf(l2p, lx_denotation, b).
32 rdf(l2o, lx_denotation, c).
33
34 % GOAL (be sure to terminate with SOS-empty when this is commented out)
35 -rdf(a,b,c).
1 %
2 % Given
3 % l1 says rdf(a,b,c) is false
4 % 1. are we satisfiable?
5 % 2. can we prove -rdf(a,b,c)?
6 %
7
8 set(auto).
9 clear(control_memory).
10
11 include('ax4.otter').
12
13 formula_list(usable).
14
15 rdf(l1, rdf_type, lx_TrueSentence).
16 rdf(l1, lx_negated, l2).
17
18 rdf(l2, lx_subjectTerm, l2s).
19 rdf(l2, lx_predicateTerm, l2p).
20 rdf(l2, lx_objectTerm, l2o).
21 rdf(l2s, lx_denotation, a).
22 rdf(l2p, lx_denotation, b).
23 rdf(l2o, lx_denotation, c).
24
25 % GOAL (be sure to terminate with SOS-empty when this is commented out)
26 %
27 rdf(a,b,c).
1 %
2 % Given
3 % l1 is the negation of l2
4 % l2 says l1 is true
5 % (neither is asserted)
6 % 1. are we satisfiable?
7 %
8 % if not, good, but then the axioms shouldn't be satisfiable either.
9 % -> some constructs, like this one, must be pre-created.
10 %
11
12 set(auto).
13 clear(control_memory).
14
15 include('ax4.otter').
16
17 formula_list(usable).
18
19 rdf(l1, lx_negated, l2).
20
21 rdf(l2, lx_subjectTerm, l2s).
22 rdf(l2, lx_predicateTerm, l2p).
23 rdf(l2, lx_objectTerm, l2o).
24 rdf(l2s, lx_denotation, l1).
25 rdf(l2p, lx_denotation, rdf_type).
26 rdf(l2o, lx_denotation, lx_TrueSentence).
27
28 % GOAL (be sure to terminate with SOS-empty when this is commented out)
29 %
30 % l1 being true -> l2 being false
31 % l2 being true -> l1 being false
32 %....
33
34 %what axioms are we missing for that?
Sandro Hawke
Generated Thu Aug 22 16:26:47 EDT 2002