Abstract In this paper we develop a many-valued and multi-preferential conditional logic with typicality, based on a multi-preferential semantics, which generalizes KLM preferential semantics. We then exploit the multi-preferential semantics to provide preferential interpretation of gradual argumentation. The approach allows for conditional reasoning over arguments and boolean combination of arguments, with respect to some chosen gradual semantics, through the verification of graded (strict or defeasible) implications over an argumentation graph. The paper also develops a probabilistic semantics for gradual argumentation, which builds on the many-valued semantics.

In this paper we investigate the relationships between a multipreferential semantics for defeasible reasoning in knowledge representation and a multilayer neural network model. Weighted knowledge bases for a simple description logic with typicality are considered under a (many-valued) “concept-wise” multipreference semantics. The semantics is used to provide a preferential interpretation of MultiLayer Perceptrons (MLPs). A model checking and an entailment based approach are exploited in the verification of conditional properties of MLPs.

Abstract Weighted knowledge bases for description logics with typicality under a ‘concept-wise’ multi-preferential semantics provide a logical interpretation of MultiLayer Perceptrons. In this context, Answer Set Programming (ASP) has been shown to be suitable for addressing defeasible reasoning in the finitely many-valued case, providing a $\varPi ^{p}_{2}$ upper bound on the complexity of the problem, nonetheless leaving unknown the exact complexity and only providing a proof-of-concept implementation. This paper fulfills the lack by providing a ${P^{NP[log]}}$-completeness result and new ASP encodings that deal with both acyclic and cyclic weighted knowledge bases with large search spaces, as assessed empirically on synthetic test cases. The encodings are used to empower a reasoner for computing solutions and answering queries, possibly interacting with ASP Chef for obtaining an interactive visualization.

Abstract In this paper we establish a link between fuzzy and preferential semantics for description logics and self-organizing maps (SOMs), which have been proposed as possible candidates to explain the psychological mechanisms underlying category generalization. In particular, we show that the input/output behavior of a SOM after training can be described by a fuzzy description logic interpretation as well as by a preferential interpretation, based on a concept-wise multipreference semantics, which takes into account preferences with respect to different concepts and has been recently proposed for ranked and for weighted defeasible description logics. Properties of the network can be proven by model checking on the fuzzy or on the preferential interpretation. Starting from the fuzzy interpretation, we also provide a probabilistic account for this neural network model.

Abstract Weighted knowledge bases for description logics with typicality have been recently considered under a “concept-wise” multipreference semantics (in both the two-valued and fuzzy case), as the basis of a logical semantics of multilayer perceptrons (MLPs). In this paper we consider weighted conditional $\mathcal{ALC}$ knowledge bases with typicality in the finitely many-valued case, through three different semantic constructions. For the boolean fragment $\mathcal{LC}$ of $\mathcal{ALC}$ we exploit answer set programming and asprin for reasoning with the concept-wise multipreference entailment under a $\varphi$ -coherent semantics, suitable to characterize the stationary states of MLPs. As a proof of concept, we experiment the proposed approach for checking properties of trained MLPs.

We propose a framework for structuring the description and results of the forensic analysis of actions of investigative interest in digital applications, and for automated reasoning on such actions. A high level of abstraction is suitable for forensic stakeholders that are not ICT experts; other levels are suitable for automating experiments on the devices to establish traces left by actions, and for associating the results of the experiments. Such results are used in a computational logic framework to conclude evidence on the occurrence of actions. The evidence can be presented to stakeholders or used in further automated reasoning, and traced back to data on the device.

We formalized renvoi in private international law in JURIX 2019 in terms of modal logic fragment. In this demonstration paper, we show an implementation of the formalism by translating modal formula into a logic program.

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.

Abstract In this paper we develop a concept aware multi-preferential semantics for dealing with typicality in description logics, where preferences are associated with concepts, starting from a collection of ranked TBoxes containing defeasible concept inclusions. Preferences are combined to define a preferential interpretation in which defeasible inclusions can be evaluated. The construction of the concept-aware multipreference semantics is related to Brewka’s framework for qualitative preferences. We exploit Answer Set Programming (in particular,asprin) to achieve defeasible reasoning under the multipreference approach for the lightweight description logic ξ $\mathcal L_ \bot ^ + $ .

The paper deals with the problem of formalizing the renvoi in private international law.A rule based (first-order) fragment of a multimodal logic including context modalities as well as a (simplified) notion of common knowledge is introduced.It allows context variables to occur within modalities and context names to be used as predicate arguments, providing a simple combination of meta-predicates and modal constructs.The nesting of contexts in queries is exploited in the formalization of the renvoi problem.

In this work we study a rational extension 𝒮ℛ𝒪ℰℒ(⊓, ×)R T of the low complexity description logic 𝒮ℛ𝒪ℰℒ(⊓, ×), which underlies the OWL EL ontology language. The extension involves a typicality operator T, whose semantics is based on Lehmann and Magidor’s ranked models and allows for the definition of defeasible inclusions. We consider both rational entailment and minimal entailment. We show that deciding instance checking under minimal entailment is in general ∏2P -hard, while, under rational entailment, instance checking can be computed in polynomial time. We develop a Datalog calculus for instance checking under rational entailment and exploit it, with stratified negation, for computing the rational closure of simple KBs in polynomial time.

We explore the extension of the notion of rational closure to logics lacking the finite model property, considering the logic 𝒮𝒽𝒾𝓆. We provide a semantic characterization of rational closure in 𝒮𝒽𝒾𝓆 in terms of a preferential semantics, based on a finite rank characterization of minimal models. We show that the rational closure of a KB can be computed in EXPTIME based on a polynomial encoding of the rational extension of 𝒮𝒽𝒾𝓆 into entailment in 𝒮𝒽𝒾𝓆. We discuss the extension of rational closure to more expressive description logics.

This special issue of Fundamenta Informaticae contains the revised, extended versions of selected papers presented at the Italian Conference on Computational Logic (Convegno Italiano di Logica Computazionale, CILC 2014) which was hosted by the University of Turin, Italy, from June 16th to June 18th, 2014.The event was the twenty-ninth edition of the annual meeting of the Italian Association for Logic Programming (GULP, Gruppo Ricercatori e Utenti di Logic Programming).Since its first edition, which took place in Genoa in 1986, the annual conference organized by GULP is the main occasion of meeting and exchanging ideas and experiences among Italian researchers who work in the field of Computational Logic.During the years, this annual meeting extended its horizons from the specific field of traditional Logic Programming to more general declarative programming as well as to Artificial Intelligence and Deductive Databases.All these areas had a very significant growth over the last decades and nowadays they all play a crucial role in the fields of Information Processing and Computer Science.The program of CILC 2014 included 29 technical papers accepted for presentation (23 for long presentation and 6 for short presentation).Paper selection was made by peer reviewing.The technical presentations were of high quality and concerned several topics related to computational logic, including probabilistic logic programming, verification of logic programs, answer set programming, revision and query of ontologies, argumentation theory, proof and decision systems for non-classical logics, computable set theory, multi-agent systems, and machine learning.The conference program included also two invited talks: (i) "From logic programming to argumentation and back", by Francesca Toni (Department of Computing, Imperial College London, U.K.), and (ii) "Tractable approaches to consistent query answering in ontology-based-data access", by Riccardo Rosati (DIAG, Dipartimento di Ingegneria informatica, automatica e gestionale, Università di Roma "Sapienza", Italy).Some of the papers presented at the conference were selected for this special issue and their authors were invited to submit an improved, extended version for publication.The papers that have been accepted went through a two-round careful review by qualified international referees, to whom we express our deep gratitude for their comments and criticisms.

Abstract In this paper we exploit Answer Set Programming (ASP) for reasoning in a rational extensionSROEL(⊓,×)RTof the low complexity description logicSROEL(⊓, ×), which underlies the OWL EL ontology language. In the extended language, a typicality operatorTis allowed to define conceptsT(C) (typicalC's) under a rational semantics. It has been proven that instance checking under rational entailment has a polynomial complexity. To strengthen rational entailment, in this paper we consider a minimal model semantics. We show that, for arbitrarySROEL(⊓,×)RTknowledge bases, instance checking under minimal entailment is ΠP2-complete. Relying on a Small Model result, where models correspond to answer sets of a suitable ASP encoding, we exploit Answer Set Preferences (and, in particular, theasprinframework) for reasoning under minimal entailment.

Temporal logics are well suited for reasoning about actions, as they allow for the specification of domain descriptions including temporal constraints as well as for the verification of temporal properties. The article deals with verification of action theories defined in a temporal extension of answer set programming which combines ASP with a dynamic linear time temporal logic (DLTL). The article proposes an approach to bounded model checking that exploits the Büchi automaton construction while searching for a counterexample, with the aim of achieving completeness. The article provides an encoding in ASP of the temporal action domains and of Bounded Model Checking of DLTL formulas. The article also deals with reasoning about epistemic knowledge and incomplete states.

The paper introduces a framework based on constructive conditional logics to define axiomatization, semantics and proof methods for access control logics. We formalize the well-known says operator as a conditional normal modality and, by considering some specific ombinations of access control axioms, we define four access control logics, namely, CondACLUC⁠, CondACLU4⁠, CondACLIC and CondACLI4⁠. Such logics integrate access control logics with intuitionistic conditional logics and provide a natural formulation of Boolean principals. The well-known 'speaks for' operator introduced in the logic ABLP is defined on the top of the says modality. We provide a Kripke model semantics for the logics and we prove that their axiomatization is sound and complete with respect to the semantics. Also, we develop sound, complete, cut-free sequent calculi for them. For the logic CondACLUC⁠, which (as concerns atomic principals) is slightly stronger than the logic ICL recently introduced by Garg and Abadi, we also provide a terminating sequent calculus, thus proving that the logic is decidable and that validity in CondACLUC is in PSPACE.

Computer Interpretable Guidelines (CIG) are an emerging area of research, to support medical decision making through evidence-based recommendations. However, new challenges in the data management field have to be faced, to integrate CIG management with a proper treatment of patient data, and of other forms of medical knowledge (e.g., causal and behavioral knowledge). In this position paper, we summarize a proposal for a research agenda that, in our opinion, can lead to a significant advancement in the field. The goal of the work is to provide suitable models and reasoning methodologies to cope with the aforementioned aspects, and to properly integrate them for medical decision support. Achieving such a goal requires advances in data management, and, in particular, in the treatment of indeterminate valid-time data in relational databases, of temporal abstraction on time series, of case retrieval on time series, of design-time and run-time model-based verification of guidelines, of case-based reasoning, of non-monotonic logics, of formal ontologies, of probabilistic graphical models (Bayesian Networks and Influence Diagrams).

The verification of compliance of business processes to norms requires the representation of different kinds of obligations, including achievement obligations, maintenance obligations, obligations with deadlines and contrary to duty obligations. In this paper we develop a deontic temporal extension of Answer Set Programming (ASP) suitable for verifying compliance of a business process to norms involving such different types of obligations. To this end, we extend Dynamic Linear Time Temporal Logic (DLTL) with deontic modalities to define a Deontic DLTL. We then combine it with ASP to define a deontic action language in which until formulas and next formulas are allowed to occur within deontic modalities. We show that in the language we can model the different kinds of obligations which are useful in the verification of compliance to normative requirements. The verification can be performed by bounded model checking techniques.

Abstract In this paper, we combine Answer Set Programming (ASP) with Dynamic Linear Time Temporal Logic (DLTL) to define a temporal logic programming language for reasoning about complex actions and infinite computations. DLTL extends propositional temporal logic of linear time with regular programs of propositional dynamic logic, which are used for indexing temporal modalities. The action language allows general DLTL formulas to be included in domain descriptions to constrain the space of possible extensions. We introduce a notion of Temporal Answer Set for domain descriptions, based on the usual notion of Answer Set. Also, we provide a translation of domain descriptions into standard ASP and use Bounded Model Checking (BMC) techniques for the verification of DLTL constraints.

Abstract The paper provides a framework for the verification of business processes, based on an extension of answer set programming (ASP) with temporal logic and constraints. The framework allows to capture expressive fluent annotations as well as data awareness in a uniform way. It allows for a declarative specification of a business process but also for encoding processes specified in conventional workflow languages. Verification of temporal properties of a business process, including verification of compliance to business rules, is performed by bounded model checking techniques in Answer Set Programming, extended with constraint solving for dealing with conditions on numeric data.

We propose a nonmonotonic extension of low complexity Description Logics EL ⊥ and DL-Litecore for reasoning about typicality and defeasible properties. The resulting logics are called EL ⊥ Tmin and DL-LitecTmin. we prove that entailment is in Π p 2 Concerning DL-LitecTmin,. With regard to EL ⊥ Tmin, we first show that entailment remains EXPTIME-hard. Next we consider the known fragment of Left Local EL ⊥ Tmin and we prove that the complexity of entailment drops to Π p 2. 1

We define an Intuitionistic Conditional Logic for Access Control called CICL. The logic CICLis based on a conditional language allowing principals to be defined as arbitrary formulas and it includes few uncontroversial axioms of access control logics. We provide an axiomatization and a Kripke model semantics for the logic CICL, and we prove that the axiomatization is sound and complete with respect to the semantics.

Extensions of Description Logics (DLs) to reason about typicality and defeasible inheritance have been largely investigated. In this paper, we consider two such extensions, namely (i) the extension of DLs with a typicality operator T, having the properties of Preferential nonmonotonic entailment P, and (ii) its variant with a typicality operator having the properties of the stronger Rational entailment R. The first one has been proposed in [6]. Here, we investigate the second one and we show, by a representation theorem, that it is equivalent to the approach to preferential subsumption proposed in [3]. We compare the two extensions, preferential and rational, and argue that the first one is more suitable than the second one to reason about typicality, as the latter leads to very unintuitive inferences.

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.

We present tableau calculi for the logics of nonmonotonic reasoning defined by Kraus, Lehmann and Magidor (KLM). We give a tableau proof procedure for all KLM logics, namely preferential, loop-cumulative, cumulative, and rational logics. Our calculi are obtained by introducing suitable modalities to interpret conditional assertions. We provide a decision procedure for the logics considered and we study their complexity.

We present a tableau calculus for some fundamental systems of propositional conditional logics. We consider the conditional logics that can be characterized by preferential semantics (i.e., possible world structures equipped with a family of preference relations). For these logics, we provide a uniform completeness proof of the axiomatization with respect to the semantics, and a uniform labeled tableau procedure.

The paper defines a notion of conformance of a set of k agents with a multiparty protocol with k roles, requiring the agents to be interoperable and to produce correct executions of the protocol. Conditions are introduced that enable each agent to be independently verified with respect to the protocol.

We present a tableau-based algorithm for obtaining a Buchi automaton from a formula in dynamic linear time temporal logic (DLTL), a logic which extends LTL by indexing the until operator with regular programs. The construction of the states of the automaton is similar to the standard construction for LTL, but a different technique must be used to verify the fulfillment of until formulas. The resulting automaton is a Buchi automaton rather than a generalized one. The construction can be done on-the-fly, while checking for the emptiness of the automaton.

The paper presents a logic for action theory based on a modal language, where modalities represent actions. The frame problem is tackled by using a nonmonotonic formalism which maximizes persistency assumptions. The problem of ramification is tackled by introducing a modal causality operator which is used to represent causal rules. Assumptions on the value of fluents in the initial state allow reasoning with incomplete initial states and postdiction. The action theory can also deal with nonminimal change and nondeterministic actions.

In this paper we present a modal extension of logic programming, which allows both multiple universal modal operators and embedded implications. We show that this extension is well suited for structuring knowledge and, more specifically, for defining module constructs within programs, for representing agents beliefs, and also for hypothetical reasoning. The language contains modalities [a1] to represent agent beliefs, and a modality □ which is a kind of common knowledge operator. It allows sequences of modalities to occur in front of clauses, goals and clause heads, and hypothetical implications to occur in goals and in clause bodies. We present a goal directed proof procedure for the language, and several examples of its use for defining modules are given. In particular, the language allows different proposals to be captured for module definition and composition presented in the literature. The modal logic, of which our programming language is a clausal fragment, is introduced through its Kripke semantics. This has strong similarities with the possible world semantics for the (propositional) logics of knowledge and belief proposed by Halpern & Moses. A cut-free sequent calculus is also given for this logic, which proves the soundness and completeness of the goal-directed proof procedure by showing that goal directed proofs correspond to some sequent proofs.

In this paper we present various logical characterizations of justification‐based (nonmonotonic) truth maintenance systems (JTMS). These characterizations, which are proved to be equivalent, aim at describing dependency‐directed backtracking (DDB) (i.e., the process of resolving conflicts which can arise when nogoods are allowed in the set of justifications), mainly relying on the intuitive idea that a contrapositrve use of justifications is needed to resolve inconsistencies. The idea is first formalized by means of the notion of three‐valued labeling and then through a transformation which explicitly adds all contrapositives of the justifications. An abductive characterization of the JTMS is provided through a further transformation which converts a set of nonmonotonic justifications to a corresponding abduction framework. This approach provides a unifying framework, based on the notion of abduction, for describing both JTMSs and assumption‐based TMSs (ATMSs).