function FiniteModelProp() // Do we know something about Finite Model Property of the Logic?
{
// ========= Negative ===========================================
if(SH==3 && II==1 && FNQ>0) // Extensions of SHIF has no FMP
{
FiniteAnswer='No';
FiniteComment='The SHIF-concept '+
'¬A '+sAND+' C '+sAND+
' ∀U—.C, '+
'where C ≡ ∃R—.A '+sAND+
' (≤1 R), has only infinite models '+
'w.r.t. the TBox: { R ⊆ U, Tr(U) }. '+
'See ['+HorrocksSattlerPract2000+', Sect.3.4].';
return;
}
if(II==1 && FNQ>0 && RStr==1) // Extensions of ALCIF(*)
{
FiniteAnswer='No';
FiniteComment=
'The ALCIF(*)-concept '+
'¬A '+sAND+
' ∀R*.[∃R.A '+sAND+ ' (≤1 R—)] '+
'has only infinite models. '+
'See ['+DLBook+', p.92].';
return;
}
if(II==1 && FNQ>0 && TBoxIsCycle) // Extensions of ALCIF + general TBox
{
FiniteAnswer='No';
FiniteComment=''+
'- The ALCFI-concept A is has only infinite models w.r.t. the following TBox:
'+
'{ T ⊆ ∃R.¬A; '+
'T ⊆ (≤1 R—) }. '+
// '{ A ⊆ B '+sAND+' ¬∃R—; '+
// 'B ⊆ ∃R '+sAND+' (≤1 R—) '+sAND+
// ' ∀R.B }.'+
'See also ['+DLBook+', p.209].'+
' - Finite model reasoning w.r.t. ALCQI TBoxes (and ABoxes!) is ExpTime-complete, '+
'even with binary encoding of numbers. See ['+LutzSattlerTendera2005+'].'+
'
- An intermediate result that the finite model reasoning w.r.t. ALCQI TBoxes '+
'is decidable in deterministic ExpExpTime was obtained in ['+Calvanese1996a+']; '+
'see also ['+DLBook+', p.214, Theorem 5.26].'+
'
';
return;
}
// ALC_reg(cap) has not FMP. More exactly: (cap,o,*,id(T)) or (cap,cup,+,id(T))
if(RStr==1 && RCap==1 && RIdC==1 && RCrc==1)
{
FiniteAnswer='No';
FiniteComment='The ALC(∩,o,*,id(T))-concept '
+'∀R*.(∃R.T ∩ ∀(R+∩id(T)).⊥), where '
+'R+ := R o R*,'
+' is satisfiable, but every its model has an infinite acyclic chain ['+Harel1984+', Theorem 2.35].';
}
// 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!
{
FiniteAnswer='Yes';
FiniteComment='ALC is a notational variant of the multi-modal logic Km (cf. ['+Schild1991+']), '+
'for which the finite model property can be found in ['+MLBook+', Sect. 2.3].';
return;
}
if(LogicInterval(0,0,1,0, 0,0,3,0) && TBoxIsEmpty) // All logics below ALCQ, thanks Birte!
{
FiniteAnswer='Yes';
FiniteComment='For all sublogics of ALCQ , which corresponds to Graded Modal Logic ['+
WvanderHoek1992+', '+MdeRijke2000Graded+'].';
return;
}
if(LogicInterval(0,0,0,0, 1,1,0,0) && TBoxIsEmpty) // All logics below SI, thanks Birte!
{
FiniteAnswer='Yes';
FiniteComment='For all sublogics of SI. This follows from the results in ['+HorrocksSattlerTobies1998+']: '+
'for a satisfiable concept, one can build a finite tableaux (see Lemma 6), '+
'which can be used to build a finite model (see Lemma 3). '+
'See also the corresponding Lemmas 6.7 and 6.3 in ['+TobiesPhD2001+'].';
return;
}
if(LogicInterval(0,0,0,0, 1,1,2,0) && TBoxIsEmpty) // All logics below SIN, thanks Birte!
{
FiniteAnswer='Yes';
FiniteComment='For all sublogics of SIN. This follows from the results in ['+HorrocksSattlerTobies1998+']: '+
'for a satisfiable concept, one can build a finite tableaux (see Lemma 25), '+
'which can be used to build a finite model (see Lemma 21).';
return;
}
if(LogicInterval(0,0,0,0, 3,0,3,0) ||
LogicInterval(0,2,0,0, 3,2,3,0) ) // All logics below SHOQ! i.e. (ALC,SHQ) + (ALCO,SHOQ)
{
FiniteAnswer='Yes';
FiniteComment='For all sublogics of SHOQ. This is mentioned in ['+LutzArecHorSat2004+
'], where a similar result is obtained in Corollary 4.3 for SHOQ extended with concrete domains and keys. '+
'(I did not find a \"proper\" reference for SHOQ or its sublogics.)';
return;
}
if(LogicBetween(0,0,0,0,0,0,0,0,0,0,0,
0,0,1,0,0,0,1,0,1,1,1)) // All logics below ALCI_reg + any TBoxes
{
FiniteAnswer='Yes';
FiniteComment='For all sublogics of '+((II==0)?
'ALCreg with any TBoxes; see ['+FischerLadner1979+', Theorem 3.2].':
'ALCIreg with any TBoxes; see ['+FischerLadner1979+', Theorem 3.2 and discussion after Theorem 3.3].');
return;
}
if(LogicBetween(0,0,0,0,0,0,0,0,0,0,0,
0,0,0,0,2,1,0,0,0,0,0)) // All logics below ALCN(cap) + any TBoxes, thanks Birte!
{
FiniteAnswer='Yes';
FiniteComment='For the logic ALCN(∩) with any TBoxes, see the very end of Sect. 3 in ['+Buchheit_etal_1993a+'].';
return;
}
if(Logic(0,0,0,4) && TBoxIsEmpty) // ALC(neg)
{
FiniteAnswer='Yes';
FiniteComment='See ['+Gargov_etal_1987+'].';
return;
}
}else{ // Logics with Mu-operator
if(Logic(0,0,0,reg)) // mu-ALC (We have to put "reg" here, since mu automatically checks them!)
{
FiniteAnswer='Yes';
FiniteComment='See ['+Kozen1988+', Theorem 6.1].';
}
}
} // End "No Complex Role Inclusions"
else
{ // Complex Role Inclusions: RIQ, SRIQ, sROIQ
}
}