A cornerstone of Shannon's famous information theory is the idea of decoupling the meaning of a message from its efficient transmission. In this article, we propose an extension of Shannon's communication model where the sender and receiver are assumed to have reasoning capabilities. In such a setting, we gain insights by coupling the fields of information theory and mathematical logic. Under the assumption that a message is coming from a stochastic source, Shannon's theory establishes that the fundamental compression limit is the entropy of the source. Imagine, however, that we were not interested in the message itself, but rather, we were focused on the logical conclusions that one could derive from it. In this work, we obtain a closed-form expression for a fundamental compression limit in the presence of reasoning capabilities. Our expression is valid under various assumptions about what the sender and receiver know, providing initial answers to key questions such as how much the fundamental limit varies as one narrows or widens the amount of knowledge that is being transferred from sender to receiver, or how, surprisingly, such a fundamental limit remains the same even if the sender is unaware of what it is that a receiver already knows. We also offer practical algorithms that are empirically demonstrated to be significantly more efficient than alternatives that do not account for the existence of reasoning capabilities.

In 1893, James Joseph Sylvester posed the following problem: given n points in the plane, not all collinear, must there be a line determined by two of the points that does not pass through any of the other points? In 1940, Eberhard Melchior studied the equivalent dual problem in the projective plane: given a set of n lines in the (real) projective plane, not all passing through a common point, must there be a point where exactly two of the lines intersect? Such a point of intersection is called an *ordinary point*. Via a clever double-counting argument, Melchior found that in fact there must be at least three such points. Given the many simple "visual" proofs of what is today known as the Sylvester-Gallai Theorem — the theorem that states there must be at least one ordinary point — a natural question is whether there is a simple visual proof that recovers all three of Melchior's ordinary points. This paper provides such a proof.

Machine-assisted methods for discovering physical laws from background theory and data have recently emerged, promising to advance our understanding of the physical world. However, training and benchmarking these systems remains challenging: real physical theories are limited in number. To address this need, we introduce SynPAT, a system for generating synthetic physical theories with accompanying data. SynPAT produces: (i) a consistent set of axioms forming a synthetic theory, (ii) a symbolic consequence of these axioms representing the discovery target, and (iii) noisy data approximating this consequence. Crucially, to mirror historically incorrect theories (e.g., Newtonian mechanics before Special Relativity), SynPAT can also generate theories whose axioms do not strictly entail, and in fact conflict with, the observed consequence, requiring a correction to the assumed axioms to bridge the gap. We detail SynPAT's methodology and benchmark several open-source symbolic regression systems on our generated theories and data.

Information theory has provided foundations for the theories of several application areas critical for modern society, including communications, computer storage, and AI. A key aspect of Shannon's 1948 theory is a sharp lower bound on the number of bits needed to encode and communicate a string of symbols. When he introduced the theory, Shannon famously excluded any notion of semantics behind the symbols being communicated. This semantics-free notion went on to have massive impact on communication and computing technologies, even as multiple proposals for reintroducing semantics in a theory of information were being made, notably one where Carnap and Bar-Hillel used logic and reasoning to capture semantics. In this paper we present, for the first time, a Shannon-style analysis of a communication system equipped with a deductive reasoning capability, implemented using logical inference. We use some of the most important techniques developed in information theory to demonstrate significant and sometimes surprising gains in communication efficiency availed to us through such capability, demonstrated also through practical codes. We thus argue that proposals for a semantic information theory should include the power of deductive reasoning to magnify the value of transmitted bits as we strive to fully unlock the inherent potential of semantics.

Combinatorial games played between two players, called Spoiler and Duplicator, have often been used to capture syntactic properties of formal logical languages. For instance, the widely used Ehrenfeucht-Fraïssé (EF) game captures the syntactic measure of quantifier rank of first-order formulas. For every such game, there is an associated natural decision problem: "given an instance of the game, does Spoiler win the game on that instance?" For EF games, this problem was shown to be PSPACE-complete by Pezzoli in 1998. In this present paper, we show that the same problem for the *multi-structural* (MS) games of recent interest is PSPACE-hard, but contained in NEXPTIME. In the process, we also resolve an open problem posed by Pezzoli about the dependence of the hardness results for EF games on the arity of the schema under consideration. Our techniques combine adaptations of Pezzoli's constructions together with insights from the theory of inapproximability of optimization problems, as well as the recently developed technique of parallel play for MS games.

We study multi-structural games, played on two sets ${\mathcal{A}}$ and ${\mathcal{B}}$ of structures. These games generalize Ehrenfeucht-Fraïssé games. Whereas Ehrenfeucht-Fraïssé games capture the quantifier rank of a first-order sentence, multi-structural games capture the number of quantifiers, in the sense that Spoiler wins the r-round game if and only if there is a first-order sentence ϕ with at most r quantifiers, where every structure in ${\mathcal{A}}$ satisfies ϕ and no structure in ${\mathcal{B}}$ satisfies ϕ. We use these games to give a complete characterization of the number of quantifiers required to distinguish linear orders of different sizes, and develop machinery for analyzing structures beyond linear orders.

The number of quantifiers needed to express first-order properties is captured by two-player combinatorial games called multi-structural (MS) games. We play these games on linear orders and strings, and introduce a technique we call "parallel play", that dramatically reduces the number of quantifiers needed in many cases. Linear orders and strings are the most basic representatives of ordered structures -- a class of structures that has historically been notoriously difficult to analyze. Yet, in this paper, we provide upper bounds on the number of quantifiers needed to characterize different-sized subsets of these structures, and prove that they are tight up to constant factors, including, in some cases, up to a factor of $1+\varepsilon$, for arbitrarily small $\varepsilon$.

Multi-agent reinforcement learning (MARL) is well-suited for runtime decision-making in optimizing the performance of systems where multiple agents coexist and compete for shared resources. However, applying common deep learning-based MARL solutions to real-world problems suffers from issues of interpretability, sample efficiency, partial observability, etc. To address these challenges, we present an event-driven formulation, where decision-making is handled by distributed co-operative MARL agents using neuro-symbolic methods. The recently introduced neuro-symbolic Logical Neural Networks (LNN) framework serves as a function approximator for the RL, to train a rules-based policy that is both logical and interpretable by construction. To enable decision-making under uncertainty and partial observability, we developed a novel probabilistic neuro-symbolic framework, Probabilistic Logical Neural Networks (PLNN), which combines the capabilities of logical reasoning with probabilistic graphical models. In PLNN, the upward/downward inference strategy, inherited from LNN, is coupled with belief bounds by setting the activation function for the logical operator associated with each neural network node to a probability-respecting generalization of the Fr\'echet inequalities. These PLNN nodes form the unifying element that combines probabilistic logic and Bayes Nets, permitting inference for variables with unobserved states. We demonstrate our contributions by addressing key MARL challenges for power sharing in a system-on-chip application.

The number of quantifiers needed to express first-order (FO) properties is captured by two-player combinatorial games called multi-structural games. We analyze these games on binary strings with an ordering relation, using a technique we call parallel play, which significantly reduces the number of quantifiers needed in many cases. Ordered structures such as strings have historically been notoriously difficult to analyze in the context of these and similar games. Nevertheless, in this paper, we provide essentially tight upper bounds on the number of quantifiers needed to characterize different-sized subsets of strings. The results immediately give bounds on the number of quantifiers necessary to define several different classes of Boolean functions. One of our results is analogous to Lupanov's upper bounds on circuit size and formula size in propositional logic: we show that every Boolean function on n-bit inputs can be defined by a FO sentence having (1 + ε)nlog(n) + O(1) quantifiers, and that this is essentially tight. We reduce this number to (1 + ε)log(n) + O(1) when the Boolean function in question is sparse.

Multi-structural (MS) games are combinatorial games that capture the number of quantifiers of first-order sentences. On the face of their definition, MS games differ from Ehrenfeucht-Fraisse (EF) games in two ways: first, MS games are played on two sets of structures, while EF games are played on a pair of structures; second, in MS games, Duplicator can make any number of copies of structures. In the first part of this paper, we perform a finer analysis of MS games and develop a closer comparison of MS games with EF games. In particular, we point out that the use of sets of structures is of the essence and that when MS games are played on pairs of structures, they capture Boolean combinations of first-order sentences with a fixed number of quantifiers. After this, we focus on another important difference between MS games and EF games, namely, the necessity for Spoiler to play on top of a previous move in order to win some MS games. Via an analysis of the types realized during MS games, we delineate the expressive power of the variant of MS games in which Spoiler never plays on top of a previous move. In the second part we focus on simultaneously capturing number of quantifiers and number of variables in first-order logic. We show that natural variants of the MS game do *not* achieve this. We then introduce a new game, the quantifier-variable tree game, and show that it simultaneously captures the number of quantifiers and number of variables. We conclude by generalizing this game to a family of games, the *syntactic games*, that simultaneously capture reasonable syntactic measures and the number of variables.

Today, the vast majority of the world's digital information is represented using the fundamental assumption, introduced by Claude Shannon in 1948, that ``...the semantic aspects of communication are irrelevant to the engineering problem (of the design of communication systems)...''. Consider, nonetheless, the observation that we often combine a message with other information in order to deduce new facts, thereby expanding the value of such a message. It is noteworthy that to-date, no rigorous theory of communication has been put forth which postulates the existence of deductive capabilities on the receiver's side. The purpose of this paper is to present such a theory. We formally model such deductive capabilities using logic reasoning, and present a rigorous theory which covers the following generic scenario: Alice and Bob each have knowledge of some logic sentence, and they wish to communicate as efficiently as possible with the shared goal that, following their communication, Bob should be able to deduce a particular logic sentence that Alice knows to be true, but that Bob currently cannot prove. Many variants of this general setup are considered in this article; in all cases we are able to provide sharp upper and lower bounds. Our contribution includes the identification of the most fundamental requirements that we place on a logic and associated logical language for all of our results to apply. Practical algorithms that are in some cases asymptotically optimal are provided, and we illustrate the potential practical value of the design of communication systems that incorporate the assumption of deductive capabilities at the receiver using experimental results that suggest significant possible gains compared to classical systems.

We study a family of line segment visibility problems, related to classical art gallery problems, which are motivated by monitoring requirements in commercial data centers. Given a collection of non-overlapping line segments in the interior of a rectangle, and a requirement to monitor the segments from one side or the other, we examine the problem of finding a minimal set of point guards. Guards may be placed anywhere in the interior of the rectangle but not on a line segment. We consider combinatorial bounds of problem variants where the problem solver gets to decide which side of the segments to guard or the problem poser gets to decide which side to guard, and many others. We show that virtually all variants are NP-Hard to solve exactly, and then provide heuristics and experimental results to give insight into the associated practical problems. Finally we describe a program for using experiments to guide the search for optimal combinatorial bounds.

In 1981, Neil Immerman described a two-player game, which he called the "separability game" \cite{Immerman81}, that captures the number of quantifiers needed to describe a property in first-order logic. Immerman's paper laid the groundwork for studying the number of quantifiers needed to express properties in first-order logic, but the game seemed to be too complicated to study, and the arguments of the paper almost exclusively used quantifier rank as a lower bound on the total number of quantifiers. However, last year Fagin, Lenchner, Regan and Vyas rediscovered the games, provided some tools for analyzing them, and showed how to utilize them to characterize the number of quantifiers needed to express linear orders of different sizes. In this paper, we push forward in the study of number of quantifiers as a bona fide complexity measure by establishing several new results. First we carefully distinguish minimum number of quantifiers from the more usual descriptive complexity measures, minimum quantifier rank and minimum number of variables. Then, for each positive integer $k$, we give an explicit example of a property of finite structures (in particular, of finite graphs) that can be expressed with a sentence of quantifier rank $k$, but where the same property needs $2^{\Omega (k^2)}$ quantifiers to be expressed.

Epistemic Planning (EP) refers to an automated planning setting where the agent reasons in the space of knowledge states and tries to find a plan to reach a desirable state from the current state. Its general form, the Multi-agent Epistemic Planning (MEP) problem involves multiple agents who need to reason about both the state of the world and the information flow between agents. In a MEP problem, multiple approaches have been developed recently with varying restrictions, such as considering only the concept of knowledge while not allowing the idea of belief, or not allowing for “complex” modal operators such as those needed to handle dynamic common knowledge. While the diversity of approaches has led to a deeper understanding of the problem space, the lack of a standardized way to specify MEP problems independently of solution approaches has created difficulties in comparing performance of planners, identifying promising techniques, exploring new strategies like ensemble methods, and making it easy for new researchers to contribute to this research area. To address the situation, we propose a unified way of specifying EP problems the Epistemic Planning Domain Definition Language, E-PDDL. We show that EPPDL can be supported by leading MEP planners and provide corresponding parser code that translates EP problems specified in E-PDDL into (M)EP problems that can be handled by several planners. This work is also useful in building more general epistemic planning environments where we envision a meta-cognitive module that takes a planning problem in E-PDDL, identifies and assesses some of its features, and autonomously decides which planner is the best one to solve it.

This paper proposes a research direction to advance AI which draws inspiration from cognitive theories of human decision making. The premise is that if we gain insights about the causes of some human capabilities that are still lacking in AI (for instance, adaptability, generalizability, common sense, and causal reasoning), we may obtain similar capabilities in an AI system by embedding these causal components. We hope that the high-level description of our vision included in this paper, as well as the several research questions that we propose to consider, can stimulate the AI research community to define, try and evaluate new methodologies, frameworks, and evaluation metrics, in the spirit of achieving a better understanding of both human and machine intelligence.

There is a problem with the foundations of classical mathematics, and potentially even with the foundations of computer science, that mathematicians have by-and-large ignored. This essay is a call for practicing mathematicians who have been sleep-walking in their infinitary mathematical paradise to take heed. Much of mathematics relies upon either (i) the "existence'" of objects that contain an infinite number of elements, (ii) our ability, "in theory", to compute with an arbitrary level of precision, or (iii) our ability, "in theory", to compute for an arbitrarily large number of time steps. All of calculus relies on the notion of a limit. The monumental results of real and complex analysis rely on a seamless notion of the "continuum" of real numbers, which extends in the plane to the complex numbers and gives us, among other things, "rigorous" definitions of continuity, the derivative, various different integrals, as well as the fundamental theorems of calculus and of algebra -- the former of which says that the derivative and integral can be viewed as inverse operations, and the latter of which says that every polynomial over $\mathbb{C}$ has a complex root. This essay is an inquiry into whether there is any way to assign meaning to the notions of "existence" and "in theory'" in (i) to (iii) above.

We present a generalization of the marriage problem underlying Hall's famous Marriage Theorem to what we call the Symmetric Marriage Problem, a problem that can be thought of as a special case of Maximal Weighted Bipartite Matching. We show that there is a solution to the Symmetric Marriage Problem if and only if a variation on Hall's Condition holds on each of the bipartitions. We prove both finite and infinite versions of this result and provide applications. We also introduce a non-bipartite version of the problem and show that a generalization of Tutte's Theorem applies.

Motivated by the application of Hall's Marriage Theorem in various LP-rounding problems, we introduce a generalization of the classical marriage problem (CMP) that we call the Fractional Marriage Problem. We show that the Fractional Marriage Problem is NP-Complete by reduction from Boolean Satisfiability (SAT). We show that when we view the classical marriage problem (a.k.a. bipartite matching) as a sub-class of SAT we get a new class of polynomial-time satisfiable SAT instances that we call CMP-SAT, different from the classically known polynomial-time satisfiable SAT instances 2-SAT, Horn-SAT and XOR-SAT. We next turn to the problem of recognizing CMP-SAT instances, first using SAT embeddings, and then using their embeddings within the universe of Fractional Marriage Problems (FMPs). In the process we are led to another generalization of the CMP that we call the Symmetric Marriage Problem, which is polynomial time decidable and leads to a slight enlargement of the CMP-SAT class. We develop a framework for simplifying FMP problems to identify CMP instances that we call Fragment Logic. Finally we give a result that sheds light on how expressive the FMP need be to still be NP-Complete. The result gives a second NP-Complete reduction of the FMP, this time to Tripartite Matching. We conclude with a wide assortment of suggested additional problems.