Doctoral Symposium of MATES'06 Abstract: Automated management and monitoring of service contracts like Service Level Agreements (SLAs) or higher-level policies is vital for efficient and reliable distributed se rvice-oriented architectures (SOA) with high quality of service (QoS) levels. IT service provider need to manage, exec ute and maintain thousands of SLAs for different customers and different types of services, which needs new levels of flexibility and automation not available with the current technology. I propose a novel rule-based knowledge representation (KR) for SLA rules and a respective rule-based service level management (RBSLM) framework. My rule-based approach based on logic programming pr ovides several advantages including automated rule chaining allowing for compact knowledge representation and high levels of automation as well as flexibility to adapt to rapidly changing business requirements. Therewith, I address an urgent need service-oriented businesses do have nowadays which is to dynamically change their business and contractual logic in order to adapt to rapidly changing business environments and to overcome the restricting nature of slow change cycles.

We show that the unification problem `is there a substitution instance of a given formula that is provable in a given logic?' is undecidable for basic modal logics K and K4 extended with the universal modality. It follows that the admissibility problem for inference rules is undecidable for these logics as well. These are the first examples of standard decidable modal logics for which the unification and admissibility problems are undecidable. We also prove undecidability of the unification and admissibility problems for K and K4 with at least two modal operators and nominals (instead of the universal modality), thereby showing that these problems are undecidable for basic hybrid logics. Recently, unification has been introduced as an important reasoning service for description logics. The undecidability proof for K with nominals can be used to show the undecidability of unification for boolean description logics with nominals (such as ALCO and SHIQO). The undecidability proof for K with the universal modality can be used to show that the unification problem relative to role boxes is undecidable for Boolean description logic with transitive roles, inverse roles, and role hierarchies (such as SHI and SHIQ).

We introduce and study logic programs whose clauses are buil t out of monotone constraint atoms . We show that the operational concept of the one-step provab ility operator generalizes to programs with monotone constraint atoms, bu t the generalization involves nondeterminism. Our main results demonstrate that our form alism is a common generalization of (1) normal logic programming with its semantics o f models, supported models and stable models, (2) logic programming with weight atoms ( lparse programs) with the semantics of stable models, as defined by Niemel a, Simons an d Soininen, and (3) of disjunctive logic programming with the possible-model semant ics of Sakama and Inoue. To appear in Theory and Practice of Logic Programming (TPLP).

In answer set programming (ASP), a problem at hand is solved by (i) writing a logic program whose answer sets correspond to the solutions of the problem, and by (ii) computing the answer sets of the program using an answer set solver as a search engine. Typically, a programmer creates a series of gradually improving logic programs for a particular problem when optimizing program length and execution time on a particular solver. This leads the programmer to a meta-level problem of ensuring that the programs are equivalent, i.e., they give rise to the same answer sets. To ease answer set programming at methodological level, we propose a translation-based method for verifying the equivalence of logic programs. The basic idea is to translate logic programs P and Q under consideration into a single logic program EQT(P,Q) whose answer sets (if such exist) yield counter-examples to the equivalence of P and Q. The method is developed here in a slightly more general setting by taking the visibility of atoms properly into account when comparing answer sets. The translation-based approach presented in the paper has been implemented as a translator called lpeq that enables the verification of weak equivalence within the smodels system using the same search engine as for the search of models. Our experiments with lpeq and smodels suggest that establishing the equivalence of logic programs in this way is in certain cases much faster than naive cross-checking of answer sets.

We introduce a constraint-based framework for studying infinite qualitative simulations concerned with contingencies such as time, space, shape, size, abstracted into a finite set of qualitative relations. To define the simulations, we combine constraints that formalize the background knowledge concerned with qualitative reasoning with appropriate inter-state constraints that are formulated using linear temporal logic. We implemented this approach in a constraint programming system by drawing on ideas from bounded model checking. The resulting system allows us to test and modify the problem specifications in a straightforward way and to combine various knowledge aspects.

I ns ti t ut Gal i lé e - U niv. P ar is - Nord 93430 V il l et ane us e - F RA NC E noui ouaf @l ipn.uni v-pa ri s 13.fr G eneral ly s peaking, form al NL s em antic s i s re ferenti al i .e. it as sum es t hat i t is pos si ble t o c reate a s tati c dis course uni verse and to equat e t he obj ect s of t his uni verse t o the (s tat ic) mea nings of w ords . The me aning of a sent ence is then buil t from t he me anings of the w ords in a c ompos iti onal proces s and the se mant ic inte rpretat ion of a s entenc e i s reduce d to it s logic al i nterpret ati on bas ed on t he t ruth condit ions . The very diffic ult tas k of ada pting the mea ning of a s ent ence to its c ontext is often left to the pragm ati c l evel, and this tas k re quires t o us e a huge a mount of com mon s ens e know ledge a bout the domai n. It has bee n s howe d t hat the above tri-pa rtit ion i s very arti fici al becaus e l inguis ti c a s we ll as e xtra-li nguis tic know ledge i nterac t i n t he s am e gl obal proces s to provide the ne ces sa ry elem ents for unders ta nding. But what kind of rea soni ng is needed for na tural language se manti cs? T he ans we r to thi s que st ion is bas ed on the remark t hat t exts s eldom provide norma l det ail s t hat are a ss umed to be known to the reader.

We present in this paper a general algorithm for solving first-order formulas in particular theories called "decomposable theories". First of all, using special quantifiers, we give a formal characterization of decomposable theories and show some of their properties. Then, we present a general algorithm for solving first-order formulas in any decomposable theory "T". The algorithm is given in the form of five rewriting rules. It transforms a first-order formula "P", which can possibly contain free variables, into a conjunction "Q" of solved formulas easily transformable into a Boolean combination of existentially quantified conjunctions of atomic formulas. In particular, if "P" has no free variables then "Q" is either the formula "true" or "false". The correctness of our algorithm proves the completeness of the decomposable theories. Finally, we show that the theory "Tr" of finite or infinite trees is a decomposable theory and give some benchmarks realized by an implementation of our algorithm, solving formulas on two-partner games in "Tr" with more than 160 nested alternated quantifiers.

The research results described are concerned with: - developing a domain modeling method and tools to provide the design and implementation of decision-making support systems for computer integrated manufacturing; - building a decision-making support system based on know-how and its software environment. The research is funded by NEDO, Japan.

The paper presents two equivalent definitions of answer sets for logic programs with aggregates. These definitions build on the notion of unfolding of aggregates, and they are aimed at creating methodologies to translate logic programs with aggregates to normal logic programs or positive programs, whose answer set semantics can be used to defined the semantics of the original programs. The first definition provides an alternative view of the semantics for logic programming with aggregates described by Pelov et al. The second definition is similar to the traditional answer set definition for normal logic programs, in that, given a logic program with aggregates and an interpretation, the unfolding process produces a positive program. The paper shows how this definition can be extended to consider aggregates in the head of the rules. The proposed views of logic programming with aggregates are simple and coincide with the ultimate stable model semantics, and with other semantic characterizations for large classes of program (e.g., programs with monotone aggregates and programs that are aggregate-stratified). Moreover, it can be directly employed to support an implementation using available answer set solvers. The paper describes a system, called ASP^A, that is capable of computing answer sets of programs with arbitrary (e.g., recursively defined) aggregates.

We extend the 0-approximation of sensing actions and incomplete information in [Son and Baral 2000] to action theories with static causal laws and prove its soundness with respect to the possible world semantics. We also show that the conditional planning problem with respect to this approximation is NP-complete. We then present an answer set programming based conditional planner, called ASCP, that is capable of generating both conformant plans and conditional plans in the presence of sensing actions, incomplete information about the initial state, and static causal laws. We prove the correctness of our implementation and argue that our planner is sound and complete with respect to the proposed approximation. Finally, we present experimental results comparing ASCP to other planners.