Fundamenta Informaticae - Volume 124, issue 4

Authors: Fioravanti, Fabio | Pettorossi, Alberto | Rossi, Gianfranco

Article Type: Other

DOI: 10.3233/FI-2013-838

Citation: Fundamenta Informaticae, vol. 124, no. 4, pp. i-ii, 2013

Authors: Alberti, Marco | Gavanelli, Marco | Lamma, Evelina

Article Type: Research Article

Abstract: Abduction is a form of inference that supports hypothetical reasoning and has been applied to a number of domains, such as diagnosis, planning, protocol verification. Abductive Logic Programming (ALP) is the integration of abduction in logic programming. Usually, the operational semantics of an ALP language is defined as a proof procedure. The first implementations of ALP proof-procedures were based on the meta-interpretation technique, which is flexible but limits the use of the built-in predicates of logic programming systems. Another, more recent, approach exploits theoretical results on the similarity between abducibles and constraints. With this approach, which bears the advantage of …an easy integration with built-in predicates and constraints, Constraint Handling Rules has been the language of choice for the implementation of abductive proof procedures. The first CHR-based implementation mapped integrity constraints directly to CHR rules, which is an efficient solution, but prevents defined predicates from being in the body of integrity constraints and does not allow a sound treatment of negation by default. In this paper, we describe the CHR-based implementation of the SCIFF abductive proof-procedure, which follows a different approach. The SCIFF implementation maps integrity constraints to CHR constraints, and the transitions of the proof-procedure to CHR rules, making it possible to treat default negation, while retaining the other advantages of CHR-based implementations of ALP proof-procedures. Show more

DOI: 10.3233/FI-2013-839

Citation: Fundamenta Informaticae, vol. 124, no. 4, pp. 365-381, 2013

Authors: Bistarelli, Stefano | Santini, Francesco

Article Type: Research Article

Abstract: The aggregation of generic items into coalitions leads to the creation of sets of homogenous entities. In this paper we accomplish this for an input set of arguments, and the result is a partition according to distinct lines of thought, i.e., groups of “coherent” ideas. We extend Dung's Argumentation Framework (AF) in order to deal with coalitions of arguments. The initial set of arguments is partitioned into not-intersected subsets. All the found coalitions show the same property inherited by Dung, e.g., all the coalitions in the partition are admissible (or conflict-free, complete, stable): they are generated according to Dung's principles. …Each of these coalitions can be assigned to a different agent. We use Soft Constraint Programming as a formal approach to model and solve such partitions in weighted AFs: semiring algebraic structures can be used to model different optimization criteria for the obtained coalitions. Moreover, we implement and solve the presented problem with JaCoP, a Java constraint solver, and we test the code over a small-world network. Show more

DOI: 10.3233/FI-2013-840

Citation: Fundamenta Informaticae, vol. 124, no. 4, pp. 383-401, 2013

Authors: Campagna, Dario | Formisano, Andrea

Article Type: Research Article

Abstract: Product configuration systems are an emerging technology that supports companies in deploying mass customization strategies. Such strategies need to cover the management of the whole customizable product cycle. Adding process modeling and configuration features to a product configurator may improve its ability to assist mass customization development. In this paper, we describe a modeling framework, PRODPROC, that allows one to model both a product and its production process. We first introduce our framework by describing how configurable products are modeled. Then, we describe the main features and capabilities offered to model production processes and to link them with the corresponding …products models. The configuration task (namely, the procedure that, from a configurable object/activity generates a configured product/process) is then analyzed. We also outline a possible CSP-based implementation of a configurator. A comparison with some of the existing systems for product configuration and process modeling emphasizes that none of the considered system/tools offers the complete set of features supported by PRODPROC for interdependent product and process modeling/configuration. Show more

Keywords: Product and process modeling languages, Configuration of product/process models

DOI: 10.3233/FI-2013-841

Citation: Fundamenta Informaticae, vol. 124, no. 4, pp. 403-425, 2013

Authors: Cantone, Domenico | Asmundo, Marianna Nicolosi

Article Type: Research Article

Abstract: We introduce a multi-sorted stratified syllogistic, called 4LQSR , admitting variables of four sorts and a restricted form of quantification over variables of the first three sorts, and prove that it has a solvable satisfiability problem by showing that it enjoys a small model property. Then, we consider the fragments (4LQSR )h of 4LQSR , consisting of 4LQSR -formulae whose quantifier prefixes have length bounded by h ≥ 2 and satisfying certain additional syntactical constraints, and prove that each of them has an NP-complete satisfiability problem. Finally we show that the modal logic K45 can be expressed in (4LQSR …)3 . Show more

DOI: 10.3233/FI-2013-842

Citation: Fundamenta Informaticae, vol. 124, no. 4, pp. 427-448, 2013

Authors: Costantini, Stefania | Formisano, Andrea

Article Type: Research Article

Abstract: Weight constraints are a powerful programming construct that has proved very useful within the Answer Set Programming paradigm. In this paper, we argue that practical Answer Set Programming might take profit from introducing some forms of nested weight constraints. We define such empowered constraints (that we call “Nested Weight Constraints”) and discuss their semantics and their complexity.

Keywords: Weight constraints in ASP, Non-monotonic reasoning, Knowledge representation

DOI: 10.3233/FI-2013-843

Citation: Fundamenta Informaticae, vol. 124, no. 4, pp. 449-464, 2013

Authors: D'Agostino, Giovanna | Lenzi, Giacomo

Article Type: Research Article

Abstract: We consider the μ-calculus over graphs where the accessibility relation is an equivalence (S5-graphs). We show that the vectorial μ-calculus model checking problem over arbitrary graphs reduces to the vectorial, existential μ-calculus model checking problem over S5 graphs. Moreover, we give a proof that satisfiability of μ-calculus in S5 is NP-complete, and by using S5 graphs we give a new proof that the satisfiability problem of the existential μ-calculus is also NP-complete. Finally we prove that on multimodal S5, in contrast with the monomodal case, the fixpoint hierarchy of the μ-calculus is infinite and the finite model property fails.

Keywords: μ-Calculus, Parity Games, Equivalence Relations, S5, Model Checking

DOI: 10.3233/FI-2013-844

Citation: Fundamenta Informaticae, vol. 124, no. 4, pp. 465-482, 2013

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

Article Type: Research Article

Abstract: Program specialization has been proposed as a means of improving constraint-based analysis of infinite state reactive systems. In particular, safety properties can be specified by constraint logic programs encoding (backward or forward) reachability algorithms. These programs are then transformed, before their use for checking safety, by specializing them with respect to the initial states (in the case of backward reachability) or with respect to the unsafe states (in the case of forward reachability). By using the specialized reachability programs, we can considerably increase the number of successful verifications. An important feature of specialization algorithms is the so called polyvariance, that …is, the number of specialized variants of the same predicate that are introduced by specialization. Depending on this feature, the specialization time, the size of the specialized program, and the number of successful verifications may vary. We present a specialization framework which is more general than previous proposals and provides control on polyvariance. We demonstrate, through experiments on several infinite state reactive systems, that by a careful choice of the degree of polyvariance we can design specialization-based verification procedures that are both efficient and precise. Show more

Keywords: Program specialization, constraint logic programming, polyvariance, generalization, verification of infinite state reactive systems, unfold/fold transformation

DOI: 10.3233/FI-2013-845

Citation: Fundamenta Informaticae, vol. 124, no. 4, pp. 483-502, 2013

Authors: Lisi, Francesca A. | Straccia, Umberto

Article Type: Research Article

Abstract: Fuzzy Description Logics (DLs) are logics that allow to deal with structured vague knowledge. Although a relatively important amount of work has been carried out in the last years concerning the use of fuzzy DLs as ontology languages, the problem of automatically managing the evolution of fuzzy ontologies has received very little attention so far. We describe here a logic-based computational method for the automated induction of fuzzy ontology axioms which follows the machine learning approach of Inductive Logic Programming. The potential usefulness of the method is illustrated by means of an example taken from the tourism application domain.

Keywords: Inductive Logic Programming, Fuzzy Description Logics, Ontologies

DOI: 10.3233/FI-2013-846

Citation: Fundamenta Informaticae, vol. 124, no. 4, pp. 503-519, 2013

Authors: Riguzzi, Fabrizio

Article Type: Research Article

Abstract: Probabilistic Logic Programming is receiving an increasing attention for its ability to model domains with complex and uncertain relations among entities. In this paper we concentrate on the problem of approximate inference in probabilistic logic programming languages based on the distribution semantics. A successful approximate approach is based on Monte Carlo sampling, that consists in verifying the truth of the query in a normal program sampled from the probabilistic program. The ProbLog system includes such an algorithm and so does the cplint suite. In this paper we propose an approach for Monte Carlo inference that is based on a program …transformation that translates a probabilistic program into a normal program to which the query can be posed. The current sample is stored in the internal database of the Yap Prolog engine. The resulting system, called MCINTYRE for Monte Carlo INference wiTh Yap REcord, is evaluated on various problems: biological networks, artificial datasets and a hidden Markov model. MCINTYRE is compared with the Monte Carlo algorithms of ProbLog and cplint and with the exact inference of the PITA system. The results show that MCINTYRE is faster than the other Monte Carlo systems. Show more

Keywords: Probabilistic Logic Programming, Monte Carlo Methods, Logic Programs with Annotated Disjunctions, ProbLog

DOI: 10.3233/FI-2013-847

Citation: Fundamenta Informaticae, vol. 124, no. 4, pp. 521-541, 2013

Authors: Solomakhin, Dmitry | Franconi, Enrico | Mosca, Alessandro

Article Type: Research Article

Abstract: Automated support to enterprise modeling has increasingly become a subject of interest for organizations seeking solutions for storage, distribution and analysis of knowledge about business processes. This interest has recently resulted in approving the standard for specifying Semantics of Business Vocabulary and Business Rules (SBVR). Despite the existence of formally grounded notations, up to now SBVR still lacks a sound and consistent logical formalization which would allow developing automated solutions able to check the consistency of a set of business rules. This work reports on the attempt to provide logical foundations for SBVR by the means of defining a specific …first-order deontic-alethic logic (FODAL). The connections of FODAL with the modal logic QK and the description logic 𝒜ℒ𝒞𝒬ℐ have been investigated and, on top of the obtained theoretical results, a special tool providing automated support for consistency checks of a set of 𝒜ℒ𝒞𝒬ℐ-expressible deontic and alethic business rules has been implemented. Show more

Keywords: business rules, deontic rules, consistency, reasoning, ORM2

DOI: 10.3233/FI-2013-848

Citation: Fundamenta Informaticae, vol. 124, no. 4, pp. 543-560, 2013

Authors: Zhou, Neng-Fa | Dovier, Agostino

Article Type: Research Article

Abstract: This paper presents our program in B-Prolog submitted to the third ASP solver competition for the Sokoban problem. This program, based on dynamic programming, treats Sokoban as a generalized shortest path problem. It divides a problem into independent subproblems and uses mode-directed tabling to store subproblems and their answers. This program is very simple but quite efficient. Without use of any sophisticated domain knowledge, it easily solves 14 of the 15 instances used in the competition. We show that the approach can be easily applied to other optimization planning problems.

DOI: 10.3233/FI-2013-849

Citation: Fundamenta Informaticae, vol. 124, no. 4, pp. 561-575, 2013

Article Type: Other

Citation: Fundamenta Informaticae, vol. 124, no. 4, pp. 577-578, 2013