Logic Programming and Nonmonotonic Reasoning

In this paper, we present a syntactic transformation, called the unfolding operator, that allows forgetting an atom in a logic program (under ASP semantics). The main advantage of unfolding is that, unlike other syntactic operators, it is always applicable and guarantees strong persistence, that is, the result preserves the same stable models with respect to any context where the forgotten atom does not occur. The price for its completeness is that the result is an expression that may contain the fork operator. Yet, we illustrate how, in some cases, the application of fork properties may allow us to reduce the fork to a logic program, even in conditions that could not be treated before using the syntactic methods in the literature.

Modal logic S5 is used extensively for representing knowledge that includes statements about necessity and possibility, owing to its simplicity in handling chained modal operators. Significant research effort has been devoted in developing efficient reasoning mechanisms over complex S5 formulas, resulting in various solvers taking advantage of the boolean satisfiability problem (SAT). Among them, the most performant solver implements a heuristic for identifying worlds that can be merged, hence reducing the size of SAT instances to be checked. Recently, Answer Set Programming (ASP) has also been considered, and different ASP encodings were proposed and tested, reaching state-of-the-art performance. In particular, a heuristic for identifying the propositional atoms that are relevant in every world resulted in a performance gain in previous experiments. This work addresses the open question of whether the aforementioned two heuristics can be combined, as well as possibly enabling lazy instantiation of the resulting encodings, and what their potential impact is on the performance of the ASP-based solver. Experiments show that lazy creation of worlds provides some further performance gain to the ASP-based solver on the tested instances.

Several AI problems can be conveniently modelled in ASP, and many of them require to enumerate solutions characterized by an optimality property that can be expressed in terms of subset-minimality with respect to some objective atoms. In this context, solutions are often either (i) answer sets or (ii) sets of atoms that enforce the absence of answer sets on the ASP program at hand—such sets are referred to as minimal unsatisfiable subsets (MUSes). In both cases, the required enumeration task is currently not supported by state-of-the-art ASP solvers.

Probabilistic Logic Programs under the distribution semantics (PLPDS) do not allow statistical probabilistic statements of the form “90% of birds fly”, which were defined “Type 1” statements by Halpern. In this paper, we add this kind of statements to PLPDS and introduce the PASTA (“Probabilistic Answer set programming for STAtistical probabilities”) language. We translate programs in our new formalism into probabilistic answer set programs under the credal semantics. This approach differs from previous proposals, such as the one based on “probabilistic conditionals” as, instead of choosing a single model by making the maximum entropy assumption, we take into consideration all models and we assign probability intervals to queries. In this way we refrain from making assumptions and we obtain a more neutral framework. We also propose an inference algorithm and compare it with an existing solver for probabilistic answer set programs on a number of programs of increasing size, showing that our solution is faster and can deal with larger instances.

An interesting feature that traditional approaches to inductive logic programming are missing is the ability to treat noisy and non-logical data. Neural-symbolic approaches to inductive logic programming have been recently proposed to combine the advantages of inductive logic programming, in terms of interpretability and generalization capability, with the characteristic capacity of deep learning to treat noisy and non-logical data. This paper concisely surveys and briefly compares three promising neural-symbolic approaches to inductive logic programming that have been proposed in the last five years. The considered approaches use Datalog dialects to represent background knowledge, and they are capable of producing reusable logical rules from noisy and non-logical data. Therefore, they provide an effective means to combine logical reasoning with state-of-the-art machine learning.

We propose a different way to compute sceptical semantics in the constellations approach: we define the grounded, ideal, and eager extension of a Probabilistic Argumentation Framework by merging the subsets with the maximal probability of complete, preferred, semi-stable extensions respectively. Differently from the original work (i.e., [19]), the extension we propose is unique, as the principle of scepticism usually demands. This definition maintains some well-known properties, as set-inclusion among the three semantics. Moreover, we advance a quantitative relaxation of these semantics with the purpose to mitigate scepticism in case the result corresponds to empty-set, which is not very informative.

SHACL is a W3C-proposed language for expressing structural constraints on RDF graphs. In recent years, SHACL’s popularity has risen quickly. This rise in popularity comes with questions related to its place in the semantic web, particularly about its relation to OWL (the de facto standard for expressing ontological information on the web) and description logics (which form the formal foundations of OWL). We answer these questions by arguing that SHACL is in fact a description logic. On the one hand, our answer is surprisingly simple, some might even say obvious. But, on the other hand, our answer is also controversial. By resolving this issue once and for all, we establish the field of description logics as the solid formal foundations of SHACL.

Answer set programming (ASP) solvers have advanced in recent years, with a variety of different specialisation and overall development. Thus, even more complex and detailed programs can be solved. A side effect of this development are growing solution spaces and the problem of how to find those answer sets one is interested in. One general approach is to give an overview in form of a small number of highly diverse answer sets. By choosing a favourite and repeating the process, the user is able to leap through the solution space. But finding highly diverse answer sets is computationally expensive. In this paper we introduce a new approach called Tunas for Trade Up Navigation for Answer Sets to find diverse answer sets by reworking existing solution collections. The core idea is to collect diverse answer sets one after another by iteratively solving and updating the program. Once no more answer sets can be added to the collection, the program is allowed to trade answer sets from the collection for different answer sets, as long as the collection grows and stays diverse. Elaboration of the approach is possible in three variations, which we implemented and compared to established methods in an empirical evaluation. The evaluation shows that the Tunas approach is competitive with existing methods, and that efficiency of the approach is highly connected to the underlying logic program.

This paper introduces formal models for emotional reasoning, expressing emotional states and emotional causality, using action reasoning and transition systems. A general framework is defined, comprised of two main components: 1) a model for emotions based on the Appraisal theory of Emotion (AE), and 2) a model for emotional change based on Hedonic Emotion Regulation (HER). A particular transition system is modelled in which states correspond to human emotional states and transitions correspond to restrictive (safe) ways to influence emotions while reducing negative emotional side-effects. The introduced emotional reasoning can be applied to guide a software agent’s actions for dealing with emotions while estimating and planning future interactions with humans.

In temporal extensions of Answer Set Programming (ASP) based on linear-time, the behavior of dynamic systems is captured by sequences of states. While this representation reflects their relative order, it abstracts away the specific times associated with each state. In many applications, however, timing constraints are important like, for instance, when planning and scheduling go hand in hand. We address this by developing a metric extension of linear-time temporal equilibrium logic, in which temporal operators are constrained by intervals over natural numbers. The resulting Metric Equilibrium Logic provides the foundation of an ASP-based approach for specifying qualitative and quantitative dynamic constraints. To this end, we define a translation of metric formulas into monadic first-order formulas and give a correspondence between their models in Metric Equilibrium Logic and Monadic Quantified Equilibrium Logic, respectively. Interestingly, our translation provides a blue print for implementation in terms of ASP modulo difference constraints.

Epistemic Logic Programs (ELPs), extend Answer Set Programming (ASP) with epistemic operators. The semantics of such programs is provided in terms of world views, which are sets of belief sets. Different semantic approaches propose different characterizations of world views. Recent work has introduced semantic properties that should be met by any semantics for ELPs, like the Epistemic Splitting Property, that, if satisfied, allows to modularly compute world views in a bottom-up fashion, analogously to ‘traditional’ ASP. We analyze the possibility to change the perspective, shifting from a bottom-up to a top-down approach to splitting. Our new definition: (i) copes with concerns regarding unfoundedness of world views and subjective constraint monotonicity; (ii) is provably applicable to many of the existing semantics; (iii) operates similarly to “traditional” ASP; (iv) provably coincides with the bottom-up notion of splitting at least on the class of Epistemically Stratified Programs (which are, intuitively, those where the use of epistemic operators is stratified).

Answer Set Programming (ASP) is a well-established declarative AI formalism for knowledge representation and reasoning. ASP systems were successfully applied to both industrial and academic problems. Nonetheless, their performance can be improved by embedding domain-specific heuristics into their solving process. However, the development of domain-specific heuristics often requires both a deep knowledge of the domain at hand and a good understanding of the fundamental working principles of the ASP solvers. In this paper, we investigate the use of deep learning techniques to automatically generate domain-specific heuristics for ASP solvers targeting the well-known graph coloring problem. Empirical results show that the idea is promising: the performance of the ASP solver wasp can be improved.

Model-based Diagnosis (MBD) is an approach to diagnosis, where an (objective) model of a system is diagnosed to find a set of explanations revealing root causes for issues. Temporal behavioral models are prominent approach for temporal MBD, where their associated temporal formulas (TBFs) by Brusoni et al. (Artificial Intelligence, 102:39–79, 1998) can be used to relate explanations to observations under temporal constraints based on Allen’s Interval Algebra (IA). Due to expressive limitations of the constructs, we envision an extended language of TBFs that allows for complex formulas and nesting of formulas in temporal constraints. To this end, we present a language that extends propositional resp. FO logic with IA relations and provide semantics for it based on here-and-there (HT) logic as well as on Equilibrium Logic. Furthermore, we lift a well-known tableau calculus for propositional HT logic to the temporal setting and report about an experimental prototype implementation. Based on these results, rich notions of diagnostic explanations from temporal behavior models may be developed.

Abstract dialectical frameworks (ADFs) are a well-studied generalisation of the prominent argumentation frameworks due to Phan Minh Dung. In this paper we propose to use reduced ordered binary decision diagrams (roBDDs) as a suitable representation of the acceptance conditions of arguments within ADFs. We first show that computational complexity of reasoning on ADFs represented by roBDDs is milder than in the general case, with a drop of one level in the polynomial hierarchy. Furthermore, we present a framework to systematically define heuristics for search space exploitation, based on easily retrievable properties of roBDDs and the recently proposed approach of weighted faceted navigation for answer set programming. Finally, we present preliminary experiments of an implementation of our approach showing promise both when compared to state-of-the-art solvers and when developing heuristics for reasoning.

This paper studies the problem of arguing program correctness for logic programs with aggregates in the context of Answer Set Programming. Cabalar, Fandinno, and Lierler (2020) championed a modular methodology for arguing program correctness. We show how a recently proposed many-sorted semantics for logic programs with aggregates allows us to apply their methodology to this type of program. This is illustrated using well-known encodings for the Graph Coloring and Traveling Salesman problems. In particular, we showcase how this modular approach allows us to reuse the proof of correctness of a Hamiltonian Cycle encoding studied in a previous publication when considering the Traveling Salesman program.

Answer set programming (ASP) is a declarative programming paradigm where the solutions of a search problem are captured by the answer sets of a logic program describing its solutions. Besides native algorithms implemented as answer-set solvers, the computation of answer sets can be realized (i) by translating the logic program into propositional logic or its extensions and (ii) by finding satisfying assignments with appropriate solvers. In this work, we recall the graph-based extension of propositional logic, viz. SAT modulo graphs, and the case of acyclicity constraint which keeps a digraph associated with each truth assignment acyclic. This particular extension lends itself very well for answer set computation, e.g., using extended SAT solvers, such as GraphSAT, as back-end solvers. The goal of this work, however, is to translate away the acyclicity extension altogether using a vertex elimination technique, giving rise to a translation from ASP into propositional clauses only. We use non-tight benchmarks and a state-of-the-art SAT solver, Kissat, to illustrate that performance obtained in this way can be competitive against GraphSAT and native ASP solvers such as Clasp and Wasp.

Answer set programming (ASP) is a popular declarative programming paradigm with various applications. Programs can easily have so many answer sets that they cannot be enumerated in practice, but counting still allows to quantify solution spaces. If one counts under assumptions on literals, one obtains a tool to comprehend parts of the solution space, so called answer set navigation. But navigating through parts of the solution space requires counting many times, which is expensive in theory. There, knowledge compilation compiles instances into representations on which counting works in polynomial time. However, these techniques exist only for CNF formulas and compiling ASP programs into CNF formulas can introduce an exponential overhead. In this paper, we introduce a technique to iteratively count answer sets under assumptions on knowledge compilations of CNFs that encode supported models. Our anytime technique uses the principle of inclusion-exclusion to systematically improve bounds by over- and undercounting. In a preliminary empirical analysis we demonstrate promising results. After compiling the input (offline phase) our approach quickly (re)counts.

We propose an approach for reasoning about actions with domain descriptions including an $$\mathcal{E}\mathcal{L}^{\bot }$$ E L ⊥ ontology in a temporal action theory. The action theory is based on a Dynamic Linear Time Temporal Logic, whose extensions are defined through temporal answer sets. The work provides conditions under which action consistency can be guaranteed with respect to an $$\mathcal{E}\mathcal{L}^{\bot }$$ E L ⊥ ontology, by polynomially encoding an $$\mathcal{E}\mathcal{L}^{\bot }$$ E L ⊥ knowledge base into a domain description of the temporal action theory.

The process of explaining a piece of evidence by constructing a set of assumptions that are a good explanation for that evidence is ubiquitous in real-life (e.g. in legal systems). In this paper, we introduce, discuss, and formalise the notion of stable explanations in a non-monotonic setting. We show how, while applying it to the process of (1) computing a set of literals able to (2) derive a conclusion (3) from a set of defeasible rules, we obtain a restricted version of the notion of abduction. This is both interesting and useful: when an explanation for a given conclusion is stable, it can, in fact, be used to infer the same conclusion independently of other pieces of evidence that are found afterwards.

Conditional literals are an expressive Answer Set Programming language construct supported by the solver clingo. Their semantics are currently defined by a translation to infinitary propositional logic, however, we develop an alternative characterization with the SM operator which does not rely on grounding. This allows us to reason about the behavior of a broad class of clingo programs/encodings containing conditional literals, without referring to a particular input/instance of an encoding. We formalize the intuition that conditional literals behave as nested implications, and prove the equivalence of our semantics to those implemented by clingo.

In this paper we develop a state transition function for partially observable multi-agent epistemic domains and implement it using Answer Set Programming (ASP). The transition function computes the next state upon an occurrence of a single action. Thus it can be used as a module in epistemic planners. Our transition function incorporates ontic, sensing and announcement actions and allows for arbitrary nested belief formulae and general common knowledge. A novel feature of our model is that upon an action occurrence, an observing agent corrects his (possibly wrong) initial beliefs about action precondition and his observability. By examples, we show that this step is necessary for robust state transition. We establish some properties of our state transition function regarding its soundness in updating beliefs of agents consistent with their observability.

A rapidly increasing amount of data, information and knowledge is becoming available on the Web, often written in different formats and languages, adhering to standardizations driven by the World Wide Web Consortium initiative. Taking advantage of all this heterogeneous knowledge requires its integration for more sophisticated reasoning services and applications. To fully leverage the potential of such systems, their inferences should be accompanied by justifications that allow a user to understand a proposed decision/recommendation, in particular for critical systems (healthcare, law, finances, etc.). However, determining such justifications has commonly only been considered for a single formalism, such as relational databases, description logic ontologies, or declarative rule languages. In this paper, we present the first approach for providing provenance for heterogeneous knowledge bases building on the general framework of multi-context systems, as an abstract, but very expressive formalism to represent knowledge bases written in different formalisms and the flow of information between them. We also show under which conditions and how provenance information in this formalism can be computed.

Computing small (subset-minimal or smallest) explanations is a computationally challenging task for various logics and non-monotonic formalisms. Arguably the most progress in practical algorithms for computing explanations has been made for propositional logic in terms of minimal unsatisfiable subsets (MUSes) of conjunctive normal form formulas. In this work, we propose an approach to computing smallest MUSes of quantified Boolean formulas (QBFs), building on the so-called implicit hitting set approach and modern QBF solving techniques. Connecting to non-monotonic formalisms, our approach finds applications in the realm of abstract argumentation in computing smallest strong explanations of acceptance and rejection. Justifying our approach, we pinpoint the complexity of deciding the existence of small MUSes for QBFs with any fixed number of quantifier alternations. We empirically evaluate the approach on computing strong explanations in abstract argumentation frameworks as well as benchmarks from recent QBF Evaluations.

Axiom pinpointing is the task of identifying the axiomatic causes for a consequence to follow from an ontology. Different approaches have been proposed in the literature for finding one or all the subset-minimal subontologies that preserve a description logic consequence. We propose an approach that leverages the capabilities of answer set programming for transparent axiom pinpointing. We show how other associated tasks can be modelled without much additional effort.

Logic programs (LPs) and argumentation frameworks (AFs) are two declarative knowledge representation (KR) formalisms used for different reasoning tasks. The purpose of this study is interlinking two different reasoning components. To this end, we introduce two frameworks: LPAF and AFLP. The former enables to use the result of argumentation in AF for reasoning in LP, while the latter enables to use the result of reasoning in LP for arguing in AF. These frameworks are extended to bidirectional frameworks in which AF and LP can exchange information with each other. We also investigate their connection to several general KR frameworks from the literature.

We propose a method for computing supported models of normal logic programs in vector spaces using gradient information. First, the program is translated into a definite program and embedded into a matrix representing the program. We introduce a loss function based on the implementation of the immediate consequence operator $$T_P$$ T P by matrix-vector multiplication with a suitable thresholding function, and we incorporate regularization terms into the loss function to avoid undesirable results. The proposed thresholding operation is an almost everywhere differentiable alternative to the non-linear thresholding operation. We report the results of several experiments where our method shows promising performance when used with adaptive gradient update.

Using answer set programming in real-world applications requires that the answer set program is correct and adequately represents knowledge. In this paper, we present strategies to resolve unintended contradictory statements resulting from modelling gaps and other flaws by modifying the program without manipulating the actual conflicting rules (inconsistency-causing rules with complementary head literals). We show how latent conflicts can be detected to prevent further conflicts during the resolution process or after subsequent modifications in the future. The presented approach is another step towards a general framework where professional experts who are not necessarily familiar with ASP can repair existing answer set programs and independently resolve conflicts resulting from contradictory statements in an informative way. In such a framework, conflict resolution strategies allow for generating possible solutions that consist of informative extensions and modifications of the program. In interaction with the professional expert, these solution options can then be used to obtain the solution that represents the underlying knowledge best.

In this paper, we present a system, called xASP, for generating explanations that explain why an atom belongs to (or does not belong to) an answer set of a given program. The system can generate all possible explanations for a query without the need to simplify the program before computing explanations, i.e., it works with non-ground programs. These properties distinguish xASP from existing systems such as $$\texttt{xClingo}$$ xClingo , $$\texttt{DiscASP}$$ DiscASP , $$\textit{exp}(\textit{ASP}^c)$$ exp ( ASP c ) , and $$\textit{s(CASP)}$$ s ( CASP ) , which also generate explanations for queries to logic programs under the answer set semantics but simplify and ground the programs (the three systems $$\texttt{xClingo}$$ xClingo , $$\texttt{DiscASP}$$ DiscASP , $$\textit{exp}(\textit{ASP}^c)$$ exp ( ASP c ) ) or do not always generate all possible explanations (the system $$\textit{s(CASP)}$$ s ( CASP ) ). In addition, the output of xASP is insensitive to syntactic variations such as the order conditions and the order of rules, which is also different from the output of $$\textit{s(CASP)}$$ s ( CASP ) .

Answer Set Programming with Quantifiers ASP(Q) is a recent extension of Answer Set Programming (ASP) that allows one to model problems from the entire polynomial hierarchy. Earlier work focused on demonstrating modeling capabilities of ASP(Q). In this paper, we propose a modular ASP(Q) solver that translates a quantified ASP program together with a given data instance into a Quantified Boolean Formula (QBF) to be solved by any QBF solver. We evaluate the performance of our solver on several instances and with different back-end QBF solvers, demonstrating the efficacy of ASP(Q) as a tool for rapid modeling and solving of complex combinatorial problems. The benchmark problems we use include two new ones, Argumentation Coherence and Para-coherent ASP, for which we develop elegant ASP(Q) encodings.

Abstract argumentation and Dung’s framework are popular for modeling and evaluating arguments in artificial intelligence. We consider various counting problems in abstract argumentation under practical aspects. We revisit algorithms and establish a framework that employs dynamic programming on tree decompositions for counting extensions of abstract argumentation frameworks under admissible, stable, and complete semantics. We provide an empirical evaluation and investigate conditions under which our approach is useful.

We present the ASP-based visualization tool clingraph, which aims at visualizing ASP by means of ASP itself. This idea traces back to the aspviz tool and clingraph redevelops and extends it in the context of modern ASP systems. More precisely, clingraph takes graph specifications in terms of ASP facts and hands them over to the graph visualization system graphviz. The use of ASP provides a great interface between logic programs and/or answer sets and their visualization. Also, clingraph offers a Python API that extends this ease of interfacing to clingo’s API, and in turn to connect and monitor various aspects of the solving process.

Answer set programming (ASP) has long been used for modeling and solving hard search problems. Experience shows that the performance of ASP tools on different ASP encodings of the same problem may vary greatly from instance to instance and it is rarely the case that one encoding outperforms all others. We describe a system and its implementation that given a set of encodings and a training set of instances, builds performance models for the encodings, predicts the execution time of these encodings on new instances, and uses these predictions to select an encoding for solving.

While certification has been successful in the context of satisfiablity solving, with most state-of-the-art solvers now able to provide proofs of unsatisfiability, in maximum satisfiability, such techniques are not yet widespread. In this paper, we present QMaxSATpb, an extension of QMaxSAT that can produce proofs of optimality in the VeriPB proof format, which itself builds on the well-known cutting planes proof system. Our experiments demonstrate that proof logging is possible without much overhead.

This work presents a real-life application developed to assist adhesive experts in the selection of suitable adhesives. As the popularity of adhesive joints in industry increases, so does the need for tools to support the selection process. While such tools already exist, they are either too limited in scope, or offer too little flexibility in use. In this work, we first extract experts’ knowledge about this domain and formalize it in a Knowledge Base (KB). The IDP-Z3 reasoning system can then be used to derive the necessary functionality from this KB. Together with a user-friendly interactive interface, this creates an easy-to-use tool capable of assisting the adhesive experts. The experts are positive about the tool, stating that it will help save time and find more suitable adhesives.

Payroll management is a critical business task that is subject to a large number of rules, which vary widely between companies, sectors and countries. Moreover, the rules are often complex and change regularly. Therefore, payroll management systems must be flexible in design. In this paper, we suggest an approach based on a flexible Answer Set Programming model, and an easy-to-read tabular representation based on the DMN standard. It allows HR consultants to represent complex rules without the need for a software engineer, and to ultimately design payroll systems for diverging scenarios. We show how the multi-shot solving capabilities of the clingo ASP system can be used to reach the performance that is necessary to handle real-world instances.

Analyzing the propagation of faults is part of the preliminary safety assessment for complex safety-critical systems. A recent work proposes an smt-based approach to deal with propagation of faults in presence of circular dependencies. The set of all the fault configurations that cause the violation of a property, also referred to as the set of minimal cut sets, is computed by means of repeated calls to the smt solver, hence enumerating all minimal models of an smt formula. Circularity is dealt with by imposing a strict temporal order, using the theory of difference logic.In this paper, we explore the use of Answer-Set Programming to tackle the same problem. We propose two encodings, leveraging the notion of stable model. The first approach deals with cycles in the encoding, while the second relies on asp Modulo Acyclicity (aspma).We experimentally evaluate the three approaches on a comprehensive set of benchmarks. The first asp-based encoding significantly outperforms the smt-based approach; the aspma-based encoding, on the other hand, does not yield the expected performance gains.

Comparative Case Analysis is an analytical process used to detect serial offending. It focuses on identifying distinctive behaviour that an offender displays consistently when committing their crimes. In practice, crime analysts consider the context in which each behaviour occurs to determine its distinctiveness, which subsequently impacts on their determination of whether crimes are committed by the same person or not. Existing algorithms do not currently consider context in this way when generating linkage predictions.This paper presents the first learning-based approach aimed at identifying contexts within which behaviour may be considered more distinctive. We show how this problem can be modelled as that of learning preferences (in answer set programming) from examples of ordered pairs of contexts in which a behaviour was observed. In this setting, a context is preferred to another context if the behaviour is rarer in the first context. We make novel use of odds ratios to determine which examples are used for learning. Our approach has been applied to a real dataset of serious sexual offences provided by the UK National Crime Agency. The approach provides (i) a systematic methodology for selecting examples from which to learn preferences; (ii) novel insights for practitioners into the contexts under which an exhibited behaviour is more rare.

Declarative business process discovery aims at identifying sets of constraints, from a given formal language, that characterise a workflow by using pre-recorded activity logs. Since the provided logs represent a fraction of all the consistent evolution of a process, and the fact that many sets of constraints covering those examples can be selected, empirical criteria should be employed to identify the “best” candidates. In our work we frame the process discovery as an optimisation problem, where we want to identify optimal sets of constraints according to preference criteria. Declarative constraints for processes are usually characterised via temporal logics, so different solutions can be semantically equivalent. For this reason, it is difficult to use an arbitrary finite domain constraints solvers for the optimisation. The use of Answer Set Programming enables the combination of deduction rules within the optimisation algorithm, in order to take into account not only the user preferences but also the implicit semantics of the formal language. In this paper we show how we encoded the process discovery problem using the ASPrin framework for qualitative and quantitative optimisation in ASP, and the results of our experiments.

In the last decades, Deep Learning (DL)-based approaches have been fruitfully employed in many tasks, such as providing valuable support to computer-aided diagnosis and medicine. However, DL-based approaches are known to suffer from some limitations; for instance, they lack of proper means for providing clear explanations and interpretations of the results, or explicitly including available knowledge to drive decisions. In this work, we present DeduDeep, the prototypical implementation of a framework explicitly conceived with the aim of tackling such limitations by making use of deductive declarative formalisms. In particular, the framework aims at enabling the declarative encoding of explicit knowledge, and, by relying on the use of Answer Set Programming (ASP), taking advantage of it for driving decisions taken by neural networks and refining the output. The framework has been tested using different artificial neural networks tailored to semantic segmentation tasks over Laryngeal Endoscopic Images and Freiburg Sitting People Images.