Fundamenta Informaticae - Volume 96, issue 3

Article Type: Other

DOI: 10.3233/FI-2009-176

Citation: Fundamenta Informaticae, vol. 96, no. 3, pp. i-ii, 2009

Authors: Bergenti, Federico | Dal Pal `, Alessandro | Rossi, Gianfranco

Article Type: Research Article

Abstract: This paper summarizes a constraint solving technique that is used to reason effectively in the scope of a set-based constraint language that supersedes existing finite domain languages. The first part of this paper motivates the presented work and introduces the constraint language, namely the language of Hereditarily Finite Sets (HFS). Then, the proposed constraint solver is detailed in terms of a set of rewrite rules that exploit finite domain reasoning within the HFS language. The …proposed solution improves previous work on CLP (SET) [11] by integrating intervals into the constraint system and by providing a new layered architecture for the solver that supports more effective constraint solving strategies. On the other hand, the proposed approach provides enhanced expressivity and flexibility of domain representation than those usually found in existing finite domain constraint solvers. Show more

Keywords: Finite Domain constraints, Set Constraints, Hereditarily Finite Sets

DOI: 10.3233/FI-2009-177

Citation: Fundamenta Informaticae, vol. 96, no. 3, pp. 227-252, 2009

Authors: Bozzato, Loris | Ferrari, Mauro | Villa, Paola

Article Type: Research Article

Abstract: Following the approaches given in recent works about action languages over description logics, we propose an action formalism based on a constructive information terms semantics for ALC. We discuss how a notion of state can be naturally encoded by this semantics. We address the problems of determining executability of an action, building the state obtained by an action application and checking its consistency: we present an algorithm to solve the latter two problems.

DOI: 10.3233/FI-2009-178

Citation: Fundamenta Informaticae, vol. 96, no. 3, pp. 253-269, 2009

Authors: Bria, Annamaria | Faber, Wolfgang | Leone, Nicola

Article Type: Research Article

Abstract: Disjunctive logic programming under the answer set semantics (DLP, ASP) has been acknowledged as a versatile formalism for knowledge representation and reasoning during the last decades. Lifschitz, Tang, and Turner have introduced an extended language of DLP, called Nested Logic Programming (NLP), in 1999 [12]. It often allows for more concise representations by permitting a richer syntax in rule heads and bodies. However, that language is propositional and thus does not allow for variables, …one of the strengths of DLP. In this paper, we introduce a language similar to NLP, called Normal Form Nested (NFN) programs, which does allow for variables, and present the syntax and semantics. However, with the introduction of variables an important issue arises: domain independence, the question of whether the semantics of a program is independent of the considered domain (given that it is sufficiently rich). Domain independence, originally studied for logic-based database query languages, is desirable because it guarantees that the semantics remains equal if unrelated information is added and also ensures finiteness of intended models even if infinite domains are considered. With the presence of variables, NFN programs in general are not domain independent. We study this issue in depth and define the class of safe NFN programs, which are guaranteed to be domain independent. Moreover, we show that for those NFN programs, which are also NLPs, our semantics coincides with the one of [12], while keeping the standard meaning of answer sets on DLP programs with variables. We also show that our semantics coincides with Herbrand stable models as defined in [6] of formulas corresponding to NFN programs. Finally, we provide an algorithm which transforms NFN programs into DLP programs in a correct and efficient way. We have implemented this algorithm, which provides an effective implementation of the NFN language, using existing DLP systems as a back-end. Show more

DOI: 10.3233/FI-2009-179

Citation: Fundamenta Informaticae, vol. 96, no. 3, pp. 271-295, 2009

Authors: Dal Palù, Alessandro | Dovier, Agostino | Pontelli, Enrico | Rossi, Gianfranco

Article Type: Research Article

Abstract: In recent years, Answer Set Programming has gained popularity as a viable paradigm for applications in knowledge representation and reasoning. This paper presents a novel methodology to compute answer sets of an answer set program. The proposed methodology maintains a bottom-up approach to the computation of answer sets (as in existing systems), but it makes use of a novel structuring of the computation, that originates from the non-ground version of the program. Grounding is …lazily performed during the computation of the answer sets. The implementation has been realized using Constraint Logic Programming over finite domains. Show more

Keywords: Answer set programming, logic programming, non-monotonic reasoning

DOI: 10.3233/FI-2009-180

Citation: Fundamenta Informaticae, vol. 96, no. 3, pp. 297-322, 2009

Authors: Ferrante, Alessandro | Napoli,, Margherita | Parente, Mimmo

Article Type: Research Article

Abstract: Recently, complexity issues related to the decidability of the μ-calculus, when the universal and existential quantifiers are augmented with graded modalities, have been investigated by Kupfermann, Sattler and Vardi ([19]). Graded modalities refer to the use of the universal and existential quantifiers with the added capability to express the concept of at least k or all but k, for a non-negative integer k. In this paper we study the Computational Tree Logic CTL, a branching time …extension of classical modal logic, augmented with graded modalities and investigate the complexity issues with respect to the model-checking problem. We consider a system model represented by a Kripke structure K and give an algorithm to solve the model-checking problem running in time O(|K| · |φ|) which is hence tight for the problem (here |φ| is the number of temporal and boolean operators and does not include the values occurring in the graded modalities). In this framework, the graded modalities express the ability to generate a user-defined number of counterexamples to a specification φ given in CTL. However, these multiple counterexamples can partially overlap, that is they may share some behavior. We have hence investigated the case when all of them are completely disjoint. In this case we prove that the model-checking problem is both NP-hard and coNP-hard and give an algorithm for solving it running in polynomial space. We have thus studied a fragment of graded-CTL, and have proved that the model-checking problem is solvable in polynomial time. Show more

Keywords: Model-checking, Computational Tree Logic, Graded Modalities

DOI: 10.3233/FI-2009-181

Citation: Fundamenta Informaticae, vol. 96, no. 3, pp. 323-339, 2009

Authors: Giordano, Laura | Olivetti, Nicola | Gliozzic, Valentina | Pozzato, Gian Luca

Article Type: Research Article

Abstract: We extend the Description Logic ALC with a "typicality" operator T that allows us to reason about the prototypical properties and inheritance with exceptions. The resulting logic is called ALC + T. The typicality operator is intended to select the "most normal" or "most typical" instances of a concept. In our framework, knowledge bases may then contain, in addition to ordinary ABoxes and TBoxes, subsumption relations of the form "T(C) is subsumed by P", …expressing that typical C-members have the property P. The semantics of a typicality operator is defined by a set of postulates that are strongly related to Kraus-Lehmann-Magidor axioms of preferential logic P. We first show that T enjoys a simple semantics provided by ordinary structures equipped with a preference relation. This allows us to obtain a modal interpretation of the typicality operator. We show that the satisfiability of anALC+Tknowledge base is decidable and it is precisely EXPTIME. We then present a tableau calculus for deciding satisfiability of ALC + T knowledge bases. Our calculus gives a (suboptimal) nondeterministic-exponential time decision procedure for ALC + T. We finally discuss how to extend ALC + T in order to infer defeasible properties of (explicit or implicit) individuals. We propose two alternatives: (i) a nonmonotonic completion of a knowledge base; (ii) a "minimal model" semantics for ALC + T whose intuition is that minimal models are those that maximise typical instances of concepts. Show more

Keywords: Description Logics, Prototypical Reasoning, Tableaux Calculi

DOI: 10.3233/FI-2009-182

Citation: Fundamenta Informaticae, vol. 96, no. 3, pp. 341-372, 2009

Authors: Senni, Valerio | Pettorossi, Alberto | Proietti, Maurizio

Article Type: Research Article

Abstract: The existential variables of a clause in a constraint logic program are the variables which occur in the body of the clause and not in its head. The elimination of these variables is a transformation technique which is often used for improving program efficiency and verifying program properties. We consider a folding transformation rule which ensures the elimination of existential variables and we propose an algorithm for applying this rule in the case where the …constraints are linear inequations over rational or real numbers. The algorithm combines techniques for matching terms modulo equational theories and techniques for solving systems of linear inequations. Through some examples we show that an implementation of our folding algorithm has a good performance in practice. Show more

Keywords: Program transformation, folding rule, variable elimination, constraint logic programming

DOI: 10.3233/FI-2009-183

Citation: Fundamenta Informaticae, vol. 96, no. 3, pp. 373-393, 2009