Fundamenta Informaticae - Volume 176, issue 3-4

Authors: Della Monica, Dario | Murano, Aniello | Sauro, Luigi

Article Type: Other

DOI: 10.3233/FI-2020-1971

Citation: Fundamenta Informaticae, vol. 176, no. 3-4, pp. i-ii, 2020

Authors: Su, Ezgi Iraz

Article Type: Research Article

Abstract: This paper presents a general strategy, bringing together some major types of nonmonotonic reasoning under a monotonic bimodal setting. Such formalisms are also of interest to the fields of knowledge representation and declarative programming. We exemplify the methodology, capturing minimal model reasoning that underlies nonmonotonicity over S4F first, but then we also show how to apply the technique to other nonmonotonic logics respectively based on the modal logics KD45 and SW5 . We naturally succeed it, by modifying only the axioms of the underlying modal logic and show that it successfully works. The last two formalisms are also …known as autoepistemic logic (AEL ) and its reflexive extension (R AEL ) in the given order: AEL is an important form of nonmonotonic reasoning, introduced by Robert C. Moore in order to allow an agent to reason about his own knowledge. Equilibrium logic (EL ) is a general-purpose nonmonotonic reasoning formalism, proposed more recently by David Pearce as a semantical framework for answer set programming (ASP ). The latter is an efficient declarative problem solving approach with lots of applications to science and technology. Fariñas et al. have embedded EL (and so ASP ) into a monotonic bimodal logic. We take this work as an initiative and successfully apply a similar methodology to closely aligned nonmonotonic modal logics. We finally discuss the potential capability to subsume the epistemic extensions of ASP within our unified paradigm. Show more

Keywords: nonmonotonic reasoning, minimal model semantics, (autoepistemic) equilibrium logic, answer set programming, epistemic specifications, monotonic modal logic, Kripke model

DOI: 10.3233/FI-2020-1972

Citation: Fundamenta Informaticae, vol. 176, no. 3-4, pp. 205-234, 2020

Authors: Giordano, Laura | Gliozzi, Valentina

Article Type: Research Article

Abstract: Reasoning about exceptions in ontologies is nowadays one of the challenges the description logics community is facing. The paper describes a preferential approach for dealing with exceptions in Description Logics, based on the rational closure. The rational closure has the merit of providing a simple and efficient approach for reasoning with exceptions, but it does not allow independent handling of the inheritance of different defeasible properties of concepts. In this work we outline a possible solution to this problem by introducing a weaker variant of the lexicographical closure, that we call skeptical closure , which requires to construct a single …base. We develop a bi-preference semantics for defining a characterization of the skeptical closure. Show more

DOI: 10.3233/FI-2020-1973

Citation: Fundamenta Informaticae, vol. 176, no. 3-4, pp. 235-269, 2020

Authors: Alviano, Mario | Dodaro, Carmine

Article Type: Research Article

Abstract: Many efficient algorithms for the computation of optimum stable models in the context of Answer Set Programming (ASP) are based on unsatisfiable core analysis. Among them, algorithm OLL was the first introduced in the context of ASP, whereas algorithms ONE and PMRES were first introduced for solving the Maximum Satisfiability problem (MaxSAT) and later on adapted to ASP. In this paper, we present the porting to ASP of another state-of-the-art algorithm introduced for MaxSAT, namely K , which generalizes ONE and PMRES . Moreover, we present a new algorithm called OLL-IN-ONE that compactly encodes all aggregates …of OLL by taking advantage of shared aggregate sets propagators. The performance of the algorithms have been empirically compared on instances taken from the latest ASP Competition. Show more

Keywords: Answer Set Programming, weak constraints, unsatisfiable core analysis

DOI: 10.3233/FI-2020-1974

Citation: Fundamenta Informaticae, vol. 176, no. 3-4, pp. 271-297, 2020

Authors: Tarzariol, Alice | Zanazzo, Eugenia | Dovier, Agostino | Policriti, Alberto

Article Type: Research Article

Abstract: The main goal of this work is to propose a tool-chain capable of analyzing a data collection of temporally qualified (genetic) mutation profiles, i.e., a collection of DNA-sequences (genes) that present variations with respect to their “healthy” versions. We implemented a system consisting of a front-end, a reasoning core, and a post-processor: the first transforms the input data retrieved from medical databases into a set of logical facts, while the last displays the computation results as graphs. Concerning the reasoning core, we employed the Answer Set Programming paradigm, which is capable of deducing complex information from data. However, since the …system is modular, this component can be replaced by any logic programming tool for different kinds of data analysis. Indeed, we tested the use of a probabilistic inductive logic programming core. Show more

Keywords: Bioinformatics, Big Data Analysis, ASP

DOI: 10.3233/FI-2020-1975

Citation: Fundamenta Informaticae, vol. 176, no. 3-4, pp. 299-319, 2020

Authors: Alberti, Marco | Gavanelli, Marco | Lamma, Evelina | Riguzzi, Fabrizio | Satoh, Ken | Zese, Riccardo

Article Type: Research Article

Abstract: Abductive Logic Programming (ALP) has been proven very effective for formalizing societies of agents, commitments and norms, in particular by mapping the most common deontic operators (obligation, prohibition, permission) to abductive expectations. In our previous works, we have shown that ALP is a suitable framework for representing norms. Normative reasoning and query answering were accommodated by the same abductive proof procedure, named 𝒮 CIFF. In this work, we introduce a defeasible flavour in this framework, in order to possibly discharge obligations in some scenarios. Abductive expectations can also be qualified as dischargeable, in the new, extended syntax. Both …declarative and operational semantics are improved accordingly, and proof of soundness is given under syntax allowedness conditions Moreover, the dischargement itself might be proved invalid, or incoherent with the rules, due to new knowledge provided later on. In such a case, a discharged expectation might be reinstated and hold again after some evidence is given. We extend the notion of dischargement to take into consideration also the reinstatement of expectations. The expressiveness and power of the extended framework, named 𝒮 CIFF𝒟 , is shown by modeling and reasoning upon a fragment of the Japanese Civil Code. In particular, we consider a case study concerning manifestations of intention and their rescission (Section II of the Japanese Civil Code). Show more

Keywords: Normative reasoning, Abductive Logic Programming, Constraint Logic Programming, Dischargement of expectations

DOI: 10.3233/FI-2020-1976

Citation: Fundamenta Informaticae, vol. 176, no. 3-4, pp. 321-348, 2020

Authors: Cantone, Domenico | Nicolosi-Asmundo, Marianna | Santamaria, Daniele Francesco

Article Type: Research Article

Abstract: In this paper we consider the most common TBox and ABox reasoning services for the description logic 𝒟ℒ〈4LQSR,x 〉(D) (𝒟 ℒ D 4 , × , for short) and prove their decidability via a reduction to the satisfiability problem for the set-theoretic fragment 4LQSR . 𝒟 ℒ D 4 , × is a very expressive description logic. It combines the high scalability and efficiency of rule languages such as the SemanticWeb Rule Language (SWRL) with the expressivity of description logics. In fact, among other features, it supports Boolean operations …on concepts and roles, role constructs such as the product of concepts and role chains on the left-hand side of inclusion axioms, role properties such as transitivity, symmetry, reflexivity, and irreflexivity, and data types. We further provide a KE-tableau-based procedure that allows one to reason on the main TBox and ABox reasoning tasks for the description logic 𝒟 ℒ D 4 , × . Our algorithm is based on a variant of the KE-tableau system for sets of universally quantified clauses, where the KE-elimination rule is generalized in such a way as to incorporate the γ-rule. The novel system, called KEγ -tableau, turns out to be an improvement of the system introduced in [1] and of standard first-order KE-tableaux [2]. Suitable benchmark test sets executed on C++ implementations of the three mentioned systems show that in several cases the performances of the KEγ -tableau-based reasoner are up to about 400% better than the ones of the other two systems. Show more

DOI: 10.3233/FI-2020-1977

Citation: Fundamenta Informaticae, vol. 176, no. 3-4, pp. 349-384, 2020