|
Piero Bonatti,
Università di Napoli
|
|
Nonmonotonic Description Logics - Requirements, Theory, and Implementations.
|
|
|
The Semantic Web and a number of modern knowledge-based applications have turned
ontologies into a familiar, popular ICT notion. Description Logics (DLs) are one of the
major formalisms for encoding ontologies.
Many "users" of such formalisms - that is ontologies writers - would appreciate DLs to
have nonmonotonic features. For example, it would be appealing to describe taxonomies by
means of general default properties that may be later overridden in special cases (after
all, a similar behavior issupported by all object-oriented languages). However,
nonmonotonic extensions of DLs involve tricky technical problems.
This talk will briefly illustrate requirements for nonmonotonic description logics and
some of the formalisms currently available. Then we shall point out the major problems
that still have to be solved in order to apply standard tableaux optimization techniques
to nonmonotonic DLs. Such optimization techniques are crucial in making formalisms with
such a high worst-case complexity usable in practice.
|
| Profile |
|
Piero Andrea Bonatti is currently a professor at the University of Naples Federico II, and
coordinator of the working group on "Policy specification, composition, and conformance"
of the Network of Excellence REWERSE (http://rewerse.net/i2). His main research interests
cover knowledge representation and reasoning, as well as computer security and privacy. By
working in the intersection of these two areas, he is currently trying to prove that carrying
out basic research with an eye to concrete problems is not an oxymoron.
|
|
|
John-Jules Meyer,
Utrecht University
|
|
The Quest for the Holy Grail of Agent Verification
|
|
|
Since the inception of agent technology almost two decades ago, researchers have worked
both on the formal, theoretical aspects of intelligent agents and on the realisation /
implementation of them. However, the link between the two has always remained rather
unclear, to this day. A case in point is the pioneering work of Rao & Georgeff, who
developed their famous BDI (beliefs-desires-intentions) logic on the one hand, while
working on their BDI architecture and programming language AgentSpeak to realize agents,
on the other. Although the names of the logic and architecture (both containing 'BDI')
suggests an intrinsic connection, they are only superficially related. More generally,
this lack of relationship is referred to in the literature as the 'gap' between agent
logics and implemented agent systems. One of the problems is that the BDI notions in agent
logics generally are not 'grounded' in agent computations: they are rather general
notions, modelled by abstract (accessibility) relations in modal logic, and have no
apparent association with concrete agent behaviour, and an agent program in particular.
In the last 15 years we have been working on both agent logics (viz. the KARO framework)
and agent programming (viz. the agent languages 3APL and, more recently, 2APL), and
personally I have been always fascinated by the relation between the two, and in
particular how agent logics can be used to specify and verify agent programs. In this talk
I'll discuss the problem of the 'gap' and a number of routes we have taken attempting to
bridge it.
|
| Profile |
|
Prof.dr. John-Jules Ch. Meyer obtained his Ph.D. from the Vrije Universiteit (VU) in
Amsterdam in 1985. Since 1988 he has been a full professor of computer science,
subsequently at the VU in Amsterdam, Nijmegen University and Utrecht University. At the
moment he is heading the Intelligent Systems Group in Utrecht. He is a member of the IFAAMAS
board steering the international AAMAS conferences, and of the editorial boards of the
Journal of Applied Non-Classical Logics, Data and Knowledge Engineering and the Journal of
Intelligent Agents & Multi-Agent Systems. His current research interests include logics for
AI, intelligent agents and cognitive robotics. In 2005 he was awarded a fellowship of the
European Coordinating Committee for Artificial Intelligence (ECCAI).
|
|
|
Cesare Tinelli,
University of Iowa
|
|
Satisfiability Modulo Theories
|
|
|
The Satisfiability Modulo Theories problem is that of checking the satisfiability of first-order
formulas with respect to some logical theory T of interest. What distinguishes SMT from general
automated deduction is that the background theory T need not be finitely or even first-order
axiomatizable, and that specialized inference methods are used for each theory. By being
theory-specific and restricting their language to only certain classes of formulas, (such as,
typically but not exclusively, ground formulas), these specialized methods can be implemented
into solvers that are more efficient in practice than general-purpose theorem provers. While SMT
techniques have been traditionally used to support deductive software verification, they are now
finding applications in other area such as model checking and automated test generation, among
others.
Theory-specific solvers can be often described conveniently in terms of tableau calculi, especially
if one wants to prove that a solver decides a certain fragment of a theory T. In practice, however,
most modern SMT solvers are not tableau-based and follow one of two main approaches, both of which
exploit the recent technological advances in SAT solving. The "eager" approach uses smart encodings
to propositional logic to compile T-satisfiability problems into SAT problems. The "lazy" approach
instead uses general run-time mechanisms to separate plain Boolean reasoning from theory reasoning
proper, doing the latter with "small" specialized procedures and delegating the former to a
dedicated SAT engine based on the popular DPLL method.
This talk gives an overview of the SMT field, focusing on a general and extensible abstract framework,
Abstract DPLL Modulo Theories, for modeling lazy STM solvers declaratively and studying some of their
theoretical properties. The framework is used to present and discuss a few basic variants of the lazy
approach, both in the case of a single and of multiple background theories. The talk also presents an
extension of the framework that drastically simplifies the implementation of theory-specific
components, and could be of interest to implementors of ground tableaux calculi as well.
|
| Profile |
|
Cesare Tinelli has a PhD in Computer Science from the University of Illinois at Urbana-Champaign and is
currently an associate professor at the University of Iowa. His research interests include automated
reasoning, formal methods, foundations of programming languages, and applications of logic in computer
science. He has published on SMT and on theory reasoning in general in such conferences as CADE, CAV,
FTP, FroCoS, IJCAR and LPAR, as well as in a number of related workshops. He has served in the program
committee of several automated reasoning conferences and workshops, and is currently a steering
committee member of CADE, IJCAR, FTP, and FroCoS. He also co-leads an international initiative, called
SMT-LIB, supported by several research groups in academia and industry, aimed at producing a number of
common standards for SMT applications, as well as a large library of theories and benchmarks.
|
|