-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathREADME.text
113 lines (81 loc) · 3.4 KB
/
README.text
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
yadlr
=====
yadlr is multi-valued reasoning system written in Prolog.
At its current state of development, yadlr only provides ABox services
over the SHOIQ Description Logic, although there is no DL-like front
end and atleast, atmost constructs have to be translated using the
dlalldifferent built-in concept, where the "atom" is a list of variables.
Emphasis is given to coupling yadlr to a ILP systems in order to
evaluate multi-valued DL hypotheses, so there is no plan for providing
TBox services in the forseeable future.
Prolog APIs
===========
yadlr provides two Prolog front-ends, yadlr and prodlr. Although the
intension is to eventually allow all front-end and inference engine
combinations, currently the yadlr can be used with the resolution and
Prolog engine, and prodlr with the Prolog engine.
Before loading either of the front-end modules, use_inference_engine/1
and use_algebra/1 must be asserted in the user namespace.
yadlr.pl provides the following predicates:
yadlr_init( +KB )
yadlr_concept( +KB, +ConceptName )
yadlr_relation( +KB, +RelationName )
yadlr_instance( +KB, +InstanceName )
yadlr_assert( +KB, +Formula, +Degree )
check_membership/5 ( +KB, +InstanceName, +ConceptName, +Degree, -Restrictions )
check_types/5 ( +KB, +InstanceName, +Degree, ?ConceptNames, -Restrictions )
check_members/5 ( +KB, +ConceptName, +Degree, ?InstanceNames, -Restrictions )
set_proof_tree_log/1 ( +Filename|no )
unset_proof_tree_log/0
set_depth_limit/1 ( +YESNO )
prodlr.pl provides the following predicates:
declare_concept( +ConceptName, +SuperConceptName )
assert_instance( +ConceptName, +InstanceName, +Degree )
add_to_concept( +ConceptName, [ (+InstanceName, +Degree) ] )
declare_relation( +RelationName, +DomainConceptName, +RangeConceptName )
add_to_relation( +RelationName, +InstanceName, [ (+FillerInstanceName, +Degree) ] )
concept_select( +InList, ?ConceptName, -OutList )
forall_select( +InList, +RelationName, +ConceptName, -OutList )
atleast_select( +InList, ?RelationName, ?ConceptName, +Min, -OutList )
atmost_select( +InList, ?RelationName, ?ConceptName, +Max, -OutList )
self_select( +InList, ?RelationName, -OutList )
Formula Syntax
==============
S is the start symbol. F is a formula non-terminal symbol. A is an
atomic non-terminal symbol. <whatever> are terminal symbols.
S :== all(X,F)
F :== all(X,F)
F :== exists(X,F)
F :== dlnot(F)
F :== dland(F, F)
F :== dlor(F, F)
F :== dlimplies(F, F)
F :== dlequiv(F, F)
F :== C(A)
F :== R(A, A)
F :== dlalldifferent( [X1..Xn] )
A :== <Instance> | X
C :== <Concept Name>
R :== <Relation Name>
X :== <Variable>
Proof Tree Log
==============
By declaring
:- use_proof_tree_log( yes ).
each proof will print on standard output all the derivations made during
the proof. The tree representation can be retrieved from this log by
keeping track of the depth of the derivation.
STEP-TYPE is either i (initial), mp (modus-ponens), or l (leaf).
Line syntax:
LINE :== DEPTH ( STEP-TYPE ) ( NUM-RESTRS ) CLAUSE-LIST
DEPTH :== <Integer>
STEP-TYPE :== i || mp || l
NUM-RESTRS :== NUM-RESTR NUM-RESTRS
NUM-RESTR :== <Algebraic Expression involving d,x>
CLAUSE-LIST :== [ CLAUSE | CLAUSE-LIST ]
CLAUSE :== yclause( <Positive Literal List>, <Negative Lit List>, <Fuzzy Degree> )
Known Problems
==============
Complementization doesn't take into account complement relationships between
"symmetric" number restrictions and quantifiers. This is going to be tricky
to fix, I see trouble ahead.