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