Fundamenta Informaticae - Volume 140, issue 3-4

Article Type: Other

DOI: 10.3233/FI-2015-1251

Citation: Fundamenta Informaticae, vol. 140, no. 3-4, pp. i-ii, 2015

Authors: Ancona, Davide | Dovier, Agostino

Article Type: Research Article

Abstract: In this paper we study the semantics of Coinductive Logic Programming and clarify its intrinsic computational limits, which prevent, in particular, the definition of a complete, computable, operational semantics. We propose a new operational semantics that allows a simple correctness result and the definition of a simple meta-interpreter. We compare, and prove the equivalence, with the operational semantics defined and used in other papers on this topic.

Keywords: Foundations of Logic Programming, Denotational Semantics, Coinduction

DOI: 10.3233/FI-2015-1252

Citation: Fundamenta Informaticae, vol. 140, no. 3-4, pp. 221-246, 2015

Authors: Avellone, Alessandro | Fiorentini, Camillo | Momigliano, Alberto

Article Type: Research Article

Abstract: Focusing is a proof-theoretic device to structure proof search in the sequent calculus: it provides a normal form to cut-free proofs in which the application of invertible and non-invertible inference rules is structured in two separate and disjoint phases. Although stemming from proof-search considerations, focusing has not been thoroughly investigated in actual theorem proving, in particular w.r.t. termination. We present a contraction-free (and hence terminating) focused multi-succedent sequent calculus for propositional intuitionistic logic, which refines the G4ip calculus in the tradition of Vorob’ev, Hudelmeier and Dyckhoff. We prove completeness of the calculus semantically and argue that this …offers a viable alternative to other more syntactical means. Show more

DOI: 10.3233/FI-2015-1253

Citation: Fundamenta Informaticae, vol. 140, no. 3-4, pp. 247-262, 2015

Authors: Bistarelli, Stefano | Rossi, Fabio | Santini, Francesco

Article Type: Research Article

Abstract: We compare four different implementations of reasoning-tools dedicated to Abstract Argumentation Frameworks. These systems are ArgTools, ASPARTIX, ConArg2, and Dung-O-Matic. They have been tested over three different models of randomly-generated graph models, corresponding to the Erdős-Rényi model, the Kleinberg small-world model, and the scale-free Barabasi-Albert model. This first comparison is useful to study the behaviour of these tools over networks with different topologies (also small-world): we scale the number of arguments to check the limits of today’s systems. Such results can be used to guide further improvements of ConArg2 (our tool), but also different tools.

DOI: 10.3233/FI-2015-1254

Citation: Fundamenta Informaticae, vol. 140, no. 3-4, pp. 263-278, 2015

Authors: Costantini, Stefania | Formisano, Andrea

Article Type: Research Article

Abstract: In recent work, we provided a formulation of ASP programs in terms of linear logic theories. Answer sets were characterized in terms of maximal tensor conjunctions provable from such theories. In this paper, we propose a full comparison between Answer Set Semantics and its variation obtained by interpreting literals (including negative literals) as resources, which leads to a different interpretation of negation. We argue that this novel view can be of both theoretical and practical interest, and we propose a modified Answer Set Semantics that we call Resource-based Answer Set Semantics. An advantage is that of avoiding inconsistencies, as every …program has a (possibly empty) resource-based answer set. This implies however the introduction of a different way of representing constraints. We provide a characterization of the new semantics as a variation of the answer set semantics, and also in terms of Autoepistemic Logic. The latter characterization leads to a way of computing resource-based answer set via answer set solvers. Show more

Keywords: Answer Set Programming, Default Negation, Linear Logic, Autoepistemic Logic

DOI: 10.3233/FI-2015-1255

Citation: Fundamenta Informaticae, vol. 140, no. 3-4, pp. 279-305, 2015

Authors: D’Agostino, Giovanna | Omodeo, Eugenio G. | Policriti, Alberto | Tomescu, Alexandru I.

Article Type: Research Article

Abstract: We introduce and prove the basic properties of encodings that generalize to non-well-founded hereditarily finite sets the bijection defined by Ackermann in 1937 between hereditarily finite sets and natural numbers.

Keywords: Computable set theory, non-well-founded sets, bisimulation, Ackermann bijection

DOI: 10.3233/FI-2015-1256

Citation: Fundamenta Informaticae, vol. 140, no. 3-4, pp. 307-328, 2015

Authors: De Angelis, Emanuele | Fioravanti, Fabio | Pettorossi, Alberto | Proietti, Maurizio

Article Type: Research Article

Abstract: We present a method for verifying properties of imperative programs that manipulate integer arrays. Imperative programs and their properties are represented by using Constraint Logic Programs (CLP) over integer arrays. Our method is refutational. Given a Hoare triple {ϕ } prog {ψ } that defines a partial correctness property of an imperative program prog , we encode the negation of the property as a predicate incorrect defined by a CLP program P , and we show that the property holds by proving that incorrect is not a consequence of P . Program verification is performed by applying a sequence …of semantics preserving transformation rules and deriving a new CLP program T such that incorrect is a consequence of P iff it is a consequence of T . The rules are applied according to an automatic strategy whose objective is to derive a program T that satisfies one of the following properties: either (i) T is the empty set of clauses, hence proving that incorrect does not hold and prog is correct, or (ii) T contains the fact incorrect, hence proving that prog is incorrect. Our transformation strategy makes use of an axiomatization of the theory of arrays for the manipulation of array constraints, and also applies the widening and convex hull operators for the generalization of linear integer constraints. The strategy has been implemented in the VeriMAP transformation system and it has been shown to be quite effective and efficient on a set of benchmark array programs taken from the literature. Show more

DOI: 10.3233/FI-2015-1257

Citation: Fundamenta Informaticae, vol. 140, no. 3-4, pp. 329-355, 2015

Authors: Gentilini, Paolo | Martelli, Maurizio | Rosolini, Giuseppe

Article Type: Research Article

Abstract: One of the main goals of Explicit Constructive Logic (ECL) is to provide a constructive formulation of Full (Classical) Higher Order Logic LK ω that can be seen as a foundation for knowledge representation. ECL is introduced as a subsystem Z ω of LK ω . The first order case Z 1 and the propositional case Z 0 of ECL are examined as well. A comparison of constructivism from the point of view of ECL and of the corresponding features of Intuitionistic Logic, and Constructive Paraconsistent Logic is proposed.

Keywords: Constructivism in Logic, Higher Order Logic, Intuitionistic Logic, Constructive Paraconsistent Logic

DOI: 10.3233/FI-2015-1258

Citation: Fundamenta Informaticae, vol. 140, no. 3-4, pp. 357-372, 2015

Authors: Lisi, Francesca A. | Straccia, Umberto

Article Type: Research Article

Abstract: Description Logics (DLs) are a family of logic-based Knowledge Representation (KR) formalisms, which are particularly suitable for representing incomplete yet precise structured knowledge. Several fuzzy extensions of DLs have been proposed in the KR field in order to handle imprecise knowledge which is particularly pervading in those domains where entities could be better described in natural language. Among the many approaches to fuzzification in DLs, a simple yet interesting one involves the use of fuzzy concrete domains. In this paper, we present a method for learning within the KR framework of fuzzy DLs. The method induces fuzzy DL inclusion axioms …from any crisp DL knowledge base. Notably, the induced axioms may contain fuzzy concepts automatically generated from numerical concrete domains during the learning process. We discuss the results obtained on a popular learning problem in comparison with state-of-the-art DL learning algorithms, and on a test bed in order to evaluate the classification performance. Show more

Keywords: Fuzzy Description Logics, Ontologies, Concept Learning

DOI: 10.3233/FI-2015-1259

Citation: Fundamenta Informaticae, vol. 140, no. 3-4, pp. 373-391, 2015

Authors: Rossi, Gianfranco | Bergenti, Federico

Article Type: Research Article

Abstract: JSetL is a Java library that endows Java with a number of facilities that are intended to support declarative and constraint (logic) programming. In this paper we show how JSetL can be used to support general forms of nondeterministic programming in an object-oriented framework. This is obtained by combining different but related facilities, such as logical variables, set data structures, unification, along with a constraint solver that allows the user to solve nondeterministic constraints as well as to define new constraints using the nondeterminism handling facilities provided by the solver itself. Thus, the user can define her/his own general nondeterministic …procedures as new constraints, letting the constraint solver handle them. The proposed solutions are illustrated through a number of concrete Java programs using JSetL, including the implementation of simple Definite Clause Grammars. Show more

Keywords: Nondeterministic Programming, Constraint Programming, Set-based Programming, Java language

DOI: 10.3233/FI-2015-1260

Citation: Fundamenta Informaticae, vol. 140, no. 3-4, pp. 393-412, 2015