INF-DATALOG, MO DAL LOGIC AND C OMPLEXITIES

I n f- D at alog e x t en d s t h e u su al least fi x p oint sem ant ics ofD at alog wit h great est fi x p oint sem ant ics: we d e fi n e d in f- D at alog an dch aract e rized t h e ex p r essive p owe r of variou s fragm ent s of in f- D at alogin [ 16]. In the p resent pap er, we study the complex ity of q uery evalua-t i on on fi n i t e m o d e ls for ( variou s fragm ent s of ) i n f- D at alog. We d e d u c ea unified and elementary pro of that global mo d el-check in g (i.e. com-putin g all no des satisfy in g a formula in a given structure) h as 1. qua-d r at ic d at a comp lex ity in t ime an d lin ear p rogram comp lex ity in sp acefor CT Lan d alt ern at ion - free m o d al µ- c alcu lu s, an d 2. lin ear- sp ace( d at a an d p r ogram ) c om p lex it ies, lin ear- t im e p r ogram com p lex ity an dp oly n om i al- t im e d at a c om p l ex ity for Lµk(mo d al µ- c alcu lu s wit h fi x e dalternation-depth at most k )