Complex artifacts are, of necessity, constructed by assembling simpler components. Software systems use libraries of reusable components, and often access multiple remote services. In this paper, we consider systems that can be formalized as solving the model expansion task for some class of finite structures. A wide range of problem solving and query answering systems are so accounted for. We present a method for automatically generating a solver for a complex system from a declarative definition of that system in terms of simpler modules, together with solvers for those modules. The work is motivated primarily by "knowledge-intensive" computing contexts, where the individual modules are defined in (possibly different) declarative languages, such as logical theories or logic programs, but can be applied anywhere the model expansion formalization can. The Algebra of Modular Systems (AMS) [48, 49], provides a way to define a complex module in terms of a collection of other modules, in purely semantic terms. Formally, each module in this algebra represents a class of structures, and a "solver" for the module solves the model expansion task for that class. That is, a solver for module M takes as input a structure A for a part of the vocabulary of M, and returns either a set of expansions of A that are in M, or the empty set.

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.

Syntactical antiunification reflects these abstraction techniques in the theoretically elegant domain of term algebras. In this article, we propose an extension, called E-anti-unification or E-generalization, which also provides a way of coping with the well-known problem of representation change [O'H92,DIS97]. It allows us to perform abstraction while modeling equivalent representations using appropriate equations between terms. This means that all equivalent representations are considered simultaneously in the abstraction process. Abstraction becomes insensitive to representation changes. In 1970, Plotkin and Reynolds [Plo70,Plo71,Rey70] introduced the notion of (syntactical) anti-unification of terms as the dual operation to unification: while the latter computes the most general common specialization of the given 1 1. x 0 x 2. x s(y) s(x y) 3. x 0 0 4. x s(y) x y x 0

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.

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 developed a method to draw and animate using SPARC, a logic programming system, and an online environment to support this method.Particularly, we introduce two predicates: one for drawing and one for animation. By our method, programmers will write a SPARC program, using our introduced predicates, to specify their drawing or animation. The drawing or animation will then be rendered upon executing the program with our system. In fact, our online system provides an environment where the programmers can easily edit and execute their programs.

Cyber-physical systems (CPS) are intended to receive information from the environment through sensors and perform appropriate actions using actuators of the controller. In the last years world of intelligent technologies has grown in an exponential fashion: from cruise control to smart ecosystems. Next we are facing the future of CPS involved in almost every aspect of our lives bringing higher comfortability and efficiency. Our goal is to help smart inventions adjust to this highly uncertain environment and guarantee safety for its inhabitants. The physical environment renders the problem of CPS verification extremely cumbersome. Due to a wealth of uncertainties introduced by physical processes, the system is best described by stochastic models. Approximate prediction techniques, such as Statistical Model Checking (SMC), have therefore recently become increasingly popular. As a result, verification of a CPS boils down to quantitative analysis of how close the system is to reaching bad states (safety property) or desired goal (liveness property). Controlling the systems, that is, computing appropriate response actions depending on the environment, involves probabilistic state estimation, as well as optimal action prediction, i.e., choosing the best next step by simulating the future. In my thesis, I develop a novel intelligent algorithm addressing existing deficiencies of SMC such as poor prediction of rare events (RE) and sampling divergence.

We study algorithms for fragments of first order logic ex- tended with counting quantifiers, which are known to be highly complex in general. We propose a fragment over unary predicates that is NP-complete and for which there is a nor- mal form where Counting Quantification sentences have a single Unary predicate, thus call it the CQU fragment. We provide an algebraic formulation of the CQU satisfiability problem in terms of Integer Linear Programming based on which two algorithms are proposed, a direct reduction to SAT instances and an Integer Linear Programming version extended with a column generation mechanism. The latter is shown to lead to a viable implementation and experiments shows this algorithm presents a phase transition behavior.