To celebrate the first 25 years of the International Conference on Principles and Practice of Constraint Programming (CP) the editors invited the authors of the most cited paper of each year to write a commentary on their paper. This report describes our reflections on the CP 2014 paper "Incremental Cardinality Constraints for MaxSAT" and its impact on the Maximum Satisfiability community and beyond.

The article introduces a notion of a stochastic game with failure states and proposes two logical systems with modality "coalition has a strategy to transition to a non-failure state with a given probability while achieving a given goal." The logical properties of this modality depend on whether the modal language allows the empty coalition. The main technical results are a completeness theorem for a logical system with the empty coalition, a strong completeness theorem for the logical system without the empty coalition, and an incompleteness theorem which shows that there is no strongly complete logical system in the language with the empty coalition.1. Introduction In this article we study coalition power in stochastic games. An example of such a game is the road situation depicted in Figure 1. In this situation, self-driving car a is trying to pass self-driving car b . Unexpectedly, a truck moving in the opposite direction appears on the road. For the sake of simplicity, we assume that cars a and b have only three strategies: slowdown (), maintain the current speed (0), and accelerate (). We also assume that the truck is too heavy to significantly change the speed before a possible collision. The diagram in Figure 2 describes probabilities of different outcomes of all possible combinations of actions of cars a and b . This diagram has five states: state p is the current ("passing") state of the system.

A BSTRACT The capability of making interpretable and self-explanatory decisions is essential for developing responsible machine learning systems. In this work, we study the learning to explain problem in the scope of inductive logic programming (ILP). We propose Neural Logic Inductive Learning (NLIL), an efficient differentiable ILP framework that learns first-order logic rules that can explain the patterns in the data. In experiments, compared with the state-of-the-art methods, we find NLIL can search for rules that are x10 times longer while remaining x3 times faster. We also show that NLIL can scale to large image datasets, i.e. The recent years have witnessed the growing success of deep learning models in a wide range of applications. However, these models are also criticized for the lack of interpretability in its behavior and decision making process (Lipton, 2016; Mittelstadt et al., 2019), and for being data-hungry. The ability to explain its decision is essential for developing a responsible and robust decision system (Guidotti et al., 2019). On the other hand, logic programming methods, in the form of first-order logic (FOL), are capable of discovering and representing knowledge in explicit symbolic structure that can be understood and examined by human (Evans & Grefenstette, 2018). In this paper, we investigate the learning to explain problem in the scope of inductive logic programming (ILP) which seeks to learn first-order logic rules that explain the data. Traditional ILP methods (Gal arraga et al., 2015) relies on hard matching and discrete logic for rule search which is not tolerant for ambiguous and noisy data (Evans & Grefenstette, 2018). A number of works are proposed for developing differentiable ILP models that combine the strength of neural and logic-based computation (Y ang et al., 2017; Evans & Grefenstette, 2018; Campero et al., 2018; Rockt aschel & Riedel, 2017; Payani & Fekri, 2019).

This paper attempts to answer a central question in unsupervised learning: what does it mean to "make sense" of a sensory sequence? In our formalization, making sense involves constructing a symbolic causal theory that explains the sensory sequence and satisfies a set of unity conditions. This model was inspired by Kant's discussion of the synthetic unity of apperception in the Critique of Pure Reason. On our account, making sense of sensory input is a type of program synthesis, but it is unsupervised program synthesis. Our second contribution is a computer implementation, the Apperception Engine, that was designed to satisfy the above requirements. Our system is able to produce interpretable human-readable causal theories from very small amounts of data, because of the strong inductive bias provided by the Kantian unity constraints. A causal theory produced by our system is able to predict future sensor readings, as well as retrodict earlier readings, and "impute" (fill in the blanks of) missing sensory readings, in any combination. We tested the engine in a diverse variety of domains, including cellular automata, rhythms and simple nursery tunes, multi-modal binding problems, occlusion tasks, and sequence induction IQ tests. In each domain, we test our engine's ability to predict future sensor values, retrodict earlier sensor values, and impute missing sensory data. The Apperception Engine performs well in all these domains, significantly out-performing neural net baselines. We note in particular that in the sequence induction IQ tasks, our system achieved human-level performance. This is notable because our system is not a bespoke system designed specifically to solve IQ tasks, but a general purpose apperception system that was designed to make sense of any sensory sequence.

Silas: High Performance, Explainable and V erifiable Machine Learning Hadrien Bride, Zh e H ou Griffith University, Nathan, Brisbane, Australia Jie Dong Dependable Intelligence Pty Ltd, Brisbane, Australia Jin Song Dong National University of Singapore, Singapore Ali Mirjalili Griffith University, Nathan, Brisbane, AustraliaAbstract This paper introduces a new classification tool named Silas, which is built to provide a more transparent and dependable data analytics service. A focus of Silas is on providing a formal foundation of decision trees in order to support logical analysis and verification of learned prediction models. This paper describes the distinct features of Silas: The Model Audit module formally verifies the prediction model against user specifications, the Enforcement Learning module trains prediction models that are guaranteed correct, the Model Insight and Prediction Insight modules reason about the prediction model and explain the decision-making of predictions. We also discuss implementation details ranging from programming paradigm to memory management that help achieve high-performance computation.1. Introduction Machine learning has enjoyed great success in many research areas and industries, including entertainment [1], self-driving cars [2], banking [3], medical diagnosis [4], shopping [5], and among many others. However, the wide adoption of machine learn-Preprint submitted to Elsevier October 4, 2019 arXiv:1910.01382v1 The ramifications of the black-box approach are multifold. First, it may lead to unexpected results that are only observable after the deployment of the algorithm. For instance, Amazon's Alexa offered porn to a child [6], a self-driving car had a deadly accident [7], etc. Some of these accidents result in lawsuits or even lost lives, the cost of which is immeasurable. Second, it prevents the adoption in some applications and industries where an explanation is mandatory or certain specifications must be satisfied. For example, in some countries, it is required by law to give a reason why a loan application is rejected. In recent years, eXplainable AI (XAI) has been gaining attention, and there is a surge of interest in studying how prediction models work and how to provide formal guarantees for the models. A common theme in this space is to use statistical methods to analyse prediction models.

This paper presents a method for semantic indexing and describes its application in the field of knowledge representation. Starting point of the semantic indexing is the knowledge represented by concept hierarchies. The goal is to assign keys to nodes (concepts) that are hierarchically ordered and syntactically and semantically correct. With the indexing algorithm, keys are computed such that concepts are partially unifiable with all more specific concepts and only semantically correct concepts are allowed to be added. The keys represent terminological relationships. Correctness and completeness of the underlying indexing algorithm are proven. The use of classical relational databases for the storage of instances is described. Because of the uniform representation, inference can be done using case-based reasoning and generic problem solving methods.

While AI techniques have found many successful applications in autonomous systems, many of them permit behaviours that are difficult to interpret and may lead to uncertain results. We follow the "verification as planning" paradigm and propose to use model checking techniques to solve planning and goal reasoning problems for autonomous systems. We give a new formulation of Goal Task Network (GTN) that is tailored for our model checking based framework. We then provide a systematic method that models GTNs in the model checker Process Analysis Toolkit (PAT). We present our planning and goal reasoning system as a framework called Goal Reasoning And Verification for Independent Trusted Autonomous Systems (GRAVITAS) and discuss how it helps provide trustworthy plans in an uncertain environment. Finally, we demonstrate the proposed ideas in an experiment that simulates a survey mission performed by the REMUS-100 autonomous underwater vehicle.

The problem of deciding the validity (QSAT) of quantified Boolean formulas (QBF) is a vivid research area in both theory and practice. In the field of parameterized algorithmics, the well-studied graph measure treewidth turned out to be a successful parameter. A well-known result by Chen in parameterized complexity is that QSAT when parameterized by the treewidth of the primal graph of the input formula together with the quantifier depth of the formula is fixed-parameter tractable. More precisely, the runtime of such an algorithm is polynomial in the formula size and exponential in the treewidth, where the exponential function in the treewidth is a tower, whose height is the quantifier depth. A natural question is whether one can significantly improve these results and decrease the tower while assuming the Exponential Time Hypothesis (ETH). In the last years, there has been a growing interest in the quest of establishing lower bounds under ETH, showing mostly problem-specific lower bounds up to the third level of the polynomial hierarchy. Still, an important question is to settle this as general as possible and to cover the whole polynomial hierarchy. In this work, we show lower bounds based on the ETH for arbitrary QBFs parameterized by treewidth (and quantifier depth). More formally, we establish lower bounds for QSAT and treewidth, namely, that under ETH there cannot be an algorithm that solves QSAT of quantifier depth i in runtime significantly better than i-fold exponential in the treewidth and polynomial in the input size. In doing so, we provide a versatile reduction technique to compress treewidth that encodes the essence of dynamic programming on arbitrary tree decompositions. Further, we describe a general methodology for a more fine-grained analysis of problems parameterized by treewidth that are at higher levels of the polynomial hierarchy.

Answer set programming (ASP) is a declarative problem solvi ng paradigm for nonmonotonic reasoning. ASP allows intuitiive represe ntation of combinatorial search and optimization problems and is widely use d for knowledge representation and reasoning in various applications like plan generation, natural language processing etc [14, 15]. But ASP can not dea l with fuzzy information, where attributes and truth degrees lie in a con tinuous range of values. Fuzzy Answer Set Programming (F ASP) is proposed as a n extension of ASP that allows graded truth values from the interval [0,1 ]. Theoretical advancement of F ASP is remarkable [18, 32, 9, 22, 23]. Howeve r, this approach performs reasoning with absolutely certain but vagu e information and doesn't involve reasoning with uncertain information.

The growing adoption of ITsystems for the modelling and execution of (business) processes or services has thrust the scientific investigation towards techniques and tools which support complex forms of process analysis. These techniques, nowadays grouped under the umbrella of the Process Mining research area, typically rely on observation of past (tracked and logged) process executions. A first important limitation in this field is the fact that the majority of the techniques paired with concrete tool support only consider activities, but lack the ability to take into account the data objects manipulated by these activities. Second, Process Mining techniques mainly rely on complete observations of terminated process executions. In many real cases, however, only incomplete log information is available. This paper tackles these two shortcomings by proposing an approach to exploit reach-ability to reason on imperative data-aware process models and possibly incomplete process executions. The contribution of this paper is twofold: first, it formulates the trace completion as a reachability problem over data-aware models and second, it provides a rigorous mapping between our data-aware models and three important paradigms for reasoning about dynamic systems, namely Action Languages, Classical Planning, and Model-Checking. This allows us to exploit and extensively evaluate the available tools for the above paradigms to solve the trace repair problem. The rigorous encoding of our data-aware models, based on a common interpretation of the semantics of Action Languages, Classical Planning, and Model-Checking in terms of transition systems, paired with a first comprehensive assessment of the performances of their tools in computing reachability for data-aware workflow net languages, provide a solid contribution to advancing the state-of-the-art on the concrete exploitation of formal verification techniques on business processes.