function TreeModelProp() // Do we know something about Tree Model Property of the Logic?
{
// ========= Negative ===========================================
if(RNeg) // Extensions of ALC(neg)
{
TreeAnswer='No';
TreeComment='The concept A '+sAND+
' ∀(¬R).¬A is satisfiable, but has no tree models.'+
' See ['+LutzSattler2001+', Sect.2].';
return;
}
if(FNQ>0 && RCrc==1 && RinN) // ALCF(o) with complex roles in F
{
TreeAnswer='No';
TreeComment='The ALCF(o)-concept (≥2 R) '+
sAND+' (∀R.∃S.T) '+
sAND+' (≤2 RoS) is satisfiable, but has no tree models.'+
' See ['+BaaderSattler1999+', Sect. 3].';
return;
}
if(II==1 && HH==1) // Extensions of ALCHI, thanks to Birte Glimm
{
TreeAnswer='No';
TreeComment='In ALCHI, symmetric roles are expressible by a TBox '+
'{ R ⊆ R— }, '+
'so that the concept ∃R.T has no tree models. '+
'(Or maybe this kind of models are still countered as tree-like?).';
return;
}
// Now positive, for concrete logics
if(RR==0)
{ // Logics without "Complex Role Inclusion Axioms"
if(MM==0)
{
// ========= Positive ===========================================
if(Logic(0,0,0,0) && TBoxIsEmpty) // ALC = K. So - see Modal Logic!
{
TreeAnswer='Yes';
TreeComment='ALC is a notational variant of the multi-modal logic Km (cf. ['+Schild1991+']), '+
'for which the tree model property can be found in ['+MLBook+', Proposition 2.15].';
return;
}
if(LogicBetween(0,0,0,0,0,0,0,0,0,0,0,
0,0,1,0,1,0,1,0,1,1,1) && !RinN) // All logics below ALCFI_trans
{
TreeAnswer='Yes';
TreeComment='For all sublogics of ALCFIreg with any TBoxes; see ['+
DLBook+', p.189, Theorem 5.6].';
return;
}
}else{ // Logics with Mu-Operator
if(Logic(0,0,0,reg)) // mu-ALC
{
TreeAnswer='Yes';
TreeComment='See ['+StreettEmerson1989+'].';
return;
}
if(LogicInterval(0,2,0,reg, 0,3,0,reg)) // mu-ALCO < L < mu-ALCIO -- No (?)
{
TreeAnswer='No';
TreeComment='See ['+SattlerVardi2001+'].';
return;
}
} // end of "Mu-Operator".
} // End "No Complex Role Inclusions"
else // Complex Role Inclusions: RIQ, SRIQ, SROIQ
{
}
}