This is an automatically-generated collection of the layering axioms. For more information, see the Layering LX on RDF
Note that the prefix "pt" is still used here instead of "lx". This should change soon.
The axioms are divided into several files according the their general purpose:
An observation: there are tradeoffs between human-readability, machine-readability-for-proving-satisfiability, and machine-readability-for-generating-proofs. The approach taken in ax4 might be better on all counts.
1 list(usable).
2 rdf(pt_Conjunction,rx_superclass,pt_Formula).
3 rdf(pt_Constant,daml_disjointWith,pt_Variable).
4 rdf(pt_Constant,rx_superclass,pt_Term).
5 rdf(pt_Formula,rx_superclass,rdfs_Class).
6 rdf(pt_Quantification,rx_superclass,pt_Formula).
7 rdf(pt_Sentence,rx_superclass,pt_Formula).
8 rdf(pt_SubformulaProperty,rx_superclass,rdfs_Property).
9 rdf(pt_Term,daml_disjointWith,pt_Formula).
10 rdf(pt_Term,rx_superclass,rdfs_Class).
11 rdf(pt_Triple,rx_superclass,pt_Formula).
12 rdf(pt_TrueSentence,rx_superclass,pt_Sentence).
13 rdf(pt_Variable,rx_superclass,pt_Term).
14 rdf(pt_conjLeft,rdfs_domain,pt_Conjunction).
15 rdf(pt_conjLeft,rdfs_range,pt_Formula).
16 rdf(pt_conjLeft,rx_superclass,pt_subformulaProperty).
17 rdf(pt_conjRight,rdfs_domain,pt_Conjunction).
18 rdf(pt_conjRight,rdfs_range,pt_Formula).
19 rdf(pt_conjRight,rx_superclass,pt_subformulaProperty).
20 rdf(pt_denotation,rdfs_domain,pt_Constant).
21 rdf(pt_denotation,rdfs_range,rdfs_Resource).
22 rdf(pt_objectTerm,rdfs_domain,pt_Triple).
23 rdf(pt_objectTerm,rdfs_range,pt_Term).
24 rdf(pt_predicateTerm,rdfs_domain,pt_Triple).
25 rdf(pt_predicateTerm,rdfs_range,pt_Term).
26 rdf(pt_subformula,rdfs_domain,pt_Quantification).
27 rdf(pt_subformula,rdfs_range,pt_Formula).
28 rdf(pt_subformula,rx_superclass,pt_subformulaProperty).
29 rdf(pt_subjectTerm,rdfs_domain,pt_Triple).
30 rdf(pt_subjectTerm,rdfs_range,pt_Term).
31 rdf(pt_uname,rdf_type,daml_UnambiguousProperty).
32 rdf(pt_uname,rdfs_domain,rdfs_Resource).
33 rdf(pt_uname,rdfs_range,rdfs_Literal).
34 rdf(pt_variable,rdfs_domain,pt_Quantification).
35 rdf(pt_variable,rdfs_range,pt_Variable).
36 end_of_list.
1 %
2 % DAML+OIL Semantics (as much as I need, at least)
3 %
4 % See http://www.w3.org/2002/05/positive-triples
5 %
6 % $Id: ax3.20020822T1630.html,v 1.1 2002/08/22 20:33:01 sandro Exp $
7 %
8
9 formula_list(usable).
10
11 all O C1 C2 (
12 rdf(C1, daml_disjointWith, C2) &
13 rdf(O, rdf_type, C1) &
14 rdf(O, rdf_type, C2)
15 ->
16
17
18 malformed(foo(O,C1,C2), objectInDisjointClasses)
19 ).
20
21 all O (
22 rdf(O, daml_differentIndividualFrom, O)
23 ->
24 malformed(O, objectsAreDifferentAndYetTheSame)
25 ).
26
27 all A P1 P2 C (
28 rdf(A, P1, C) &
29 rdf(P1, daml_inversePropertyOf, P2)
30 ->
31 rdf(C, P2, A)
32 ).
33
34 % slows things down?
35 %all X Y A B (
36 % rdf(X, daml_equivalentTo, Y) &
37 % rdf(X, A, B)
38 % ->
39 % rdf(Y, A, B)
40 %).
41 %all X Y A B (
42 % rdf(X, daml_equivalentTo, Y) &
43 % rdf(A, X, B)
44 % ->
45 % rdf(A, Y, B)
46 %).
47 %all X Y A B (
48 % rdf(X, daml_equivalentTo, Y) &
49 % rdf(A, B, X)
50 % ->
51 % rdf(A, B, Y)
52 %).
53
54
1 %
2 % RX Semantics (as much as I need, at least)
3 %
4 % See http://www.w3.org/2002/05/positive-triples
5 %
6 % $Id: ax3.20020822T1630.html,v 1.1 2002/08/22 20:33:01 sandro Exp $
7 %
8
9 formula_list(usable).
10
11 % we can just say
12 % rdf(rx_superclass, daml_equivalentTo, rdfs_subClassOf).
13 % and define daml_equivalentTo axioms, but that's way slow.
14
15 all O Sub Super (
16 rdf(O, rdf_type, Sub) &
17 rdf(Sub, rx_superclass, Super)
18 ->
19 rdf(O, rdf_type, Super)
20 ).
21
22
1 %
2 % RDFS Semantics (as much as I need, at least)
3 %
4 % See http://www.w3.org/2002/05/positive-triples
5 %
6 % $Id: ax3.20020822T1630.html,v 1.1 2002/08/22 20:33:01 sandro Exp $
7 %
8
9 formula_list(usable).
10
11 all S P O C (
12 rdf(P, rdfs_domain, C) &
13 rdf(S, P, O)
14 ->
15 rdf(S, rdf_type, C)
16 ).
17
18 all S P O C (
19 rdf(P, rdfs_range, C) &
20 rdf(S, P, O)
21 ->
22 rdf(O, rdf_type, C)
23 ).
24
25 all O Sub Super (
26 rdf(O, rdf_type, Sub) &
27 rdf(Sub, rdfs_subClassOf, Super)
28 ->
29 rdf(O, rdf_type, Super)
30 ).
31
32
1 include('pt-schema.otter').
2 include('daml.otter').
3 include('rx.otter').
4 include('rdfs.otter').
5
6 formula_list(usable). % signal start of formulas
7
8
9
10 % these might be called "comprehension" axioms
11
12 % Every object can be denoted with a symbol
13 all X (
14 denotation(symbolFor(X), X)
15 ).
16
17 % Every symbol which denotes an object is a constant
18 all S D (
19 denotation(S,D)
20 ->
21 isConstant(S)
22 ).
23
24 % Every constant has a denotation
25 all S (
26 isConstant(S)
27 ->
28 denotation(S, denotationOf(S))
29 ).
30
31 % Every quantified formula has a possible constant replacement
32 % for the variable
33 all Var Child (
34 isConstant(ConstFor(Child, Var))
35 ).
36
37
38 all Error Message (
39 -malformed(Error, Message)
40 ).
1 formula_list(usable). % signal start of formulas
2
3 %%
4 %% Turn rdf(a,b,c) facts info into more convenient forms
5 %%
6
7 %% Some day we may want to turn these into biconditionals, which
8 %% might let us draw out the triples-encoding of a formula, although
9 %% it would naturally include all our axioms....
10
11 all T F A B C L R N D V X S
12 ((
13 rdf(T, pt_subjectTerm, A) &
14 rdf(T, pt_predicateTerm, B) &
15 rdf(T, pt_objectTerm, C)
16 <->
17 triple(T,A,B,C)
18 ) & (
19 rdf(F, pt_conjLeft, L) &
20 rdf(F, pt_conjRight, R)
21 ->
22 conjunction(F,L,R)
23 ) & (
24 rdf(F, pt_disjLeft, L) &
25 rdf(F, pt_disjRight, R)
26 ->
27 disjunction(F,L,R)
28 ) & (
29 rdf(F, pt_condLeft, L) &
30 rdf(F, pt_condRight, R)
31 ->
32 conditional(F,L,R)
33 ) & (
34 rdf(F, pt_bicondLeft, L) &
35 rdf(F, pt_bicondRight, R)
36 ->
37 biconditional(F,L,R)
38 ) & (
39 rdf(F, pt_negated, N)
40 ->
41 negation(F,N)
42 ) & (
43 rdf(F, pt_var, V) &
44 rdf(F, pt_subformula, S)
45 ->
46 quantification(F, V, S)
47 ) & (
48 rdf(T, pt_denotation, D)
49 ->
50 denotation(T, D)
51 ) & (
52 rdf(T, pt_denotation, X)
53 ->
54 isConstant(T)
55 ) & (
56 rdf(T, rdf_type, pt_UniVar)
57 ->
58 isUniVar(T)
59 ) & (
60 rdf(T, rdf_type, pt_ExiVar)
61 ->
62 isExiVar(T)
63 ) & (
64 (isUniVar(T) | isExiVar(T))
65 ->
66 isVar(T)
67 ) & (
68 rdf(F, rdf_type, pt_TrueSentence)
69 ->
70 trueSentence(F)
71 )).
72
1 formula_list(usable). % signal start of formulas
2
3
4 % Basic feedback from truth predicate
5 all T A B C DenA DenB DenC (
6 triple(T, A, B, C) &
7 denotation(A, DenA) &
8 denotation(B, DenB) &
9 denotation(C, DenC)
10 ->
11 ( trueSentence(T) <-> rdf(DenA, DenB, DenC) )
12 ).
13
14 % Each contruct implies the obvious thing
15 all F L R (
16 conjunction(F, L, R) ->
17 ( trueSentence(F) <-> ( trueSentence(L) & trueSentence(R) ) )
18 ).
19 all F L R (
20 disjunction(F, L, R) ->
21 ( trueSentence(F) <-> ( trueSentence(L) | trueSentence(R) ) )
22 ).
23 all F L R (
24 conditional(F, L, R) ->
25 ( trueSentence(F) <-> ( trueSentence(L) -> trueSentence(R) ) )
26 ).
27 all F L R (
28 biconditional(F, L, R) ->
29 ( trueSentence(F) <-> ( trueSentence(L) <-> trueSentence(R) ) )
30 ).
31 all F N (
32 negation(F, N) ->
33 ( trueSentence(F) <-> ( -trueSentence(N) ) )
34 ).
35
36 % somewhat more complicated: quantification
37
38 all Formula Var Const OldChild NewChild (
39 quantification(Formula, Var, OldChild) &
40 isUniVar(Var) &
41 isConstant(Const) &
42 subst(OldChild, NewChild, Var, Const) &
43 ground(NewChild) &
44 trueSentence(Formula)
45 ->
46 trueSentence(NewChild)
47 ).
48
49 % maybe doesn't work, maybe not needed...
50 %all Formula Var OldChild NewChild (
51 % quantification(Formula, Var, OldChild) &
52 % isUniVar(Var) &
53 % (all Object (
54 % trueSentence(NewChild) &
55 % denotation(Const, Object) &
56 % subst(OldChild, NewChild, Var, Const) &
57 % ground(NewChild)
58 % ))
59 % ->
60 % trueSentence(Formula)
61 %).
62
63 % suspend....
64 %all Formula Var OldChild NewChild (
65 % quantification(Formula, Var, OldChild) &
66 % isExiVar(Var) &
67 % isConstant(ConstFor(OldChild, Var)) &
68 % subst(OldChild, NewChild, Var, ConstFor(OldChild, Var)) &
69 % ground(NewChild)
70 % ->
71 % ( trueSentence(Formula) <-> trueSentence(NewChild) )
72 %).
73
74 % WORKS, BUT I'D RATHER SKOLEMIZE MYSELF
75 %all F V S RS (
76 % quantification(F, V, S) &
77 % isExiVar(V)
78 % ->
79 % (exists RV (
80 % isConstant(RV) &
81 % subst(S, RS, V, RV) &
82 % ground(RS) &
83 % ( trueSentence(F) <-> trueSentence(RS) )
84 % ))
85 %).
86
87
88 % DOESN'T WORK:
89 %all Formula Var OldChild NewChild (
90 % quantification(Formula, Var, OldChild) &
91 % isExiVar(Var) &
92 % isConstant(ConstFor(OldChild, Var)) &
93 % subst(OldChild, NewChild, Var, ConstFor(OldChild, Var)) &
94 % ground(NewChild)
95 % ->
96 % ( trueSentence(Formula) <-> trueSentence(NewChild) )
97 %).
98
99 % WORKS. (the subst and ground have to be in the consequent. why?)
100 all Formula Var OldChild NewChild (
101 quantification(Formula, Var, OldChild) &
102 isExiVar(Var) &
103 isConstant(ConstFor(OldChild, Var))
104 ->
105 (
106 subst(OldChild, NewChild, Var, ConstFor(OldChild, Var)) &
107 ground(NewChild) &
108 ( trueSentence(Formula) <-> trueSentence(NewChild) )
109 )
110 ).
1 formula_list(usable).
2 %%%
3 %%% Define Substitution
4 %%%
5 %%% subst(OriginalFormula, ReplacementFormula,
6 %%% OriginalTerm, ReplacementTerm)
7 %%%
8 %%% is true if zero or more occurances of OriginalTerm
9 %%% in OriginalFormula has been replaced
10 %%% by ReplacementTerm in ReplacementFormula
11 %%%
12 %%% substTerm has the same parameters except the
13 %%% formulas are the terms (occuring in the formulas).
14 %%%
15
16 % The degenerate "no replacement done" versions of substTerm and subst
17 all SomeTerm OldTerm NewTerm ( substTerm(SomeTerm, SomeTerm,
18 OldTerm, NewTerm) ).
19
20 all SomeFormula OldTerm NewTerm ( subst(SomeFormula, SomeFormula,
21 OldTerm, NewTerm) ).
22
23 % The replacement version of substTerm is simple:
24 all OldTerm NewTerm ( substTerm(OldTerm, NewTerm,
25 OldTerm, NewTerm) ).
26
27
28 %% Substitution In Triples
29 all Formula OldTerm NewTerm
30 A B C
31 RA RB RC (
32 isConstant(NewTerm) &
33 triple(Formula, A, B, C) &
34 substTerm(A, RA, OldTerm, NewTerm) &
35 substTerm(B, RB, OldTerm, NewTerm) &
36 substTerm(C, RC, OldTerm, NewTerm)
37 ->
38 % this is perhaps clearer, but it has a much higher-arity skolemization
39 % ( exists RFormula (
40 % triple(RFormula, RA, RB, RC) &
41 % subst(Formula, RF, OldTerm, NewTerm)
42 % ))
43 triple(tripleOf(RA, RB, RC), RA, RB, RC) &
44 subst(Formula, tripleOf(RA, RB, RC), OldTerm, NewTerm)
45 ).
46
47
48 %% Substitution In Conjunction
49 all Formula OldTerm NewTerm L NewLeft R NewRight (
50 conjunction(Formula, L, R) &
51 subst(L, NewLeft, OldTerm, NewTerm) &
52 subst(R, NewRight, OldTerm, NewTerm)
53 ->
54 conjunction(conjunctionOf(NewLeft, NewRight), NewLeft, NewRight) &
55 subst(Formula, conjunctionOf(NewLeft, NewRight), OldTerm, NewTerm)
56 ).
57
58 %% Substitution In Disjunction
59 all Formula OldTerm NewTerm L NewLeft R NewRight (
60 disjunction(Formula, L, R) &
61 subst(L, NewLeft, OldTerm, NewTerm) &
62 subst(R, NewRight, OldTerm, NewTerm)
63 ->
64 disjunction(disjunctionOf(NewLeft, NewRight), NewLeft, NewRight) &
65 subst(Formula, disjunctionOf(NewLeft, NewRight), OldTerm, NewTerm)
66 ).
67
68 %% Substitution In Conditional
69 all Formula OldTerm NewTerm L NewLeft R NewRight (
70 conditional(Formula, L, R) &
71 subst(L, NewLeft, OldTerm, NewTerm) &
72 subst(R, NewRight, OldTerm, NewTerm)
73 ->
74 conditional(conditionalOf(NewLeft, NewRight), NewLeft, NewRight) &
75 subst(Formula, conditionalOf(NewLeft, NewRight), OldTerm, NewTerm)
76 ).
77
78 %% Substitution In Biconditional
79 all Formula OldTerm NewTerm L NewLeft R NewRight (
80 biconditional(Formula, L, R) &
81 subst(L, NewLeft, OldTerm, NewTerm) &
82 subst(R, NewRight, OldTerm, NewTerm)
83 ->
84 biconditional(biconditionalOf(NewLeft, NewRight), NewLeft, NewRight) &
85 subst(Formula, biconditionalOf(NewLeft, NewRight), OldTerm, NewTerm)
86 ).
87
88 %% Substitution In Negation
89 all Formula OldTerm NewTerm OldChild NewChild (
90 negation(Formula, OldChild) &
91 subst(OldChild, NewChild, OldTerm, NewTerm)
92 ->
93 negation(negationOf(NewChild), NewChild) &
94 subst(Formula, negationOf(NewChild), OldTerm, NewTerm)
95 ).
96
97 %% Substitution In Quantification
98 all Formula OldTerm NewTerm Var OldChild NewChild (
99 quantification(Formula, Var, OldChild) &
100 subst(OldChild, NewChild, OldTerm, NewTerm)
101 ->
102 quantification(quantificationOf(Var,NewChild), Var, NewChild) &
103 subst(Formula, quantificationOf(Var,NewChild), OldTerm, NewTerm)
104 ).
105
1 formula_list(usable).
2 %
3 % Ground Formulas
4 %
5 % For the quantification axioms, we need to know when the Child
6 % formula has no more variables in it; we call that being a "ground"
7 % formula. Here are the ground formulas:
8
9 all T A B C AD BD CD (
10 triple(T, A, B, C) &
11 isConstant(A) &
12 isConstant(B) &
13 isConstant(C)
14 ->
15 ground(T)
16 ).
17
18 all Formula L R (
19 conjunction(Formula, L, R) &
20 ground(L) &
21 ground(R)
22 ->
23 ground(Formula)
24 ).
25
26 all Formula L R (
27 disjunction(Formula, L, R) &
28 ground(L) &
29 ground(R)
30 ->
31 ground(Formula)
32 ).
33
34 all Formula L R (
35 conditional(Formula, L, R) &
36 ground(L) &
37 ground(R)
38 ->
39 ground(Formula)
40 ).
41
42 all Formula L R (
43 biconditional(Formula, L, R) &
44 ground(L) &
45 ground(R)
46 ->
47 ground(Formula)
48 ).
49
50 all Formula Child (
51 negation(Formula, Child) &
52 ground(Child)
53 ->
54 ground(Formula)
55 ).
56
57 % this one is quite different; I don't know if it will be useful for
58 % something....
59 all Formula Var Child (
60 quantification(Formula, Var, Child)
61 ->
62 -ground(Formula)
63 ).
Sandro Hawke
Generated Thu Aug 22 16:30:54 EDT 2002