Project

General

Profile

Statistics
| Branch: | Revision:

cool / fact.conf @ master

History | View | Annotate | Download (4.34 KB)

1 d511285a Thorsten WiƟmann
[LeveLogger]
2
3
;--- Logging file name
4
 file = reasoning.log
5
;--- Logging level (the less level you give, the less information will be logged)
6
 allowedLevel = 0
7
8
9
[Tuning]
10
11
;---
12
;--- Option 'IAOEFLG': text ---
13
;---
14
;* 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.
15
;* Default value: '1263005'
16
17
; IAOEFLG = 1263005
18
19
;---
20
;--- Option 'absorptionFlags': text ---
21
;---
22
;* 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
23
;* Default value: 'BTECFSR'
24
25
; absorptionFlags = BTECFSR
26
27
;---
28
;--- Option 'alwaysPreferEquals': boolean ---
29
;---
30
;* 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.
31
;* Default value: 'true'
32
33
; alwaysPreferEquals = 1
34
35
;---
36
;--- Option 'dumpQuery': boolean ---
37
;---
38
;* Option 'dumpQuery' dumps sub-TBox relevant to given satisfiability/subsumption query.
39
;* Default value: 'false'
40
41
; dumpQuery = 0
42
43
;---
44
;--- Option 'orSortSat': text ---
45
;---
46
;* 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.
47
;* Default value: '0'
48
49
; orSortSat = 0
50
51
;---
52
;--- Option 'orSortSub': text ---
53
;---
54
;* 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).
55
;* Default value: '0'
56
57
; orSortSub = 0
58
59
;---
60
;--- Option 'testTimeout': integer ---
61
;---
62
;* Option 'testTimeout' sets timeout for a single reasoning test in milliseconds.
63
;* Default value: '0'
64
65
; testTimeout = 0
66
67
;---
68
;--- Option 'useAnywhereBlocking': boolean ---
69
;---
70
;* Option 'useAnywhereBlocking' allow user to choose between Anywhere and Ancestor blocking.
71
;* Default value: 'true'
72
73
; useAnywhereBlocking = 1
74
75
;---
76
;--- Option 'useBackjumping': boolean ---
77
;---
78
;* Option 'useBackjumping' switch backjumping on and off. The usage of backjumping usually leads to much faster reasoning.
79
;* Default value: 'true'
80
81
; useBackjumping = 1
82
83
;---
84
;--- Option 'useCompletelyDefined': boolean ---
85
;---
86
;* Option 'useCompletelyDefined' leads to simpler Taxonomy creation if TBox contains no non-primitive concepts. Unfortunately, it is quite rare case.
87
;* Default value: 'true'
88
89
; useCompletelyDefined = 1
90
91
;---
92
;--- Option 'useLazyBlocking': boolean ---
93
;---
94
;* Option 'useLazyBlocking' makes checking of blocking status as small as possible. This greatly increase speed of reasoning.
95
;* Default value: 'true'
96
97
; useLazyBlocking = 1
98
99
;---
100
;--- Option 'usePrecompletion': boolean ---
101
;---
102
;* Option 'usePrecompletion' switchs on and off precompletion process for ABox.
103
;* Default value: 'false'
104
105
; usePrecompletion = 0
106
107
;---
108
;--- Option 'useRelevantOnly': boolean ---
109
;---
110
;* 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.
111
;* Default value: 'false'
112
113
; useRelevantOnly = 0
114
115
;---
116
;--- Option 'useSemanticBranching': boolean ---
117
;---
118
;* Option 'useSemanticBranching' switch semantic branching on and off. The usage of semantic branching usually leads to faster reasoning, but sometime could give small overhead.
119
;* Default value: 'true'
120
121
; useSemanticBranching = 1
122
123
[Query]
124
125
;--
126
;-- targets for single satisfiability (is Target sat) or subsumption (if Target [= Target2 holds) test
127
;--
128
129
Target = SAT
130
; Target2 = *BOTTOM*
131
132
;***
133
;*** please do not change lines below
134
;***
135
136
;--
137
;-- target KB
138
;--
139
TBox = fact.tbox