Combining Answer Set Programming (ASP) and Constraint Logic Programming (CLP) can create a more powerful language for knowledge representation and reasoning. The language AC(C) is designed to integrate ASP and CLP. Compared with existing integration of ASP and CSP, AC(C) allows representing user-defined constraints. Such integration provides great power for applications requiring logical reasoning involving constraints, e.g., temporal planning. In AC(C), user-defined and primitive constraints can be solved by a CLP inference engine while the logical reasoning over those constraints and regular logic literals is solved by an ASP inference engine (i.e., solver). My PhD work includes improving the language AC(C), implementing its faster inference engine and investigating how effective the new system can be used to solve a challenging application, temporal planning.

Game generation and analysis has commonly relied on hand authored rules and heuristics. This authoring task comes with a high authorial burden, both in the amount of rules and heuristics that need to be authored for decent coverage and in the complexity of authoring these rules. In this paper I present early work on \textit{Leda} and inductive logic programming system designed to learn these rules, so as to support further generation and analysis. I present Leda, describe its process, and finally show a sample set of the rules that it learns.

Morals are an important part of many stories, and central to why storytelling developed in the first place as a means of communication. They have the potential to provide a framework for developing story structure, which could be utilised by modern storytelling systems. To achieve this we need a general representation for morals. We propose patterns of character emotion as a suitable foundation. In this paper, we categorise Aesop's fables based on the morals they convey, and use them as a source of emotion data corresponding to those morals. We use inductive logic programming to identify relationships between particular patterns of emotion and the morals of the stories in which they arise.

Answer-set programming (ASP), a family of SAT-based logic programming systems, is attractive for procedural content generation.

Answer Set Programming (ASP) is a powerful programming paradigm that allows for an easy encoding of decision problems in NP. If the answer to a problem in NP is "yes," then, by definition, there is a "yes"-certificate that can be checked in polynomial time. In an ASP guess-and-check program, a programmer first declares the format of such a certificate, and then specifies the constraints that a well-formatted certificate should obey in order to be a "yes"- certificate. For example, for the well-known problem SAT, an ASP-programmer can first declare that certificates take the form of truth assignments, and then specify that "yes"-certificates are those certificates that leave no clause unsatisfied. While ASP guess-and-check programs are typically oriented towards NP-complete problems, they can also be used for problems in P. For example, the previously mentioned encoding of SAT also solves 2SAT, which is known to be in P. This raises the following issue which will be addressed in this paper. Assume that we have an answer set solver at our disposal, and that we have written a guess-and-check ASP program for a particular problem that is NPcomplete in general (for example, SAT). Assume furthermore that we know that under some restrictions, the problem can be solved in polynomial time (for example, the restriction of SAT to 2SAT).

We introduce Boolean Observation Games, a subclass of multi-player finite strategic games with incomplete information and qualitative objectives. In Boolean observation games, each player is associated with a finite set of propositional variables of which only it can observe the value, and it controls whether and to whom it can reveal that value. It does not control the given, fixed, value of variables. Boolean observation games are a generalization of Boolean games, a well-studied subclass of strategic games but with complete information, and wherein each player controls the value of its variables. In Boolean observation games player goals describe multi-agent knowledge of variables. As in classical strategic games, players choose their strategies simultaneously and therefore observation games capture aspects of both imperfect and incomplete information. They require reasoning about sets of outcomes given sets of indistinguishable valuations of variables. What a Nash equilibrium is, depends on an outcome relation between such sets. We present various outcome relations, including a qualitative variant of ex-post equilibrium. We identify conditions under which, given an outcome relation, Nash equilibria are guaranteed to exist. We also study the complexity of checking for the existence of Nash equilibria and of verifying if a strategy profile is a Nash equilibrium. We further study the subclass of Boolean observation games with `knowing whether' goal formulas, for which the satisfaction does not depend on the value of variables. We show that each such Boolean observation game corresponds to a Boolean game and vice versa, by a different correspondence, and that both correspondences are precise in terms of existence of Nash equilibria.

Tractable Boolean and arithmetic circuits have been studied extensively in AI for over two decades now. These circuits were initially proposed as "compiled objects," meant to facilitate logical and probabilistic reasoning, as they permit various types of inference to be performed in linear-time and a feed-forward fashion like neural networks. In more recent years, the role of tractable circuits has significantly expanded as they became a computational and semantical backbone for some approaches that aim to integrate knowledge, reasoning and learning. In this article, we review the foundations of tractable circuits and some associated milestones, while focusing on their core properties and techniques that make them particularly useful for the broad aims of neuro-symbolic AI.

We present and analyze the employment of the Diproche system, a natural language proof checker, within a one-semester mathematics beginners lecture with 228 participants. The system is used to check the students' solution attempts to proving exercises in Boolean set theory and elementary number theory and to give them immediate feedback. The benefits of the employment of the system are assessed via a questionnaire at the end of the semester and via analyzing the solution attempts of a subgroup of the students. Based on our results we develop approaches for future improvements.

The introduction of automated deduction systems in secondary schools face several bottlenecks, the absence of the subject of rigorous mathematical demonstrations in the curricula, the lack of knowledge by the teachers about the subject and the difficulty of tackling the task by automatic means. Despite those difficulties we claim that the subject of automated deduction in geometry can be introduced, by addressing it in particular cases: simple to manipulate by students and teachers and reasonably easy to be dealt by automatic deduction tools. The subject is discussed by addressing four secondary schools geometry problems: their rigorous proofs, visual proofs, numeric proofs, algebraic formal proofs, synthetic formal proofs, or the lack of them. For these problems we discuss a lesson plan to address them with the help of Information and Communications Technology, more specifically, automated deduction tools.

Letter-string analogy is an important analogy learning task which seems to be easy for humans but very challenging for machines. The main idea behind current approaches to solving letter-string analogies is to design heuristic rules for extracting analogy structures and constructing analogy mappings. However, one key problem is that it is difficult to build a comprehensive and exhaustive set of analogy structures which can fully describe the subtlety of analogies. This problem makes current approaches unable to handle complicated letter-string analogy problems. In this paper, we propose Neural logic analogy learning (Noan), which is a dynamic neural architecture driven by differentiable logic reasoning to solve analogy problems. Each analogy problem is converted into logical expressions consisting of logical variables and basic logical operations (AND, OR, and NOT). More specifically, Noan learns the logical variables as vector embeddings and learns each logical operation as a neural module. In this way, the model builds computational graph integrating neural network with logical reasoning to capture the internal logical structure of the input letter strings. The analogy learning problem then becomes a True/False evaluation problem of the logical expressions. Experiments show that our machine learning-based Noan approach outperforms state-of-the-art approaches on standard letter-string analogy benchmark datasets.