In theory, logic-based AI is explainable by design, since all inferences can be explained using logical proofs or counterexamples. In practice, which inferences performed by an automated reasoner c...

In equational reasoning, congruence closure is known for being a semi-decision procedure that’s efficient in practice. Equality saturation can be seen as an extension of congruence closure that all...

In the setting of fair allocation of indivisible goods, there are various desiderata that one might want from an allocation. Two important ones are envy-freeness and Pareto efficiency. In general, ...

The ongoing AI revolution raises many questions. Are the current large language models intelligent? Are they becoming super intelligent? What is the role, if any, of logic in the current AI? Wh...

“Multi-agent pathfinding”, also called “pebble motion on graphs” or “cooperative pathfinding”, is the problem of deciding the existence of or generating a collision-free movement plan for a set of ...

Decision trees are an effective and concise way of conveying information, easily understood by virtually everyone regardless of the topic. Given the recent interest in explainable AI and related fi...

Graph neural networks (GNNs) are the predominant architectures for a variety of learning tasks on graphs. We present a new angle on the expressive power of GNNs by studying how the predictions of a...

Nash equilibria have been central to game theory since Von Neumann, but how fast can we compute them? The best known upper bound is achieved by letting a minimizing and a maximizing online learning...

Temporal logics have become essential tools of many AI applications, from verification to planning to synthesis. Mission-time Linear Temporal Logic (MLTL) adds closed-interval integer bounds on the...

In this talk I discuss how estimating and propagating epistemic uncertainty benefits generalization and deep exploration in reinforcement learning (RL) by focusing on two recent contributions. Fir...

In recent years there has been a growing interest in studying graph theoretical structures used for designing efficient algorithms in various computational models, such as dynamic, parallel and dis...

Judgment aggregation (JA) offers a generic formal logical framework for modeling various settings where agents must reach joint agreements through aggregating the preferences, judgments, or beliefs...

It is known that without synchronization via a global clock one cannot obtain common knowledge by communication. Moreover, it is folklore that without exchanging higher-level information arbitrary ...

One problem to solve in the context of information fusion, decision-making, and other artificial intelligence challenges is to compute justified beliefs based on evidence. In real-life examples, th...

The research area of computational social choice deals with the application of techniques from computer science and AI to the design and analysis of economic mechanisms for collective decision maki...

Supervisory Control Theory, initiated by Ramadge and Wonham, automatically transforms a formal system model and its safety requirements into a (minimally) restricted system that satisfies all safet...

Corruption in auctions, where an auctioneer engages in bid rigging with one (or several) of the bidders, occurs rather frequently in practice, especially in the public sector (e.g., in constructi...

Examples can be a useful tool when a formal specification must be synthesized or communicated. They sometimes provide a more convenient medium for communication than the formal specification itsel...

(or how to be fair to deceptive egoists.) When allocating indivisible goods to a number of selfish agents, both fairness and truthfulness are main concerns: the allocation should guarantee everyon...

Planning models are usually defined in lifted, i.e., first order formalisms, while most solvers need (variable-free) grounded representations. Though techniques for grounding prune unnecessary part...