On verification in logic database languages

We consider in this paper an extension of Datalog withmech- anisms for non-monotonic and non-deterministic reasoning and a simple form of temporal reasoning, which we refer to as Datalog++. First, we show how with this logic database language is possible to express prob- lems in heterogeneous domains, such as operation research and concur- rent programming. Second, we provide a methodology for the verifica- tion of Datalog++ programs, based on the declarative semantics, which is able to handle both atemporal and temporal properties.