Dokument-ID Dokumenttyp Verfasser/Autoren Herausgeber Haupttitel Abstract Auflage Verlagsort Verlag Erscheinungsjahr Seitenzahl Schriftenreihe Titel Schriftenreihe Bandzahl ISBN Quelle der Hochschulschrift Konferenzname Quelle:Titel Quelle:Jahrgang Quelle:Heftnummer Quelle:Erste Seite Quelle:Letzte Seite URN DOI Abteilungen OPUS4-3970 Konferenzveröffentlichung Betz, Hariolf; Raiser, Frank; Frühwirth, Thom Persistent constraints in constraint handling rules In the most abstract definition of its operational semantics, the declarative and concurrent programming language CHR is trivially non-terminating for a significant class of programs. Common refinements of this definition, in closing the gap to real-world implementations, compromise on declarativity and/or concurrency. Building on recent work and the notion of persistent constraints, we introduce an operational semantics avoiding trivial non-termination without compromising on its essential features. 2010 urn:nbn:de:kobv:517-opus-41547 Extern OPUS4-3969 Konferenzveröffentlichung Abdennadher, Slim; Ismail, Haythem; Khoury, Frederick Transforming imperative algorithms to constraint handling rules Different properties of programs, implemented in Constraint Handling Rules (CHR), have already been investigated. Proving these properties in CHR is fairly simpler than proving them in any type of imperative programming language, which triggered the proposal of a methodology to map imperative programs into equivalent CHR. The equivalence of both programs implies that if a property is satisfied for one, then it is satisfied for the other. The mapping methodology could be put to other beneficial uses. One such use is the automatic generation of global constraints, at an attempt to demonstrate the benefits of having a rule-based implementation for constraint solvers. 2010 urn:nbn:de:kobv:517-opus-41533 Extern OPUS4-3968 Konferenzveröffentlichung Brass, Stefan Range restriction for general formulas Deductive databases need general formulas in rule bodies, not only conjuctions of literals. This is well known since the work of Lloyd and Topor about extended logic programming. Of course, formulas must be restricted in such a way that they can be effectively evaluated in finite time, and produce only a finite number of new tuples (in each iteration of the TP-operator: the fixpoint can still be infinite). It is also necessary to respect binding restrictions of built-in predicates: many of these predicates can be executed only when certain arguments are ground. Whereas for standard logic programming rules, questions of safety, allowedness, and range-restriction are relatively easy and well understood, the situation for general formulas is a bit more complicated. We give a syntactic analysis of formulas that guarantees the necessary properties. 2010 urn:nbn:de:kobv:517-opus-41521 Extern OPUS4-3967 Konferenzveröffentlichung Banda, Gourinath; Gallagher, John P. Constraint-based abstraction of a model checker for infinite state systems Abstract interpretation-based model checking provides an approach to verifying properties of infinite-state systems. In practice, most previous work on abstract model checking is either restricted to verifying universal properties, or develops special techniques for temporal logics such as modal transition systems or other dual transition systems. By contrast we apply completely standard techniques for constructing abstract interpretations to the abstraction of a CTL semantic function, without restricting the kind of properties that can be verified. Furthermore we show that this leads directly to implementation of abstract model checking algorithms for abstract domains based on constraints, making use of an SMT solver. 2010 urn:nbn:de:kobv:517-opus-41516 Extern OPUS4-3966 Konferenzveröffentlichung Herre, Heinrich; Hummel, Axel Stationary generated models of generalized logic programs The interest in extensions of the logic programming paradigm beyond the class of normal logic programs is motivated by the need of an adequate representation and processing of knowledge. One of the most difficult problems in this area is to find an adequate declarative semantics for logic programs. In the present paper a general preference criterion is proposed that selects the 'intended' partial models of generalized logic programs which is a conservative extension of the stationary semantics for normal logic programs of [Prz91]. The presented preference criterion defines a partial model of a generalized logic program as intended if it is generated by a stationary chain. It turns out that the stationary generated models coincide with the stationary models on the class of normal logic programs. The general wellfounded semantics of such a program is defined as the set-theoretical intersection of its stationary generated models. For normal logic programs the general wellfounded semantics equals the wellfounded semantics. 2010 urn:nbn:de:kobv:517-opus-41501 Extern OPUS4-3965 Konferenzveröffentlichung Herre, Heinrich; Hummel, Axel A paraconsistent semantics for generalized logic programs We propose a paraconsistent declarative semantics of possibly inconsistent generalized logic programs which allows for arbitrary formulas in the body and in the head of a rule (i.e. does not depend on the presence of any specific connective, such as negation(-as-failure), nor on any specific syntax of rules). For consistent generalized logic programs this semantics coincides with the stable generated models introduced in [HW97], and for normal logic programs it yields the stable models in the sense of [GL88]. 2010 urn:nbn:de:kobv:517-opus-41496 Extern OPUS4-3964 Konferenzveröffentlichung Oetsch, Johannes; Schwengerer, Martin; Tompits, Hans Kato: a plagiarism-detection tool for answer-set programs We present the tool Kato which is, to the best of our knowledge, the first tool for plagiarism detection that is directly tailored for answer-set programming (ASP). Kato aims at finding similarities between (segments of) logic programs to help detecting cases of plagiarism. Currently, the tool is realised for DLV programs but it is designed to handle various logic-programming syntax versions. We review basic features and the underlying methodology of the tool. 2010 urn:nbn:de:kobv:517-opus-41485 Extern OPUS4-3963 Konferenzveröffentlichung Cabalar, Pedro Existential quantifiers in the rule body In this paper we consider a simple syntactic extension of Answer Set Programming (ASP) for dealing with (nested) existential quantifiers and double negation in the rule bodies, in a close way to the recent proposal RASPL-1. The semantics for this extension just resorts to Equilibrium Logic (or, equivalently, to the General Theory of Stable Models), which provides a logic-programming interpretation for any arbitrary theory in the syntax of Predicate Calculus. We present a translation of this syntactic class into standard logic programs with variables (either disjunctive or normal, depending on the input rule heads), as those allowed by current ASP solvers. The translation relies on the introduction of auxiliary predicates and the main result shows that it preserves strong equivalence modulo the original signature. 2010 urn:nbn:de:kobv:517-opus-41476 Extern OPUS4-3962 Konferenzveröffentlichung Gebser, Martin; Hinrichs, Henrik; Schaub, Torsten H.; Thiele, Sven xpanda: a (simple) preprocessor for adding multi-valued propositions to ASP We introduce a simple approach extending the input language of Answer Set Programming (ASP) systems by multi-valued propositions. Our approach is implemented as a (prototypical) preprocessor translating logic programs with multi-valued propositions into logic programs with Boolean propositions only. Our translation is modular and heavily benefits from the expressive input language of ASP. The resulting approach, along with its implementation, allows for solving interesting constraint satisfaction problems in ASP, showing a good performance. 2010 urn:nbn:de:kobv:517-opus-41466 Institut für Informatik und Computational Science OPUS4-3961 Konferenzveröffentlichung Seipel, Dietmar Practical Applications of Extended Deductive Databases in DATALOG* A wide range of additional forward chaining applications could be realized with deductive databases, if their rule formalism, their immediate consequence operator, and their fixpoint iteration process would be more flexible. Deductive databases normally represent knowledge using stratified Datalog programs with default negation. But many practical applications of forward chaining require an extensible set of user-defined built-in predicates. Moreover, they often need function symbols for building complex data structures, and the stratified fixpoint iteration has to be extended by aggregation operations. We present an new language Datalog*, which extends Datalog by stratified meta-predicates (including default negation), function symbols, and user-defined built-in predicates, which are implemented and evaluated top-down in Prolog. All predicates are subject to the same backtracking mechanism. The bottom-up fixpoint iteration can aggregate the derived facts after each iteration based on user-defined Prolog predicates. 2010 urn:nbn:de:kobv:517-opus-41457 Extern