Thank you for pointing out the issue, we'll add more discussion in the revision.

Neural networks excel at pattern recognition but struggle with reliable logical reasoning, often violating basic logical principles during inference. We address this limitation by developing a categorical framework that systematically constructs neural architectures with provable logical guarantees. Our approach treats logical theories as algebraic structures called Lawvere theories, which we transform into neural networks using categorical algebra in the 2-category of parametric maps. Unlike existing methods that impose logical constraints during training, our categorical construction embeds logical principles directly into the network's architectural structure, making logical violations mathematically impossible. We demonstrate this framework by constructing differentiable neural architectures for propositional logic that preserve boolean reasoning while remaining trainable via gradient descent. Our main theoretical result establishes a bijective correspondence between finitary logical theories and neural architectures, proving that every logically constrained network arises uniquely from our construction. This extends Categorical Deep Learning beyond geometric symmetries to semantic constraints, enabling automatic derivation of verified architectures from logical specifications. The framework provides mathematical foundations for trustworthy AI systems, with applications to theorem proving, formal verification, and safety-critical reasoning tasks requiring verifiable logical behavior.

Still, if you can do some version of the Mayan hieroglyphics, or work that example into the introduction, it would improve the paper even more. They restrict themselves to classification problems, i.e., a mapping from perceptual input to {0,1}; the discrete symbols output by the perception model act as latent variables sitting in between the input and the binary decision. Their approach is to alternate between (1) inferring a logic program consistent with the training examples, conditioned on the output of the perception model, and (2) training the perception model to predict the latent discrete symbols. Because the perception model may be unreliable, particularly early on in training, the logic program is allowed to revise or abduce the outputs of perception. The problem they pose -- integrating learned perception with learned symbolic reasoning -- is eminently important.

The field of Explainable AI (XAI) is seeking to shed light on the inner workings of complex AI models and uncover the rationale behind their decisions. One of the models gaining attention are probabilistic circuits (PCs), which are a general and unified framework for tractable probabilistic models that support efficient computation of various probabilistic queries. Probabilistic circuits guarantee inference that is polynomial in the size of the circuit. In this paper, we improve the explainability of probabilistic circuits by computing a comprehensible, readable logical theory that covers the high-density regions generated by a PC. To achieve this, pruning approaches based on generative significance are used in a new method called PUTPUT (Probabilistic circuit Understanding Through Pruning Underlying logical Theories). The method is applied to a real world use case where music playlists are automatically generated and expressed as readable (database) queries. Evaluation shows that this approach can effectively produce a comprehensible logical theory that describes the high-density regions of a PC and outperforms state of the art methods when exploring the performance-comprehensibility trade-off.

Ontic necessities are those modalities universally quantifying over domains of ontic possibilities, whose ``existence'' is independent of our knowledge. An ontic necessity, called the weak ontic necessity, causes interesting questions. An example for it is ``I should be dead by now''. A feature of this necessity is whether it holds at a state has nothing to do with whether its prejacent holds at the state. Is there a weak epistemic necessity expressed by ``should''? Is there a strong ontic necessity expressed by ``must''? How do we make sense of the strong and weak ontic necessities formally? In this paper, we do the following work. Firstly, we recognize strong/weak ontic/epistemic necessities and give our general ideas about them. Secondly, we present a complete logical theory for the strong and weak ontic necessities in branching time. This theory is based on the following approach. The weak ontic necessity quantifies over a domain of expected timelines, determined by the agent's system of ontic rules. The strong ontic necessity quantifies over a domain of accepted timelines, determined by undefeatable ontic rules.

Human beliefs change, but so do the concepts that underpin them. The recent Abduction, Belief Revision and Conceptual Change (ABC) repair system combines several methods from automated theory repair to expand, contract, or reform logical structures representing conceptual knowledge in artificial agents. In this paper we focus on conceptual change: repair not only of the membership of logical concepts, such as what animals can fly, but also concepts themselves, such that birds may be divided into flightless and flying birds, by changing the signature of the logical theory used to represent them. We offer a method for automatically evaluating entrenchment in the signature of a Datalog theory, in order to constrain automated theory repair to succinct and intuitive outcomes. Formally, signature entrenchment measures the inferential contributions of every logical language element used to express conceptual knowledge, i.e., predicates and the arguments, ranking possible repairs to retain valuable logical concepts and reject redundant or implausible alternatives. This quantitative measurement of signature entrenchment offers a guide to the plausibility of conceptual changes, which we aim to contrast with human judgements of concept entrenchment in future work.

Usage of automated controllers which make decisions on an environment are widespread and are often based on black-box models. We use Knowledge Compilation theory to bring explainability to the controller's decision given the state of the system. For this, we use simulated historical state-action data as input and build a compact and structured representation which relates states with actions. We implement this method in a Traffic Light Control scenario where the controller selects the light cycle by observing the presence (or absence) of vehicles in different regions of the incoming roads.

We present a computer-supported approach for the logical analysis and conceptual explicitation of argumentative discourse. Computational hermeneutics harnesses recent progresses in automated reasoning for higher-order logics and aims at formalizing natural-language argumentative discourse using flexible combinations of expressive non-classical logics. In doing so, it allows us to render explicit the tacit conceptualizations implicit in argumentative discursive practices. Our approach operates on networks of structured arguments and is iterative and two-layered. At one layer we search for logically correct formalizations for each of the individual arguments. At the next layer we select among those correct formalizations the ones which honor the argument's dialectic role, i.e. attacking or supporting other arguments as intended. We operate at these two layers in parallel and continuously rate sentences' formalizations by using, primarily, inferential adequacy criteria. An interpretive, logical theory will thus gradually evolve. This theory is composed of meaning postulates serving as explications for concepts playing a role in the analyzed arguments. Such a recursive, iterative approach to interpretation does justice to the inherent circularity of understanding: the whole is understood compositionally on the basis of its parts, while each part is understood only in the context of the whole (hermeneutic circle). We summarily discuss previous work on exemplary applications of human-in-the-loop computational hermeneutics in metaphysical discourse. We also discuss some of the main challenges involved in fully-automating our approach. By sketching some design ideas and reviewing relevant technologies, we argue for the technological feasibility of a highly-automated computational hermeneutics.

In 1992 Tom Gruber proposed the following definition "An ontology is a specification of a conceptualization" [4]. Several variants exist that usually add adjectives further describing the specification (e.g., "formal", "explicit") or the conceptualization (e.g., "shared") (see discussion of related work in Section 5). These definitions are not helpful because they violate one of the basic rules for good definitions: the defining statement (the definiens) should be clearer than the term that is defined (the definiendum). As long as "conceptualization" is murkier than "ontology", any attempt of defining "ontology" as a kind of "specification of a conceptualization" is an intellectual placebo: it makes us feel like it provides a better grasp of the nature of ontologies, but there is no intellectual progress, because it lacks explanatory value (see Section 2 for details). Given the difficulties in defining "ontology" one may come to the conclusion that a proper definition is not really needed.