In this work, we present a flexible method for explaining, in human readable terms, the predictions made by decision trees used as decision support in liver transplantation. The decision trees have been obtained through machine learning applied on a dataset collected at the liver transplantation unit at the Coru\~na University Hospital Center and are used to predict long term (five years) survival after transplantation. The method we propose is based on the representation of the decision tree as a set of rules in a logic program (LP) that is further annotated with text messages. This logic program is then processed using the tool xclingo (based on Answer Set Programming) that allows building compound explanations depending on the annotation text and the rules effectively fired when a given input is provided. We explore two alternative LP encodings: one in which rules respect the tree structure (more convenient to reflect the learning process) and one where each rule corresponds to a (previously simplified) tree path (more readable for decision making).

Logic artificial intelligence (AI) is a subfield of AI where variables can take two defined arguments, True or False, and are arranged in clauses that follow the rules of formal logic. Several problems that span from physical systems to mathematical conjectures can be encoded into these clauses and be solved by checking their satisfiability (SAT). Recently, SAT solvers have become a sophisticated and powerful computational tool capable, among other things, of solving long-standing mathematical conjectures. In this work, we propose the use of logic AI for the design of optical quantum experiments. We show how to map into a SAT problem the experimental preparation of an arbitrary quantum state and propose a logic-based algorithm, called Klaus, to find an interpretable representation of the photonic setup that generates it. We compare the performance of Klaus with the state-of-the-art algorithm for this purpose based on continuous optimization. We also combine both logic and numeric strategies to find that the use of logic AI improves significantly the resolution of this problem, paving the path to develop more formal-based approaches in the context of quantum physics experiments.

We present a clustering- and demotion-based algorithm called Kmeans-FOLD to induce nonmonotonic logic programs from positive and negative examples. Our algorithm improves upon-and is inspired by-the FOLD algorithm. The FOLD algorithm itself is an improvement over the FOIL algorithm. Our algorithm generates a more concise logic program compared to the FOLD algorithm. Our algorithm uses the K-means based clustering method to cluster the input positive samples before applying the FOLD algorithm. Positive examples that are covered by the partially learned program in intermediate steps are not discarded as in the FOLD algorithm, rather they are demoted, i.e., their weights are reduced in subsequent iterations of the algorithm. Our experiments on the UCI dataset show that a combination of K-Means clustering and our demotion strategy produces significant improvement for datasets with more than one cluster of positive examples. The resulting induced program is also more concise and therefore easier to understand compared to the FOLD and ALEPH systems, two state of the art inductive logic programming (ILP) systems.

While pre-trained language models (PLMs) are the go-to solution to tackle many natural language processing problems, they are still very limited in their ability to capture and to use common-sense knowledge. In fact, even if information is available in the form of approximate (soft) logical rules, it is not clear how to transfer it to a PLM in order to improve its performance for deductive reasoning tasks. Here, we aim to bridge this gap by teaching PLMs how to reason with soft Horn rules. We introduce a classification task where, given facts and soft rules, the PLM should return a prediction with a probability for a given hypothesis. We release the first dataset for this task, and we propose a revised loss function that enables the PLM to learn how to predict precise probabilities for the task. Our evaluation results show that the resulting fine-tuned models achieve very high performance, even on logical rules that were unseen at training. Moreover, we demonstrate that logical notions expressed by the rules are transferred to the fine-tuned model, yielding state-of-the-art results on external datasets.

The pursuit of responsible AI raises the ante on both the trustworthy computing and formal methods communities.

We investigate when non-dictatorial aggregation is possible from an algorithmic perspective, where non-dictatorial aggregation means that the votes cast by the members of a society can be aggregated in such a way that there is no single member of the society that always dictates the collective outcome. We consider the setting in which the members of a society take a position on a fixed collection of issues, where for each issue several different alternatives are possible, but the combination of choices must belong to a given set X of allowable voting patterns. Such a set X is called a possibility domain if there is an aggregator that is non-dictatorial, operates separately on each issue, and returns values among those cast by the society on each issue. We design a polynomial-time algorithm that decides, given a set X of voting patterns, whether or not X is a possibility domain. Furthermore, if X is a possibility domain, then the algorithm constructs in polynomial time a non-dictatorial aggregator for X. Furthermore, we show that the question of whether a Boolean domain X is a possibility domain is in NLOGSPACE. We also design a polynomial-time algorithm that decides whether X is a uniform possibility domain, that is, whether X admits an aggregator that is non-dictatorial even when restricted to any two positions for each issue. As in the case of possibility domains, the algorithm also constructs in polynomial time a uniform non-dictatorial aggregator, if one exists. Then, we turn our attention to the case where X is given implicitly, either as the set of assignments satisfying a propositional formula, or as a set of consistent evaluations of a sequence of propositional formulas. In both cases, we provide bounds to the complexity of deciding if X is a (uniform) possibility domain. Finally, we extend our results to four types of aggregators that have appeared in the literature: generalized dictatorships, whose outcome is always an element of their input, anonymous aggregators, whose outcome is not affected by permutations of their input, monotone, whose outcome does not change if more individuals agree with it and systematic, which aggregate every issue in the same way.

We present new algorithms for computing the union and intersection of all justifications for a given ontological consequence without first computing the set of all justifications. Through an empirical evaluation, we show that our approach works well in practice for expressive description logics. In particular, the union of all justifications can be computed much faster than with existing justification-enumeration approaches. We further discuss how to use these results to repair ontologies.

Logic Production System (LPS) is a logic-based framework for modelling reactive behaviour. Based on abductive logic programming, it combines reactive rules with logic programs, a database and a causal theory that specifies transitions between the states of the database. This paper proposes a systematic mapping of the Kernel of this framework (called KELPS) into an answer set program (ASP). For this purpose a new variant of KELPS with finite models, called $n$-distance KELPS, is introduced. A formal definition of the mapping from this $n$-distance KELPS to ASP is given and proven sound and complete. The Answer Set Programming paradigm allows to capture additional behaviours to the basic reactivity of KELPS, in particular proactive, preemptive and prospective behaviours. These are all discussed and illustrated with examples. Then a hybrid framework is proposed that integrates KELPS and ASP, allowing to combine the strengths of both paradigms. Under consideration in Theory and Practice of Logic Programming (TPLP).

The expressiveness of propositional non-clausal (NC) formulas is exponentially richer than that of clausal formulas. Yet, clausal efficiency outperforms non-clausal one. Indeed, a major weakness of the latter is that, while Horn clausal formulas, along with Horn algorithms, are crucial for the high efficiency of clausal reasoning, no Horn-like formulas in non-clausal form had been proposed. To overcome such weakness, we define the hybrid class $\mathbb{H_{NC}}$ of Horn Non-Clausal (Horn-NC) formulas, by adequately lifting the Horn pattern to NC form, and argue that $\mathbb{H_{NC}}$, along with future Horn-NC algorithms, shall increase non-clausal efficiency just as the Horn class has increased clausal efficiency. Secondly, we: (i) give the compact, inductive definition of $\mathbb{H_{NC}}$; (ii) prove that syntactically $\mathbb{H_{NC}}$ subsumes the Horn class but semantically both classes are equivalent, and (iii) characterize the non-clausal formulas belonging to $\mathbb{H_{NC}}$. Thirdly, we define the Non-Clausal Unit-Resolution calculus, $UR_{NC}$, and prove that it checks the satisfiability of $\mathbb{H_{NC}}$ in polynomial time. This fact, to our knowledge, makes $\mathbb{H_{NC}}$ the first characterized polynomial class in NC reasoning. Finally, we prove that $\mathbb{H_{NC}}$ is linearly recognizable, and also that it is both strictly succincter and exponentially richer than the Horn class. We discuss that in NC automated reasoning, e.g. satisfiability solving, theorem proving, logic programming, etc., can directly benefit from $\mathbb{H_{NC}}$ and $UR_{NC}$ and that, as a by-product of its proved properties, $\mathbb{H_{NC}}$ arises as a new alternative to analyze Horn functions and implication systems.

The Tsetlin Machine (TM) is a novel machine-learning algorithm based on propositional logic, which has obtained state-of-the-art performance on several pattern recognition problems. In previous studies, the convergence properties of TM for 1-bit operation and XOR operation have been analyzed. To make the analyses for the basic digital operations complete, in this article, we analyze the convergence when input training samples follow AND and OR operators respectively. Our analyses reveal that the TM can converge almost surely to reproduce AND and OR operators, which are learnt from training data over an infinite time horizon. The analyses on AND and OR operators, together with the previously analysed 1-bit and XOR operations, complete the convergence analyses on basic operators in Boolean algebra.