Kolloquium/Ringvorlesung des Graduiertenkolleg Wissensrepräsentation

Coordination is one of the defining problems in multi-agent systems research, which also impacts on many other areas of computer science research. Crudely, coordination is the problem of handling interdependencies between activities in systems containing multiple actors.

Interdependencies may be negative (such as one process overwriting critical data required by another process) or positive (such as one process assisting another by pro-actively providing data required by the other process).

Traditional approaches to coordination in distributed systems involve hardwiring a coordination regime into the system at design time; this involves a designer anticipating all relevant interactions between activities, and manually constructing a coordination mechanism to handle all such interactions. In this talk, we motivate and develop an approach to coordination based on "social laws". Roughly, a social law is a set of constraints on the behaviour of agents within a system. We investigate the computational problems associated with specifying, verifying, and automatically synthesising social laws for multi-agent systems. We then discuss an interpretation of deontic logic based on our model of social laws.

We study a collection of heterogeneous XML databases containing similar and related information, exchanging data via a peer to peer overlay network. Here, a mediated global schema is unrealistic. Yet, users/applications wish to query the databases, via one peer using its schema. We have recently developed HepToX, a P2P Heterogeneous XML database system. A key idea is that whenever a peer enters the system, it establishes an acquaintance with a small number of peer databases. The peer administrator provides correspondences between the local schema and the acquaintance schema using an intuitive notation of arrows and boxes, from which our novel algorithm infers a precise set of mapping rules. We pin down the semantics of query answering, and present a query translation algorithm for a simple but expressive fragment of XQuery. We show the translation algorithm is correct. Finally, we demonstrate the utility and scalability of our ideas and algorithms with a detailed set of experiments on top of the Emulab, a large scale P2P network emulation testbed.

This is joint work with Elaine Q. Chang, Laks V.S. Lakshmanan and Terence Ho, University of British Columbia (Canada)

Dr. Angela Bonifati is a researcher at Icar CNR (Italy). She received her MS from University of Calabria in 1997 and her PhD from Politecnico di Milano in 2001.
She held visiting positions at Stanford University (USA), HP Labs (USA), INRIA (France) and UBC (Canada). Her research interests lie in the area of database and information systems; in particular, Web-based information systems and XML data management.

Disjunctive logic programming under the stable model semantics is a new methodology called answer set programming (ASP) for solving combinatorial search problems. It is a form of declarative programming related to logic programming languages, such as Prolog. In answer set programming, solutions to a problem are represented by answer sets, and not by answer substitutions produced in response to a query as in conventional logic programming. Instead of Prolog systems, this programming method uses answer set solvers, such as for instance Smodels, Cmodels, Assat, Dlv. Systems as Assat and Cmodels use SAT solvers as their inference engines. Nowadays SAT based answer set programming systems successfully work with nondisjunctive programs. The talk will present the results on extending SAT-based system Cmodels for finding answer sets for disjunctive logic programs. Two different ways of SAT solver invocation used in nondisjunctive answer set programming are extended to the case of disjunctive programs and implemented in Cmodels. These algorithms are based on the definition of completion for disjunctive programs and the extension of loop formula definition to the disjunctive case.

The problem of the identity of proofs, i.e., the question "When are two proofs the same?" is as old as proof theory itself. To give a satisfactory answer, we have to abstract away from syntactic proof formalisms (like resolution or tableaux) and capture the "essence" of proofs.

In this talk I will present two approaches towards the identity of proofs. The first is based on "proof nets", which are concrete graph-like objects that precisely capture the essence of proofs. Cut elimination on proof nets provides a canonical way of composing proofs.

The second approach is based on abstract algebra. All proposals for an algebraic theory of proofs that have been made so far use category theory: The formulas form the objects, and the proofs form the arrows in the category. The question is then, what is the right axiomatisation for such a category of proofs.

Although the concepts mentioned above have first been developped for intuitionistic logic and linear logic, I will in the talk only concentrate on classical propositional logic. The talk will be introductory and does not require any knowledge on proof nets or category theory.

Die Allgegenwart von Viren und Root-Kits zeigt, dass bisherige Betriebssystem-Konzepte mit der zentralen Rolle eines IT-Experten als Superuser nicht geeignet sind, das Maß an Verlässlichkeit und Nichtkorrumpierbarkeit herzustellen, welches im elektronischen Geschäftsverkehr und erst recht für "elektronische Akten" (ArbGG? § 46d) erforderlich sind.

Askemos (http://www.askemos.org) ist Konzept, Projekt und Prototyp zugleich, mit denen diese Probleme bisheriger digitaler kommunikativer Umgebungen überwunden werden können. Die Konzepte sind nicht neu - vieles konnte etwa vom Design von ERLANG, einer Programmiersprache für den ausfallsicheren Betrieb von Telefonanlagen, übernommen werden - führen aber in ihrer Kombination und strikten Ausrichtung auf die Konstruktion einer nicht korrumpierbaren verteilten Dokumenten- und Rechteverwaltung zu erstaunlich klaren Ergebnissen.

Besonderes Augenmerk wurde beim Design von Askemos auf die Nichtkorrumpierbarkeit gelegt, die natürlich nicht besser sein kann als die Nichtkorrumpierbarkeit der modellierten realen Welt. Hierzu habe ich eine Reihe von Ontologisierungen entwickelt, die sich an Begriffen und Idealen des bürgerlichen Rechtssystems, insbesondere den Menschenrechten und dem Vertragsrecht, orientieren. Die für ein digitales Projekt unumgängliche Operationalisierung dieser Begriffe ist - nicht unerwartet - schwierig.

Im Vortrag werde ich mich auf den theoretischen Teil von Askemos konzentrieren, den schichtenweisen Aufbau der Begriffe und Konzepte, der als Unterbau für ein rechtssicheres System erforderlich ist, in welchem Verträge und Dokumente mit ähnlicher Verbindlichkeit verhandelt und vereinbart werden können wie dies im realen Geschäftsverkehr auch möglich ist.

Das Semantic Web muss nach der Standardisierung von Basissprachen seine Anwendbarkeit und entstehenden Mehrwert demonstrieren. In unserem Vortrag berichten wir über Ergebnisse und Erfahrungen aus laufenden Forschungsprojekten in Bereichen wie medizinischen Informationssystemen oder der Internet-basierten Personalbeschaffung. Weiterhin stellen wir erste Arbeiten zu einer Koordinationsmiddleware für ein verteiltes Semantic Web, die Semantic Web Spaces vor.

In recent years, the representation of qualitative preferential information has drawn attention of researchers in many fields: modern applications seek to employ preferences as means for specifying, designing, and controlling rational behaviors as well as intelligent systems. In this talk we consider a rather simple declarative language for policy specification (where a "policy" represents a collection of general principles specifying the desired behavior of a system), called PDL, and analyse how it can be extended to treat preferences, and how such preferences can be automatically mapped into an ASP program. Thanks to the strong connections between ASP and constraint programming, as well as non-monotonic reasoning, this mapping enables us to start from a simple policy specification and automatically get an ASP program whose solutions represent consistent results of the policy evaluation. These solutions are obtained by using rather efficient solvers that can compute the answer sets of programs defining thousands of atoms within a few seconds.
We tested our approach to policy specification and enforcement in several application contexts, such as Resource Management, Web Services Routing and Authorization Constraints specification in Workflows. On on side, this allowed us to get an application-oriented perspective, focussing how different approaches to preferences specification can be integrated and used in real contexts. On the other hand, we have been able to identify a few applicative challenges, for which extensions to the formalism may be needed.

Representation results depend sometimes on closure properties of the domain:

- closure of the domain under (finite) union, set-difference, etc.

- sufficient "richness" or "density" of the domain

- closure of the domain under the choice function considered

etc.

In my opinion, such conditions have been neglected too much, and we will begin to take a closer look at them.

Conditional logics are an extension of classical logic by a new implication connector that is weaker than material implication. In particular, the conditional is not monotonic. Conditional logics have been applied to modelize nonmonotonic and causal reasoning, update, revision and other forms of common sense reasoning.
There is no standard semantics for conditional logics. The three most important approaches are selection functions, sphere systems and preferential models. But these semantics do not characterize the same systems of conditional logics.
We present proof systems for conditional logics which can be characterized by preferential semantics. The system is based on labelled tableaux and makes use of a hybrid pseudo-modal operator for representing minimality of worlds.

We also discuss one application of conditional logic to action theory.

The *WALS *(The World Atlas of Language Structures; Haspelmath et al. 2005) is a large database of structural (phonological, grammatical, lexical) properties of languages gathered from descriptive materials (such as reference grammars) by a team of more than 40 authors (many of them the leading authorities on the subject).

Both quantitative and qualitative analysis of the data show a large number of problems that need to be solved before a concrete (and maybe linguistically specific designed) phylogenetic analysis might be applied.

In my talk I will present the techniques used for detecting/solving such problems, as well as various attempts to select the appropriate parameters for future analysis.

Gewichtete Automaten finden aktuelle Anwendungen zur Beschreibung von quantitativen Eigenschaften in so verschiedenen Gebieten wie probabilistische Automaten, digitale Bildverarbeitung oder natürliche Sprachverarbeitung. Die Gewichte werden auf Grund der vielfältigen Anwendungsmöglichkeiten allgemein als Elemente eines Semirings angenommen. Büchi und Elgot (1961) charakterisierten in einem klassischen Resultat das Verhalten von ungewichteten Automaten mit Hilfe der Logik, wodurch in der Informatik das Gebiet des Model Checkings entstand. Wir führen nun eine gewichtete monadische Logik 2. Stufe ein und zeigen, dass sich mit ihren Sätzen genau das quantitative Verhalten von gewichteten Automaten beschreiben lässt. Auf Grund von algebraischen Sätzen zu Burnside-Eigenschaften erhalten wir Konstruktions- und Entscheidbarkeitsresultate.

-----------------------------------------

Weighted automata and quantitative logics

In automata theory, a classical result of Büchi states that the recognizable languages are precisely the ones definable by sentences of monadic second order logic. We will present a generalization of this result to the context of weighted automata. A weighted automaton is a classical nondeterministic automaton in which each transition carries a weight describing e.g. the ressources used for its execution, the length of time needed, or its reliability. The behaviour (language) of such a weighted automaton is a function associating to each word the weight of its execution. We develop syntax and semantics of a quantitative logics; the semantics counts 'how often' a formula is true. Our main result shows that if the weights are taken in an arbitrary commutative semiring, then the functions associated to weighted automata are precisely the ones definable by sentences of our quantitative logic.

Wir stellen ein altbekanntes interaktives Akquisitionsverfahren aus der Formalen Begriffsanalyse vor, die sogenannte Merkmalexploration. Diskutiert werden dann naheliegende Erweiterungen und Modifikationen des Verfahrens und die Probleme, die sich dabei ergeben. Ziel des Vortrages ist weniger die Darstellung neuerer Ergebnisse; vielmehr soll diskutiert werden, wieweit die Methodik in anderer Formulierung bekannt und erprobt ist.

The field of belief revision (BR) has been, and continues to be, an active sub-area of knowledge representation. It is concerned with the problem of how an agent should rationally change its knowledge base in response to new information which, possibly, contradicts its currently held knowledge. Often it is assumed the agent has in mind some ordering of *plausibility* over the set of propositional valuations, which then acts as a guide in determining the new knowledge base. One particularly troublesome problem in BR is that of *iterated* belief revision, i.e., how an agent should respond to a *sequence* of revision inputs. This is essentially the same as asking how it should rationally update its *plausibility ordering* in response to new information. In this talk I will review some of the methods which have already been proposed for doing this, as well as propose a new one (from joint work with Thomas Meyer and Ka-Shu Wong.)

A general game player is a program that accepts formal descriptions of arbitrary games and plays these games without human intervention. General game playing requires the abilities to automatically analyze game descriptions, reason about the effects of moves (actions), and devise and execute strategies. We show how established knowledge representation languages for actions can serve as the basis of a universal game playing program. We provide insights into our system FLUXPLAYER, which came in co-3rd at the First General Game Playing World Championship in Pittsburgh last year.