Despite ample evidence that our concepts, our cognitive architecture, and mathematics itself are all deeply compositional, few models take advantage of this structure. We therefore propose a radically compositional approach to computational neuroscience, drawing on the methods of applied category theory. We describe how these tools grant us a means to overcome complexity and improve interpretability, and supply a rigorous common language for scientific modelling, analogous to the type theories of computer science. As a case study, we sketch how to translate from compositional narrative concepts to neural circuits and back again.

Standardization of solver input languages has been a main dr iver for the growth of several areas within knowledge representation and reasoning, fostering the exploitation in actual applications. In this document we present the ASP-Core-2 standard input language for Answer Set Programming, which h as been adopted in ASP Competition events since 2013. KEYWORDS: Answer Set Programming, Standard Language, Knowledge Rep resentation and Reasoning, Standardization 2 Calimeri et al. 1 Introduction The process of standardizing the input languages of solvers for knowledge representation and reasoning research areas has been of utmost importance for the growth o f the related research communities: this has been the case for, e.g., the CNF-DIMACS format for SA T, th en extended to describe input formats for Max-SA T and QBF problems, the OPB format for pseudo-Boolean problems, somehow at the intersection between the CNF-DIMACS format and the LP format for Integer L inear Programming, the XCSP3 format for CP solving, SMT -LIB format for SMT solving, and the STRIP S/ PDDL language for automatic planning. The availability of such common input languages have l ed to the development of e ffi cient solvers in di ff erent KR communities, through a series of solver competitio ns that have pushed the adoption of these standards. The availability of e ffi cient solvers, together with a presence of a common interfac e language, has helped the exploitation of these methodologies in appli cations. The same has happened for Answer Set Programming (ASP) (Brew ka et al. 2011), a well-known approach to knowledge representation and reasoning with root s in the areas of logic programming and nonmonotonic reasoning (Gelfond and Lifschitz 1991), through the development of the ASP-Core language (Calimeri et al. 2011). The first ASP-Core version was a rule-based language whose syntax stems from plain Datalog and Prolog, and was a conservative extension t o the non-ground case of the Core language adopted in the First ASP Competition held in 2002 during the D agstuhl Seminar "Nonmonotonic Reasoning, Answer Set Programming and Constraints"

An important class of decidable first-order logic fragments are those satisfying a guardedness condition, such as the guarded fragment (GF). Usually, decidability for these logics is closely linked to the tree-like model property - the fact that satisfying models can be taken to have tree-like form. Decision procedures for the guarded fragment based on the tree-like model property are difficult to implement. An alternative approach, based on restricting first-order resolution, has been proposed, and this shows more promise from the point of view of implementation. In this work, we connect the tree-like model property of the guarded fragment with the resolution-based approach. We derive efficient resolution-based rewriting algorithms that solve the Quantifier-Free Query Answering Problem under Guarded Tuple Generating Dependencies (GTGDs) and Disjunctive Guarded Tuple Generating Dependencies (DisGTGDs). The Query Answering Problem for these classes subsumes many cases of GF satisfiability. Our algorithms, in addition to making the connection to the tree-like model property clear, give a natural account of the selection and ordering strategies used by resolution procedures for the guarded fragment. We also believe that our rewriting algorithm for the special case of GTGDs may prove itself valuable in practice as it does not require any Skolemisation step and its theoretical runtime outperforms those of known GF resolution procedures in case of fixed dependencies. Moreover, we show a novel normalisation procedure for the widely used chase procedure in case of (disjunctive) GTGDs, which could be useful for future studies.

This work investigates if the current neural architectures are adequate for learning symbolic rewriting. Two kinds of data sets are proposed for this research -- one based on automated proofs and the other being a synthetic set of polynomial terms. The experiments with use of the current neural machine translation models are performed and its results are discussed. Ideas for extending this line of research are proposed and its relevance is motivated.

We define and study the problem of modular concept learning, that is, learning a concept that is a cross product of component concepts. If an element's membership in a concept depends solely on it's membership in the components, learning the concept as a whole can be reduced to learning the components. We analyze this problem with respect to different types of oracle interfaces, defining different sets of queries. If a given oracle interface cannot answer questions about the components, learning can be difficult, even when the components are easy to learn with the same type of oracle queries. While learning from superset queries is easy, learning from membership, equivalence, or subset queries is harder. However, we show that these problems become tractable when oracles are given a positive example and are allowed to ask membership queries. Keywords: Inductive Synthesis, Query-Based Learning, Modularity 1 Introduction Inductive synthesis or inductive learning is the synthesis of programs (concepts) from examples or other observations. Inductive synthesis has found application in formal methods, program analysis, software engineering, and related areas, for problems such as invariant generation (e.g.

Traditional first-order logic (FOL) reasoning systems usually rely on manual heuristics for proof guidance. We propose TRAIL: a system that learns to perform proof guidance using reinforcement learning. A key design principle of our system is that it is general enough to allow transfer to problems in different domains that do not share the same vocabulary of the training set. To do so, we developed a novel representation of the internal state of a prover in terms of clauses and inference actions, and a novel neural-based attention mechanism to learn interactions between clauses. We demonstrate that this approach enables the system to generalize from training to test data across domains with different vocabularies, suggesting that the neural architecture in TRAIL is well suited for representing and processing of logical formalisms.

A referring expression (RE) is a description that identifies a set of instances unambiguously. Mining REs from data finds applications in natural language generation, algorithmic journalism, and data maintenance. Since there may exist multiple REs for a given set of entities, it is common to focus on the most intuitive ones, i.e., the most concise and informative. In this paper we present REMI, a system that can mine intuitive REs on large RDF knowledge bases. Our experimental evaluation shows that REMI finds REs deemed intuitive by users. Moreover we show that REMI is several orders of magnitude faster than an approach based on inductive logic programming.

A coalition of agents, or a single agent, has an ethical dilemma between several statements if each joint action of the coalition forces at least one specific statement among them to be true. For example, any action in the trolley dilemma forces one specific group of people to die. In many cases, agents face ethical dilemmas because they are restricted in the amount of the resources they are ready to sacrifice to overcome the dilemma. The paper presents a sound and complete modal logical system that describes properties of dilemmas for a given limit on a sacrifice.

We present a machine-checked, formal proof of PAC learnability of the concept class of decision stumps. A formal proof has every step checked and justified using fundamental axioms of mathematics. We construct and check our proof using the Lean theorem prover. Though such a proof appears simple, a few analytic and measure-theoretic subtleties arise when carrying it out fully formally. We explain how we can cleanly separate out the parts that deal with these subtleties by using Lean features and a category theoretic construction called the Giry monad.

The Shapes Constraint Language (SHACL) has been recently introduced as a W3C recommendation to define constraints that can be validated against RDF graphs. Interactions of SHACL with other Semantic Web technologies, such as ontologies or reasoners, is a matter of ongoing research. In this paper we study the interaction of a subset of SHACL with inference rules expressed in datalog. On the one hand, SHACL constraints can be used to define a "schema" for graph datasets. On the other hand, inference rules can lead to the discovery of new facts that do not match the original schema. Given a set of SHACL constraints and a set of datalog rules, we present a method to detect which constraints could be violated by the application of the inference rules on some graph instance of the schema, and update the original schema, i.e, the set of SHACL constraints, in order to capture the new facts that can be inferred. We provide theoretical and experimental results of the various components of our approach.