Collaborating Authors

Logic & Formal Reasoning

Incremental Event Calculus for Run-Time Reasoning

Journal of Artificial Intelligence Research

We present a system for online, incremental composite event recognition. In streaming environments, the usual case is for data to arrive with a (variable) delay from, and to be revised by, the underlying sources. We propose RTECinc, an incremental version of RTEC, a composite event recognition engine with formal, declarative semantics, that has been shown to scale to several real-world data streams. RTEC deals with delayed arrival and revision of events by computing all queries from scratch. This is often inefficient since it results in redundant computations. Instead, RTECinc deals with delays and revisions in a more efficient way, by updating only the affected queries. We examine RTECinc theoretically, presenting a complexity analysis, and show the conditions in which it outperforms RTEC. Moreover, we compare RTECinc and RTEC experimentally using real-world and synthetic datasets. The results are compatible with our theoretical analysis and show that RTECinc outperforms RTEC in many practical cases.

Approximating Perfect Recall when Model Checking Strategic Abilities: Theory and Applications

Journal of Artificial Intelligence Research

The model checking problem for multi-agent systems against specifications in the alternating-time temporal logic ATL, hence ATL∗, under perfect recall and imperfect information is known to be undecidable. To tackle this problem, in this paper we investigate a notion of bounded recall under incomplete information. We present a novel three-valued semantics for ATL∗ in this setting and analyse the corresponding model checking problem. We show that the three-valued semantics here introduced is an approximation of the classic two-valued semantics, then give a sound, albeit partial, algorithm for model checking two-valued perfect recall via its approximation as three-valued bounded recall. Finally, we extend MCMAS, an open-source model checker for ATL and other agent specifications, to incorporate bounded recall; we illustrate its use and present experimental results.

Solving (Some) Formal Math Olympiad Problems


We built a neural theorem prover for Lean that learned to solve a variety of challenging high-school olympiad problems, including problems from the AMC12 and AIME competitions, as well as two problems adapted from the IMO.[1] The prover uses a language model to find proofs of formal statements. Each time we find a new proof, we use it as new training data, which improves the neural network and enables it to iteratively find solutions to harder and harder statements. We achieved a new state-of-the-art (41.2% vs 29.3%) on the miniF2F benchmark, a challenging collection of high-school olympiad problems. Our approach, which we call statement curriculum learning, consists of manually collecting a set of statements of varying difficulty levels (without proof) where the hardest statements are similar to the benchmark we target.

What is Neural-Symbolic Integration?


Historically, the two encompassing streams of symbolic and sub-symbolic stances to AI evolved in a largely separate manner, with each camp focusing on selected narrow problems of their own. Originally, researchers favored the discrete, symbolic approaches towards AI, targeting problems ranging from knowledge representation, reasoning, and planning to automated theorem proving. While the particular techniques in symbolic AI varied greatly, the field was largely based on mathematical logic, which was seen as the proper ("neat") representation formalism for most of the underlying concepts of symbol manipulation. With this formalism in mind, people used to design large knowledge bases, expert and production rule systems, and specialized programming languages for AI. These symbolic logic representations have then also been commonly used in the machine learning (ML) sub-domain, particularly in the form of Inductive Logic Programming (discussed in the previous article), which introduced the powerful ability to incorporate background knowledge into learning models and algorithms. Amongst the main advantages of this logic-based approach towards ML have been the transparency to humans, deductive reasoning, inclusion of expert knowledge, and structured generalization from small data.

PRIMA: Planner-Reasoner Inside a Multi-task Reasoning Agent Artificial Intelligence

We consider the problem of multi-task reasoning (MTR), where an agent can solve multiple tasks via (first-order) logic reasoning. This capability is essential for human-like intelligence due to its strong generalizability and simplicity for handling multiple tasks. However, a major challenge in developing effective MTR is the intrinsic conflict between reasoning capability and efficiency. An MTR-capable agent must master a large set of "skills" to tackle diverse tasks, but executing a particular task at the inference stage requires only a small subset of immediately relevant skills. How can we maintain broad reasoning capability and also efficient specific-task performance? To address this problem, we propose a Planner-Reasoner framework capable of state-of-the-art MTR capability and high efficiency. The Reasoner models shareable (first-order) logic deduction rules, from which the Planner selects a subset to compose into efficient reasoning paths. The entire model is trained in an end-to-end manner using deep reinforcement learning, and experimental studies over a variety of domains validate its effectiveness.

Quantification and aggregation over concepts of the ontology Artificial Intelligence

The first phase of developing an intelligent system is the selection of an ontology of symbols representing relevant concepts of the application domain. These symbols are then used to represent the knowledge of the domain. This representation should be \emph{elaboration tolerant}, in the sense that it should be convenient to modify it to take into account new knowledge or requirements. Unfortunately, current formalisms require a significant rewrite of that representation when the new knowledge is about the \emph{concepts} themselves: the developer needs to "\emph{reify}" them. This happens, for example, when the new knowledge is about the number of concepts that satisfy some conditions. The value of expressing knowledge about concepts, or "intensions", has been well-established in \emph{modal logic}. However, the formalism of modal logic cannot represent the quantifications and aggregates over concepts that some applications need. To address this problem, we developed an extension of first order logic that allows referring to the \emph{intension} of a symbol, i.e., to the concept it represents. We implemented this extension in IDP-Z3, a reasoning engine for FO($\cdot$) (aka FO-dot), a logic-based knowledge representation language. This extension makes the formalism more elaboration tolerant, but also introduces the possibility of syntactically incorrect formula. Hence, we developed a guarding mechanism to make formula syntactically correct, and a method to verify correctness. The complexity of this method is linear with the length of the formula. This paper describes these extensions, how their relate to intensions in modal logic and other formalisms, and how they allowed representing the knowledge of four different problem domains in an elaboration tolerant way.

Answer Set Planning: A Survey Artificial Intelligence

Answer Set Planning refers to the use of Answer Set Programming (ASP) to compute plans, i.e., solutions to planning problems, that transform a given state of the world to another state. The development of efficient and scalable answer set solvers has provided a significant boost to the development of ASP-based planning systems. This paper surveys the progress made during the last two and a half decades in the area of answer set planning, from its foundations to its use in challenging planning domains. The survey explores the advantages and disadvantages of answer set planning. It also discusses typical applications of answer set planning and presents a set of challenges for future research.

Learning Temporal Rules from Noisy Timeseries Data Artificial Intelligence

Events across a timeline are a common data representation, seen in different temporal modalities. Individual atomic events can occur in a certain temporal ordering to compose higher level composite events. Examples of a composite event are a patient's medical symptom or a baseball player hitting a home run, caused distinct temporal orderings of patient vitals and player movements respectively. Such salient composite events are provided as labels in temporal datasets and most works optimize models to predict these composite event labels directly. We focus on uncovering the underlying atomic events and their relations that lead to the composite events within a noisy temporal data setting. We propose Neural Temporal Logic Programming (Neural TLP) which first learns implicit temporal relations between atomic events and then lifts logic rules for composite events, given only the composite events labels for supervision. This is done through efficiently searching through the combinatorial space of all temporal logic rules in an end-to-end differentiable manner. We evaluate our method on video and healthcare datasets where it outperforms the baseline methods for rule discovery.


AAAI Conferences

Temporal logics can be used in reasoning about actions for specifying constraints on domain descriptions and temporal properties to be verified. In this paper, we exploit Bounded Model Checking (BMC) techniques in the verification of Dynamic Linear Time Temporal Logic (DLTL) properties of an action theory, which is formulated in a temporal extension of Answer Set Programming (ASP). To achieve completeness, we propose an approach to BMC which exploits the Buechi automaton construction while searching for a counterexample. We provide an encoding in ASP of the temporal action domain and of Bounded Model Checking of DLTL formulas.


AAAI Conferences

The paper introduces a worst-case optimal tableau algorithm for reasoning with Forest Logic Programs, a decidable fragment of Open Answer Set Programming. FoLPs are a useful device for tight integration of the Description Logic and the Logic Programming worlds: reasoning with the DL SHOQ can be simulated within the fragment. The algorithm reuses a knowledge compilation technique previously introduced, but improves on previous results by decreasing the worst-case running time with one exponential level. The decrease in complexity is due to the usage in conjunction of a new redundancy and of a new caching rule.