Modular Systems: Semantics, Logic, Algorithms, Complexity - Eugenia Ternovska (Simon Fraser Univ)

Data dell'evento: 
Mercoledì, 25 Marzo, 2015 - 12:00
B203 DIAG Via Ariosto 25
Eugenia Ternovska (Simon Fraser University)

With the development of declarative programming, more and more programs
that solve practical problems are available online. Ideally, we should be able
to reuse them by first finding suitable components on the web, and then combining
them, in order to solve new more complex problems.
The main challenge is that the programs may be written in different languages
(even legacy languages), and rely on different solving technologies.
Our goal is to develop foundations for combining such programs (or agents)
and, eventually, provide practical algorithms for finding solutions.
Towards this goal, we developed a framework of Modular Systems (MS),
where individual modules can be specified in any language that admits model-theoretic semantics. For example, modules can be specified in first-order logic,
Answer Set Programming, Integer Liner Programming, sometimes even in C or Java.
In the MS framework, such modules are combined using the
algebraic operations of sequence, union, loop, projection, etc.

In this talk, I will introduce the algebra of MSs and present its
model-theoretic, inferential and structural operational semantics (SOS).
I will define a multi-logic logic of MSs, which is a logic counterpart
of the algebra. This logic can be called the Logic of Information Flow
because the direction of information propagation from agent to agent
is always clear. I will describe a high-level algorithm for solving MSs.
The algorithm was inspired by Satisfiability Modular Theory (SMT) solvers.
Finally, I will discuss the complexity of the formalism and
the descriptive complexity of modular systems, as a function
of expressiveness of individual modules. Such analysis is important because
we want our formalism to be expressive enough to represent all problems
in a class of interest, but we don't want it be too expressive
to construct practical solvers.
If there is time, I will explain an extension of MSs with preferences.

Joint work with Shahab Tasharrofi.

bio: Eugenia Ternovska is an Associate Professor at Simon
Fraser University, Vancouver, Canada. She received her PhD
in Computer Science at the University of Toronto, and
diploma at Moscow State University. Her research interests
are in Artificial Intelligence and Computational Logic.

Giuseppe De Giacomo