What inspired you to study Artificial Intelligence? I did my first degree at Imperial College in computer science; in my final year, I took a module in Logic Programming which was taught by Professor Robert Kowalski. It was fascinating because it was so different to other things I'd learned; it featured a declarative form of programming that allowed the system to "reason" and provide its own conclusions. Indeed, this was so fascinating for me that I wrote a connection graph theorem prover in Prolog for my final year project; I then went on to study Artificial Intelligence at the University of Edinburgh. I remain fascinated by systems that permit you to say things at a high level of abstraction and then allow systems to draw their own conclusions. What were your initial main challenges when you began to study Artificial Intelligence?

To appear in the proceedings of LPAR 21. Solving complex problems can involve non-trivial combinations of distinct knowledge bases and problem solvers. The Algebra of Modular Systems is a knowledge representation framework that provides a method for formally specifying such systems in purely semantic terms. Formally, an expression of the algebra defines a class of structures. Many expressive formalism used in practice solve the model expansion task, where a structure is given on the input and an expansion of this structure in the defined class of structures is searched (this practice overcomes the common undecidability problem for expressive logics). In this paper, we construct a solver for the model expansion task for a complex modular systems from an expression in the algebra and black-box propagators or solvers for the primitive modules. To this end, we define a general notion of propagators equipped with an explanation mechanism, an extension of the alge- bra to propagators, and a lazy conflict-driven learning algorithm. The result is a framework for seamlessly combining solving technology from different domains to produce a solver for a combined system.

The optimization of algorithm (hyper-)parameters is crucial for achieving peak performance across a wide range of domains, ranging from deep neural networks to solvers for hard combinatorial problems. The resulting algorithm configuration (AC) problem has attracted much attention from the machine learning community. However, the proper evaluation of new AC procedures is hindered by two key hurdles. First, AC benchmarks are hard to set up. Second and even more significantly, they are computationally expensive: a single run of an AC procedure involves many costly runs of the target algorithm whose performance is to be optimized in a given AC benchmark scenario. One common workaround is to optimize cheap-to-evaluate artificial benchmark functions (e.g., Branin) instead of actual algorithms; however, these have different properties than realistic AC problems. Here, we propose an alternative benchmarking approach that is similarly cheap to evaluate but much closer to the original AC problem: replacing expensive benchmarks by surrogate benchmarks constructed from AC benchmarks. These surrogate benchmarks approximate the response surface corresponding to true target algorithm performance using a regression model, and the original and surrogate benchmark share the same (hyper-)parameter space. In our experiments, we construct and evaluate surrogate benchmarks for hyperparameter optimization as well as for AC problems that involve performance optimization of solvers for hard combinatorial problems, drawing training data from the runs of existing AC procedures. We show that our surrogate benchmarks capture overall important characteristics of the AC scenarios, such as high- and low-performing regions, from which they were derived, while being much easier to use and orders of magnitude cheaper to evaluate.

We extend the notion of anti-unification to cover equational theories and present a method based on regular tree grammars to compute a finite representation of E-generalization sets. We present a framework to combine Inductive Logic Programming and E-generalization that includes an extension of Plotkin's lgg theorem to the equational case. We demonstrate the potential power of E-generalization by three example applications: computation of suggestions for auxiliary lemmas in equational inductive proofs, computation of construction laws for given term sequences, and learning of screen editor command sequences.

For most branching algorithms in Boolean logic "branching" means "variable-wise branching". We present the apparently novel technique of clause-wise branching, which is used to solve the ALLSAT problem for arbitrary Boolean functions in CNF format. Specifically, it converts a CNF into an orthogonal DNF, i.e. into an exclusive sum of products. Our method is enhanced by two ingredients: The use of a good SAT-solver and wildcards beyond the common don't-care symbol.

In this paper, we propose a fundamentally new approach to Datalog evaluation. Given a linear Datalog program DB written using N constants and binary predicates, we first translate if-and-only-if completions of clauses in DB into a set Eq(DB) of matrix equations with a non-linear operation where relations in M_DB, the least Herbrand model of DB, are encoded as adjacency matrices. We then translate Eq(DB) into another, but purely linear matrix equations tilde_Eq(DB). It is proved that the least solution of tilde_Eq(DB) in the sense of matrix ordering is converted to the least solution of Eq(DB) and the latter gives M_DB as a set of adjacency matrices. Hence computing the least solution of tilde_Eq(DB) is equivalent to computing M_DB specified by DB. For a class of tail recursive programs and for some other types of programs, our approach achieves O(N^3) time complexity irrespective of the number of variables in a clause since only matrix operations costing O(N^3) or less are used. We conducted two experiments that compute the least Herbrand models of linear Datalog programs. The first experiment computes transitive closure of artificial data and real network data taken from the Koblenz Network Collection. The second one compared the proposed approach with the state-of-the-art symbolic systems including two Prolog systems and two ASP systems, in terms of computation time for a transitive closure program and the same generation program. In the experiment, it is observed that our linear algebraic approach runs 10^1 ~ 10^4 times faster than the symbolic systems when data is not sparse. To appear in Theory and Practice of Logic Programming (TPLP).

Qualitative reasoning formalisms are an active research topic in artificial intelligence. In this survey we present a model-theoretic perspective on qualitative constraint reasoning and explain some of the basic concepts and results in an accessible way. In particular, we discuss the significance of omega-categoricity for qualitative reasoning, of primitive positive interpretations for complexity analysis, and of Datalog as a unifying language for describing local consistency algorithms.

HEX-programs are an extension of answer set programming(ASP) towards external sources. To this end, external atomsprovide a bidirectional interface between the program and anexternal source. Traditionally, HEX -programs are evaluatedusing a rewriting to ordinary ASP programs which guess truthvalues of external atoms; this yields answer set candidateswhose guesses are verified by evaluating the source. Despitethe integration of learning techniques into this approach, whichreduce the number of candidates and of necessary verificationcalls, the remaining external calls are still expensive. In thispaper we present an alternative approach based on inliningof external atoms, motivated by existing but less general approaches for specialized formalisms such as DL-programs. External atoms are then compiled away such that no verification calls are necessary. To this end, we make use of supportsets, which describe conditions on input atoms that are sufficient to satisfy an external atom. The approach is implementedin the DLVHEX reasoner. Experiments show a significant performance gain.

Temporal reasoning is one of the main topics investigated within the field of Artificial Intelligence. Formal methods for temporal reasoning arouse interest of researchers from both theoretical and practical point of view. Such methods enable modelling and studying human-like reasoning mechanisms, thus constituting a valuable tool in cognitive science, philosophy, and linguistics. On the other hand, temporal reasoning formalisms have a number of potential practical applications, e.g., in task scheduling, action planning, and temporal databases. Temporal reasoning methods may be divided into point-based and interval-based depending on the type of the considered primitive ontological objects. My work revolves around the latter type of methods which seem to be more human-like and more suitable for such applications as continuous process modelling. My main result is that the satisfiability problem in a hybridized fragment of Halpern-Shoham logic in which formulas are in a form of conjunction of Horn clauses and only box modal operators are allowed (diamond operators are disallowed) is NP-complete over reflexive, as well as over irreflexive and dense time frames. Before hybridization this fragment was P-complete over such time structures.

We present a SAT-based approach for solving the modal logic S5-satisfiability problem. That problem being NP-complete, the translation into SAT is not a surprise. Our contribution is to greatly reduce the number of propositional variables and clauses required to encode the problem. We first present a syntactic property called diamond degree. We show that the size of an S5-model satisfying a formula phi can be bounded by its diamond degree. Such measure can thus be used as an upper bound for generating a SAT encoding for the S5-satisfiability of that formula. We also propose a lightweight caching system which allows us to further reduce the size of the propositional formula.We implemented a generic SAT-based approach within the modal logic S5 solver S52SAT. It allowed us to compare experimentally our new upper-bound against previously known one, i.e. the number of modalities of phi and to evaluate the effect of our caching technique. We also compared our solver againstexisting modal logic S5 solvers. The proposed approach outperforms previous ones on the benchmarks used. These promising results open interesting research directions for the practical resolution of others modal logics (e.g. K, KT, S4)