Logic & Formal Reasoning
A Rational Entailment for Expressive Description Logics via Description Logic Programs
Casini, Giovanni, Straccia, Umberto
Lehmann and Magidor's rational closure is acknowledged as a landmark in the field of non-monotonic logics and it has also been re-formulated in the context of Description Logics (DLs). We show here how to model a rational form of entailment for expressive DLs, such as SROIQ, providing a novel reasoning procedure that compiles a non-monotone DL knowledge base into a description logic program (dl-program).
Modeling and Reasoning in Event Calculus using Goal-Directed Constraint Answer Set Programming
Arias, Joaquรญn, Carro, Manuel, Chen, Zhuo, Gupta, Gopal
Automated commonsense reasoning is essential for building human-like AI systems featuring, for example, explainable AI. Event Calculus (EC) is a family of formalisms that model commonsense reasoning with a sound, logical basis. Previous attempts to mechanize reasoning using EC faced difficulties in the treatment of the continuous change in dense domains (e.g., time and other physical quantities), constraints among variables, default negation, and the uniform application of different inference methods, among others. We propose the use of s(CASP), a query-driven, top-down execution model for Predicate Answer Set Programming with Constraints, to model and reason using EC. We show how EC scenarios can be naturally and directly encoded in s(CASP) and how it enables deductive and abductive reasoning tasks in domains featuring constraints involving both dense time and dense fluents.
Formal Software Verification Measures Up
The modern world runs on software. However, there is a catch: computer code often contains programming errors--some small, some large. These glitches can lead to unexpected results--and systematic failures. "In many cases, software flaws don't make any difference. In other cases, they can cause massive problems," says Kathleen Fisher, professor and chair of the computer science department at Tufts University and a former official of the U.S. Defense Advanced Research Projects Agency (DARPA).
Program Verification
In 1969, Tony Hoare published a classical Communications' article, "An Axiomatic Basis for Computer Programming." Hoare's article culminated a sequence of works by Turing, McCarthy, Wirth, Floyd, and Manna, whose essence is an association of a proposition with each point in the program control flow, where the proposition is asserted to hold whenever that point is reach. Hoare added two important elements to that approach. First, he described a formal logic, now called Hoare Logic, for reasoning about programs. Second, he offered a compelling vision for the program-verification project: "When the correctness of a program, its compiler, and the hardware of the computer have all been established with mathematical certainty, it will be possible to place great reliance on the results of the program, and predict their properties with a confidence limited only by the reliability of the electronics."
Knowing How to Plan
Standard Epistemic Logic (EL) mainly studies reasoning patterns of knowing that ฯ, despite early contributions by Hintikka on formulating other know-wh expressions such as knowing who and why using first-order and higher-order modal logic. In recent years, there is a resurgence of interest on epistemic logics of know-wh powered by the new techniques for fragments of firstorder modal logic based on the so-called bundle modalities packing a quantifier and a normal epistemic modality together [26, 24, 21]. Within the varieties of logics of know-wh, the logics of know-how received the most attention in AI (cf.
Querying in the Age of Graph Databases and Knowledge Graphs
Arenas, Marcelo, Gutierrez, Claudio, Sequeda, Juan F.
Graphs have become the best way we know of representing knowledge. The computing community has investigated and developed the support for managing graphs by means of digital technology. Graph databases and knowledge graphs surface as the most successful solutions to this program. This tutorial will provide a conceptual map of the data management tasks underlying these developments, paying particular attention to data models and query languages for graphs.
Defeasible Reasoning via Datalog$^\neg$
Hardware architectures can range from the use of GPUs and other hardware accelerators, through multi-core multi-threaded architectures, to shared-nothing cloud computing. Causes for failure to exploit these architectures include lack of expertise in the architectural features, lack of manpower more generally, and difficulty in updating legacy systems. Such problems can be ameliorated by mapping a logic to logic programming as an intermediate language. This is a common strategy in the implementation of defeasible logics. The first implementation of a defeasible logic, d-Prolog, was implemented as a Prolog meta-interpreter (Covington et al. 1997). Courteous Logic Programs (Grosof 1997) and its successors LPDA (Wan et al. 2009), Rulelog (Grosof and Kifer 2013), Flora2 (Kifer et al. 2018), are implemented in XSB (Swift and Warren 2012).
MILP, pseudo-boolean, and OMT solvers for optimal fault-tolerant placements of relay nodes in mission critical wireless networks
Chen, Quian Matteo, Finzi, Alberto, Mancini, Toni, Melatti, Igor, Tronci, Enrico
In critical infrastructures like airports, much care has to be devoted in protecting radio communication networks from external electromagnetic interference. Protection of such mission-critical radio communication networks is usually tackled by exploiting radiogoniometers: at least three suitably deployed radiogoniometers, and a gateway gathering information from them, permit to monitor and localise sources of electromagnetic emissions that are not supposed to be present in the monitored area. Typically, radiogoniometers are connected to the gateway through relay nodes. As a result, some degree of fault-tolerance for the network of relay nodes is essential in order to offer a reliable monitoring. On the other hand, deployment of relay nodes is typically quite expensive. As a result, we have two conflicting requirements: minimise costs while guaranteeing a given fault-tolerance. In this paper, we address the problem of computing a deployment for relay nodes that minimises the relay node network cost while at the same time guaranteeing proper working of the network even when some of the relay nodes (up to a given maximum number) become faulty (fault-tolerance). We show that, by means of a computation-intensive pre-processing on a HPC infrastructure, the above optimisation problem can be encoded as a 0/1 Linear Program, becoming suitable to be approached with standard Artificial Intelligence reasoners like MILP, PB-SAT, and SMT/OMT solvers. Our problem formulation enables us to present experimental results comparing the performance of these three solving technologies on a real case study of a relay node network deployment in areas of the Leonardo da Vinci Airport in Rome, Italy.
Score-Based Explanations in Data Management and Machine Learning: An Answer-Set Programming Approach to Counterfactual Analysis
We describe some recent approaches to score-based explanations for query answers in databases and outcomes from classification models in machine learning. The focus is on work done by the author and collaborators. Special emphasis is placed on declarative approaches based on answer-set programming to the use of counterfactual reasoning for score specification and computation. Several examples that illustrate the flexibility of these methods are shown.
Leveraging Language to Learn Program Abstractions and Search Heuristics
Wong, Catherine, Ellis, Kevin, Tenenbaum, Joshua B., Andreas, Jacob
Inductive program synthesis, or inferring programs from examples of desired behavior, offers a general paradigm for building interpretable, robust, and generalizable machine learning systems. Effective program synthesis depends on two key ingredients: a strong library of functions from which to build programs, and an efficient search strategy for finding programs that solve a given task. We introduce LAPS (Language for Abstraction and Program Search), a technique for using natural language annotations to guide joint learning of libraries and neurally-guided search models for synthesis. When integrated into a state-of-the-art library learning system (DreamCoder), LAPS produces higher-quality libraries and improves search efficiency and generalization on three domains -- string editing, image composition, and abstract reasoning about scenes -- even when no natural language hints are available at test time.