Evgenia Ternovska, Simon Fraswer University, Vancouver

I will describe an ongoing project aiming at developing formal foundations of reasoning about modular systems. The basis for integration of different formalisms is classical model theory. Atomic modules are classes of structures. They can be given by, e.g., constraints,  knowledge bases, Integer Linear Programs, Constraint Satisfaction problems, be partially visible databases or decision procedures. Modules are combined using the same algebraic operations as in Codd's relational algebra. To formalize problem solving for given inputs, we add information propagation. The same algebra, but with information flow, is interpreted over a transition system and gives rise to a modal temporal logic. I give examples of information flow in formalisms for efficient reasoning such as Dynamic Logic, Description Logics, Datalog+/- and operations of graph databases. The main result connects generalized query evaluation for modular systems with temporal logic model checking over an on-the-fly constructed transition system, and with executions of abstract state machines that find solutions to modular systems.

bio: Evgenia (Eugenia) Ternovska is an associate professor at Simon Fraser University, Vancouver, Canada. She obtained her PhD at the University of Toronto in 2002. Her research interests are in Knowledge and Reasoning, in applications of Logic to Computer Science.