We present a comprehensive case study in the automated synth esis of list sorting algorithms: two main proofs produce the most popular sorting algorithms (min-so rt, quick-sort, insert-sort, merge-sort) and trigger all the proofs necessary for producing the needed au xiliary functions for inserting, splitting, and merging. This is a continuation of our work on exploring in pa rallel the theories of multisets, lists, and binary trees, for the purpose of developing proof method s for the synthesis of algorithms on these domains. In one related paper [12] we already investigated a lgorithms for deletion from lists and binary trees using multisets. We follow the proof-based approach to automated synthesis: first one proves automatically a synthesis conjecture which is based on the specification (input and output conditions) of the desired function, then the algorithm is extracted automatically from the proo f, in form of conditional rewrite rules. The theoretical basis and the correctness of this scheme is well -known [6] and we used earlier in [11, 15].

We present improvements in maximum a-posteriori inference for Markov Logic, a widely used SRL formalism. Inferring the most probable world for Markov Logic is NP-hard in general. Several approaches, including Cutting Plane Aggregation (CPA), perform inference through translation to Integer Linear Programs. Aggregation exploits context-specific symmetries independently of evidence and reduces the size of the program. We illustrate much more symmetries occurring in long ground clauses that are ignored by CPA and can be exploited by higher-order aggregations. We propose Full-Constraint-Aggregation, a superior algorithm to CPA which exploits the ignored symmetries via a lifted translation method and some constraint relaxations. RDBMS and heuristic techniques are involved to improve the overall performance. We introduce Xeggora as an evolutionary extension of RockIt, the query engine that uses CPA. Xeggora evaluation on real-world benchmarks shows progress in efficiency compared to RockIt especially for models with long formulas.

Allen's Interval Algebra constitutes a framework for reasoning about temporal information in a qualitative manner. In particular, it uses intervals, i.e., pairs of endpoints, on the timeline to represent entities corresponding to actions, events, or tasks, and binary relations such as precedes and overlaps to encode the possible configurations between those entities. Allen's calculus has found its way in many academic and industrial applications that involve, most commonly, planning and scheduling, temporal databases, and healthcare. In this paper, we present a novel encoding of Interval Algebra using answer-set programming (ASP) extended by difference constraints, i.e., the fragment abbreviated as ASP(DL), and demonstrate its performance via a preliminary experimental evaluation. Although our ASP encoding is presented in the case of Allen's calculus for the sake of clarity, we suggest that analogous encodings can be devised for other point-based calculi, too.

Within AI, several sub-fields are particularly relevant to - and benefit from - studies of argumentation. These include decision support, knowledge representation, nonmonotonic reasoning, and multiagent systems. Moreover, computational argumentation provides a formal investigation of problems that have been studied informally only by philosophers, and which consequently allow for the development of computational tools for argumentation, see (Atkinson et al., 2017). Since its invention by Dung (1995), abstract argumentation based on argumentation frameworks (AFs) has become a key concept for the field. In AFs, argumentation scenarios are modeled as simple directed graphs, where the vertices represent arguments and each edge corresponds to an attack between two arguments. Besides its simplicity, there are several reasons for the success story of this concept: First, a multitude of semantics (Baroni et al., 2011, 2018) allows for tight coupling of argumentation with existing formalisms from the areas of knowledge representation and logic programming; indeed, one of the main motivations of Dung's work (Dung, 1995) was to give a uniform representation of several nonmonotonic formalisms including Reiter's Default Logic, Pollock's Defeasible Logic, and Logic Programming (LP) with default negation; the latter lead to a series of works that investigated the relationship between different LP semantics and different AF semantics, see e.g.

This work provides proof-search algorithms and automated counter-model extraction for a class of STIT logics. With this, we answer an open problem concerning syntactic decision procedures and cut-free calculi for STIT logics. A new class of cut-free complete labelled sequent calculi G3LdmL^m_n, for multi-agent STIT with at most n-many choices, is introduced. We refine the calculi G3LdmL^m_n through the use of propagation rules and demonstrate the admissibility of their structural rules, resulting in auxiliary calculi Ldm^m_nL. In the single-agent case, we show that the refined calculi Ldm^m_nL derive theorems within a restricted class of (forestlike) sequents, allowing us to provide proof-search algorithms that decide single-agent STIT logics. We prove that the proof-search algorithms are correct and terminate.

PIE is a Prolog-embedded environment for automated reasoning on the basis of first-order logic. It includes a versatile formula macro system and supports the creation of documents that intersperse macro definitions, reasoner invocations and LaTeX-formatted natural language text. Invocation of various reasoners is supported: External provers as well as sub-systems of PIE, which include preprocessors, a Prolog-based first-order prover, methods for Craig interpolation and methods for second-order quantifier elimination.

This book dwells on mathematical and algorithmic issues of data analysis based on generality order of descriptions and respective precision. To speak of these topics correctly, we have to go some way getting acquainted with the important notions of relation and order theory. On the one hand, data often have a complex structure with natural order on it. On the other hand, many symbolic methods of data analysis and machine learning allow to compare the obtained classifiers w.r.t. their generality, which is also an order relation. Efficient algorithms are very important in data analysis, especially when one deals with big data, so scalability is a real issue. That is why we analyze the computational complexity of algorithms and problems of data analysis. We start from the basic definitions and facts of algorithmic complexity theory and analyze the complexity of various tools of data analysis we consider. The tools and methods of data analysis, like computing taxonomies, groups of similar objects (concepts and n-clusters), dependencies in data, classification, etc., are illustrated with applications in particular subject domains, from chemoinformatics to text mining and natural language processing.

Finally, you can learn computation theory and programming language design in an engaging, practical way. Understanding Computation explains theoretical computer science in a context you'll recognize, helping you appreciate why these ideas matter and how they can inform your day-to-day programming. Rather than use mathematical notation or an unfamiliar academic programming language like Haskell or Lisp, this book uses Ruby in a reductionist manner to present formal semantics, automata theory, and functional programming with the lambda calculus.

Measuring of text complexity is a needed task in several domains and applications (such as NLP, semantic web, smart education and etc.). The Semantic layer of a text is more tacit than its syntactic structure and as a result, calculation of semantic complexity is more difficult. Whereas there are famous and powerful academic and commercial syntactic complexity measures, the problem of measuring Semantic complexity is a challenging one, yet. In this article, we introduce the DAST model which stands for Deciding About Semantic Complexity of a Text. In this model, an intuitionistic approach to semantics lets us have a well-defined definition for semantic of a text and its complexity: we consider semantic and meaning as a lattice of intuitions. Semantic complexity is defined as the result of a calculation on this lattice. A set theoretic formal definition of semantic complexity, as a 6-tuple formal system, is provided. By using this formal system, a method for measuring semantic complexity is presented. The evaluation of the proposed approach is done by a detailed example and a case study, a set of eighteen human-judgment experiments and a corpus-based evaluation. The results show that DAST model is capable of deciding about semantic complexity of a text. Furthermore, Analysis of the experiment results leads us to introduce a Markovian model for the process of common-sense multi-steps semantic-complexity reasoning in people. The Experiments-result demonstrates that our method consistently outperforms the random baseline in terms of better precision and accuracy.

The notion of cyber-physical systems (CPS) describes the co mbination of Information and Communication Technology (ICT) and software (the "cyber" part) with physical compone nts. A CPS can emerge from embedded systems by internetworking them. The first big research program focusi ng on CPS has been started by the US National Science Foundation in 2006, where the term CPS is defined in as such tha t it "refers to the tight conjoining of and coordination between computational and physical resources," stating "[ w]e envision that the cyber-physical systems of tomorrow will far exceed those of today in terms of adaptability, auto nomy, efficiency, functionality, reliability, safety, and usability" [1]. While the notion of CPS by the U.S. National Science Foundati on, as outlined above, includes ICT, it does not explicitly name Artificial Intelligence (AI) as a necessary component to raise an embedded system to the status of a CPS. Y et, the availability of sensory data together with a co mmunications system and the ability to exert actions upon the physical world that have been planned for the whole compo und of embedded systems components readily suggests that issues of planning, the increase of reflectivity, effici ency, and lowering resource usage is achieved by increasing the "intelligence" of the overall system. As such, research ers in the domain of AI have found numerous application domains. However, the two worlds of CPS and AI usually operate on diffe rent terms: CPS require operation within well-defined boundaries, i.e., as far as possible deterministic behavio r within well-known, strictly enforced margins of error. In contrast, many AI techniques--Artificial Neural Networks (A NNs) foremost--are firmly rooted in the domain of statistics, which is probably very well seen in the ANN train ing process.