We consider bounded width CNF-formulas where the width is measured by popular graph width measures on graphs associated to CNF-formulas. Such restricted graph classes, in particular those of bounded treewidth, have been extensively studied for their uses in the design of algorithms for various computational problems on CNF-formulas. Here we consider the expressivity of these formulas in the model of clausal encodings with auxiliary variables. We first show that bounding the width for many of the measures from the literature leads to a dramatic loss of expressivity, restricting the formulas to those of low communication complexity. We then show that the width of optimal encodings with respect to different measures is strongly linked: there are two classes of width measures, one containing primal treewidth and the other incidence cliquewidth, such that in each class the width of optimal encodings only differs by constant factors. Moreover, between the two classes the width differs at most by a factor logarithmic in the number of variables. Both these results are in stark contrast to the setting without auxiliary variables where all width measures we consider here differ by more than constant factors and in many cases even by linear factors.

A new algorithm for deciding the satisfiability of polynomial formulas over the reals is proposed. The key point of the algorithm is a new projection operator, called sample-cell projection operator, custom-made for Conflict-Driven Clause Learning (CDCL)-style search. Although the new operator is also a CAD (Cylindrical Algebraic Decomposition)-like projection operator which computes the cell (not necessarily cylindrical) containing a given sample such that each polynomial from the problem is sign-invariant on the cell, it is of singly exponential time complexity. The sample-cell projection operator can efficiently guide CDCL-style search away from conflicting states. Experiments show the effectiveness of the new algorithm.

Given the large variety of existing logical formalisms it is of utmost importance to select the most adequate one for a specific purpose, e.g. for representing the knowledge relevant for a particular application or for using the formalism as a modeling tool for problem solving. Awareness of the nature of a logical formalism, in other words, of its fundamental intrinsic properties, is indispensable and provides the basis of an informed choice. One such intrinsic property of logic-based knowledge representation languages is the context-dependency of pieces of knowledge. In classical propositional logic, for example, there is no such context-dependence: whenever two sets of formulas are equivalent in the sense of having the same models (ordinary equivalence), then they are mutually replaceable in arbitrary contexts (strong equivalence). However, a large number of commonly used formalisms are not like classical logic which leads to a series of interesting developments.

Common criticisms of state-of-the-art machine learning include poor generalisation, a lack of interpretability, and a need for large amounts of training data. We survey recent work in inductive logic programming (ILP), a form of machine learning that induces logic programs from data, which has shown promise at addressing these limitations. We focus on new methods for learning recursive programs that generalise from few examples, a shift from using hand-crafted background knowledge to \emph{learning} background knowledge, and the use of different technologies, notably answer set programming and neural networks. As ILP approaches 30, we also discuss directions for future research.

They are a fundamental datatype in all the modern programming languages, and operations on strings frequently occur in disparate fields such as software analysis, model checking, database applications, web security, bioinformatics and so on[3, 11, 19, 21, 27, 28, 49, 60, 67]. Reasoning over strings requires solving arbitrarily complex string constraints, i.e., relations defined on a number of string variables. Typical examples of string constraints are string length, (dis-)equality, concatenation, substring, regular expression matching. With the term "string constraint solving" (in short, string solving or SCS) we refer to the process of modelling, processing, and solving combinatorial problems involving string constraints. We may see SCS as a declarative paradigm which falls at the intersection between constraint solving and combinatorics on words: the user states a problem with string variables and constraints, and a suitable string solver seeks a solution for that problem. Although works on the combinatorics of words were already published in the 1940s [110], the dawn of SCS dates back to the late 1980s in correspondence with the rise of Constraint Programming (CP) [114] and Constraint Logic Programming(CLP)[73] paradigms. Pioneers in this field were for example Trilogy[142], a language providing strings, integer and real constraints, and CLP(Σ) [144], an instance of the CLP scheme representing strings as regular sets. The latter in particular was the first known attempt to use string constraints like regular membership to denote regular sets.

Many procedures for SAT and SAT-related problems -- in particular for those requiring the complete enumeration of satisfying truth assignments -- rely their efficiency on the detection of partial assignments satisfying an input formula. In this paper we analyze the notion of partial-assignment satisfiability -- in particular when dealing with non-CNF and existentially-quantified formulas -- raising a flag about the ambiguities and subtleties of this concept, and investigating their practical consequences. This may drive the development of more effective assignment-enumeration algorithms.

The geometry automated theorem proving area distinguishes itself by a large number of specific methods and implementations, different approaches (synthetic, algebraic, semi-synthetic) and different goals and applications (from research in the area of artificial intelligence to applications in education). Apart from the usual measures of efficiency (e.g. CPU time), the possibility of visual and/or readable proofs is also an expected output against which the geometry automated theorem provers (GATP) should be measured. The implementation of a competition between GATP would allow to create a test bench for GATP developers to improve the existing ones and to propose new ones. It would also allow to establish a ranking for GATP that could be used by "clients" (e.g. developers of educational e-learning systems) to choose the best implementation for a given intended use.

When working on intelligent tutor systems designed for mathematics education and its specificities, an interesting objective is to provide relevant help to the students by anticipating their next steps. This can only be done by knowing, beforehand, the possible ways to solve a problem. Hence the need for an automated theorem prover that provide proofs as they would be written by a student. To achieve this objective, logic programming is a natural tool due to the similarity of its reasoning with a mathematical proof by inference. In this paper, we present the core ideas we used to implement such a prover, from its encoding in Prolog to the generation of the complete set of proofs. However, when dealing with educational aspects, there are many challenges to overcome. We also present the main issues we encountered, as well as the chosen solutions. The QED-Tutrix software [15, 19] provides an environment where a highschool student can solve geometry proof problems. One of its key features is that it allows the student to provide proof elements in any order, not limiting them to forward-or backward-chaining. For instance, when solving the simple problem "prove that a quadrilateral with three right angles is a rectangle", the student can provide any element of any possible proof, such as a direct consequence of the hypotheses ("if two lines are perpendicular to a third, they are parallel"), a necessary premise for the conclusion ("a rectangle is a quadrilateral that has four right angles"), or anything in between ("the quadrilateral ABCD is a parallelogram"). A second key feature is the tutoring aspect. When the student is stuck is the resolution, the software is able to provide them with relevant messages. In the previous example, if the student entered "the quadrilateral ABCD is a parallelogram" and is stuck afterwards, the software identifies that they are working on a proof using parallelogram properties, and will provide them messages such as "what is the definition of a parallelogram?" or "is there a relation between parallelogram and rectangle?" These features, the flexibility in exploration and the tutoring, are very interesting from a mathematics education perspective, but come with a cost.

PIE is a Prolog-embedded environment for automated reasoning on the basis of first-order logic. Its main focus is on formulas, as constituents of complex formalizations that are structured through formula macros, and as outputs of reasoning tasks such as second-order quantifier elimination and Craig interpolation. It supports a workflow based on documents that intersperse macro definitions, invocations of reasoners, and LaTeX-formatted natural language text. Starting from various examples, the paper discusses features and application possibilities of PIE along with current limitations and issues for future research.

The aim of this work is to provide a family of qualitative theories for spatial change in general, and for motion of spatial scenes in particular. To achieve this, we consider a spatio-temporalisation MTALC(Dx), of the well-known ALC(D) family of Description Logics (DLs) with a concrete domain: the MTALC(Dx) concepts are interpreted over infinite k-ary Sigma-trees, with the nodes standing for time points, and Sigma including, additionally to its uses in classical k-ary Sigma-trees, the description of the snapshot of an n-object spatial scene of interest; the roles split into m+n immediate-successor (accessibility) relations, which are serial, irreflexive and antisymmetric, and of which m are general, not necessarily functional, the other n functional; the concrete domain Dx is generated by an RCC8-like spatial Relation Algebra (RA) x, and is used to guide the change by imposing spatial constraints on objects of the "followed" spatial scene, eventually at different time points of the input trees. In order to capture the expressiveness of most modal temporal logics encountered in the literature, we introduce weakly cyclic Terminological Boxes (TBoxes) of MTALC(Dx), whose axioms capture the decreasing property of modal temporal operators. We show the important result that satisfiability of an MTALC(Dx) concept with respect to a weakly cyclic TBox can be reduced to the emptiness problem of a Buchi weak alternating automaton augmented with spatial constraints. In another work, complementary to this one, also submitted to this conference, we thoroughly investigate Buchi automata augmented with spatial constraints, and provide, in particular, a translation of an alternating into a nondeterministic, and an effective decision procedure for the emptiness problem of the latter.