Newer
Older
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
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
[LeveLogger]
;--- Logging file name
file = reasoning.log
;--- Logging level (the less level you give, the less information will be logged)
allowedLevel = 0
[Tuning]
;---
;--- Option 'IAOEFLG': text ---
;---
;* Option 'IAOEFLG' define the priorities of different operations in TODO list. Possible values are 7-digit strings with ony possible digit are 0-6. The digits on the places 1, 2, ..., 7 are for priority of Id, And, Or, Exists, Forall, LE and GE operations respectively. The smaller number means the higher priority. All other constructions (TOP, BOTTOM, etc) has priority 0.
;* Default value: '1263005'
; IAOEFLG = 1263005
;---
;--- Option 'absorptionFlags': text ---
;---
;* Option 'absorptionFlags' sets up absorption process for general axioms. It text field of arbitrary length; every symbol means the absorption action: (B)ottom Absorption), (T)op absorption, (E)quivalent concepts replacement, (C)oncept absorption, (N)egated concept absorption, (F)orall expression replacement, (R)ole absorption, (S)plit
;* Default value: 'BTECFSR'
; absorptionFlags = BTECFSR
;---
;--- Option 'alwaysPreferEquals': boolean ---
;---
;* Option 'alwaysPreferEquals' allows user to enforce usage of C=D definition instead of C[=D during absorption, even if implication appeares earlier in stream of axioms.
;* Default value: 'true'
; alwaysPreferEquals = 1
;---
;--- Option 'dumpQuery': boolean ---
;---
;* Option 'dumpQuery' dumps sub-TBox relevant to given satisfiability/subsumption query.
;* Default value: 'false'
; dumpQuery = 0
;---
;--- Option 'orSortSat': text ---
;---
;* Option 'orSortSat' define the sorting order of OR vertices in the DAG used in satisfiability tests (used mostly in caching). Option has form of string 'Mop', see orSortSub for details.
;* Default value: '0'
; orSortSat = 0
;---
;--- Option 'orSortSub': text ---
;---
;* Option 'orSortSub' define the sorting order of OR vertices in the DAG used in subsumption tests. Option has form of string 'Mop', where 'M' is a sort field (could be 'D' for depth, 'S' for size, 'F' for frequency, and '0' for no sorting), 'o' is a order field (could be 'a' for ascending and 'd' for descending mode), and 'p' is a preference field (could be 'p' for preferencing non-generating rules and 'n' for not doing so).
;* Default value: '0'
; orSortSub = 0
;---
;--- Option 'testTimeout': integer ---
;---
;* Option 'testTimeout' sets timeout for a single reasoning test in milliseconds.
;* Default value: '0'
; testTimeout = 0
;---
;--- Option 'useAnywhereBlocking': boolean ---
;---
;* Option 'useAnywhereBlocking' allow user to choose between Anywhere and Ancestor blocking.
;* Default value: 'true'
; useAnywhereBlocking = 1
;---
;--- Option 'useBackjumping': boolean ---
;---
;* Option 'useBackjumping' switch backjumping on and off. The usage of backjumping usually leads to much faster reasoning.
;* Default value: 'true'
; useBackjumping = 1
;---
;--- Option 'useCompletelyDefined': boolean ---
;---
;* Option 'useCompletelyDefined' leads to simpler Taxonomy creation if TBox contains no non-primitive concepts. Unfortunately, it is quite rare case.
;* Default value: 'true'
; useCompletelyDefined = 1
;---
;--- Option 'useLazyBlocking': boolean ---
;---
;* Option 'useLazyBlocking' makes checking of blocking status as small as possible. This greatly increase speed of reasoning.
;* Default value: 'true'
; useLazyBlocking = 1
;---
;--- Option 'usePrecompletion': boolean ---
;---
;* Option 'usePrecompletion' switchs on and off precompletion process for ABox.
;* Default value: 'false'
; usePrecompletion = 0
;---
;--- Option 'useRelevantOnly': boolean ---
;---
;* Option 'useRelevantOnly' is used when creating internal DAG representation for externally given TBox. If true, DAG contains only concepts, relevant to query. It is safe to leave this option false.
;* Default value: 'false'
; useRelevantOnly = 0
;---
;--- Option 'useSemanticBranching': boolean ---
;---
;* Option 'useSemanticBranching' switch semantic branching on and off. The usage of semantic branching usually leads to faster reasoning, but sometime could give small overhead.
;* Default value: 'true'
; useSemanticBranching = 1
[Query]
;--
;-- targets for single satisfiability (is Target sat) or subsumption (if Target [= Target2 holds) test
;--
Target = SAT
; Target2 = *BOTTOM*
;***
;*** please do not change lines below
;***
;--
;-- target KB
;--
TBox = fact.tbox