CS Forum: Prof. Evgenia Ternovska
Evgenia Ternovska will describe a project aiming at developing formal foundations of combined multi-language constraint solving.
CS-Forum 14:15-15:00 Odeion. Coffee from 14:00
Speaker: Prof. Evgenia Ternovska
Visiting Prof Tomi Janhunen
Abstract
I will describe a project aiming at developing formal foundations of combined multi-language constraint solving in the form of an algebra of modular systems. The basis for integration of different formalisms is the classic model theory. Each atomic module is a class of structures.
It can be given, e.g., by a set of constraints in a constraint formalism that has an associated solver, such as Answer Set Programming or Constraint Satisfaction Problem. Atomic modules are combined using the same algebraic operations as in Codd's relational algebra that is in the foundation of database management systems. Just as Codd's algebra, our algebra has a natural counterpart in logic.
Since constraint solving often involves finding solutions for given inputs, we add a direction of information propagation to the the formalism. Our algebra with information flow is interpreted over a transition system and gives rise to a modal temporal logic. Finding solutions to multi-language constraint problems can be done by solving Model Checking task for this modal temporal logic. This observation implies that both SAT-based and symbolic model checking techniques can be used.
I will describe possible applications of our formalism in hierarchical solving of large-scale discrete optimization problems and in formulating high-level solving control that can also be viewed as special-purpose propagators.
Bio
Evgenia (Eugenia) Ternovska is an associate professor at Simon Fraser University, Vancouver, Canada. She obtained her PhD under the supervision of Ray Reiter at the University of Toronto in 2002. Her research interests are in Knowledge Representation and Reasoning, in applications of Logic to Computer Science.