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.

A new challenge for knowledge graph reasoning started in 2018. Deep learning has promoted the application of artificial intelligence (AI) techniques to a wide variety of social problems. Accordingly, being able to explain the reason for an AI decision is b ecoming important to ensure the secure and safe use of AI techniques. Thus, we, the Special Interest Group on Semantic Web and Ontology of the Japanese Society for AI, organized a challenge calling for techniques that reason and/or estimate which character s are criminals while providing a reasonable explanation based on an open knowledge graph of a well - known Sherlock Holmes mystery story . This paper presents a summary report of the first challenge held in 2018, including the knowledge graph construction, t he techniques proposed for reasoning and/or estimation, the evaluation metrics, and the results. The first prize went to an approach that formalized the problem as a constraint satisfaction problem and solved it using a lightweight formal method; the secon d prize went to an approach that used SPARQL and rules; the best resource prize went to a submission that constructed word embedding of characters from all sentences of Sherlock Holmes novels; and the best idea prize went to a discussion multi - agents model . We conclude this paper with the plans and issues for the next challenge in 2019.

Natural language understanding (NLU) of text is a fundamental challenge in AI, and it has received significant attention throughout the history of NLP research. This primary goal has been studied under different tasks, such as Question Answering (QA) and Textual Entailment (TE). In this thesis, we investigate the NLU problem through the QA task and focus on the aspects that make it a challenge for the current state-of-the-art technology. This thesis is organized into three main parts: In the first part, we explore multiple formalisms to improve existing machine comprehension systems. We propose a formulation for abductive reasoning in natural language and show its effectiveness, especially in domains with limited training data. Additionally, to help reasoning systems cope with irrelevant or redundant information, we create a supervised approach to learn and detect the essential terms in questions. In the second part, we propose two new challenge datasets. In particular, we create two datasets of natural language questions where (i) the first one requires reasoning over multiple sentences; (ii) the second one requires temporal common sense reasoning. We hope that the two proposed datasets will motivate the field to address more complex problems. In the final part, we present the first formal framework for multi-step reasoning algorithms, in the presence of a few important properties of language use, such as incompleteness, ambiguity, etc. We apply this framework to prove fundamental limitations for reasoning algorithms. These theoretical results provide extra intuition into the existing empirical evidence in the field.

This volume contains the Regular Papers, Technical Communicationsand the Doctoral Consortium papers of the 35th International Conference on Log ic Programming (ICLP 2019), held in Las Cruces, New Mexico, USA, from September 20-25, 2019. Since the first conference held in Marseille in 1982, ICLP has been the premier international event for presenting research in logic programming. Cont ributions are sought in all areas of logic programming, including but not restricted to: Foundations: Semantics, Formalisms, Nonmonotonic reasoning, Knowledge repre sen-tation.

Decades of research in artificial intelligence (AI) have produced formidable technologies that are providing immense benefit to industry, government, and society. AI systems can now translate across multiple languages, identify objects in images and video, streamline manufacturing processes, and control cars. The deployment of AI systems has not only created a trillion-dollar industry that is projected to quadruple in three years, but has also exposed the need to make AI systems fair, explainable, trustworthy, and secure. Future AI systems will rightfully be expected to reason effectively about the world in which they (and people) operate, handling complex tasks and responsibilities effectively and ethically, engaging in meaningful communication, and improving their awareness through experience. Achieving the full potential of AI technologies poses research challenges that require a radical transformation of the AI research enterprise, facilitated by significant and sustained investment. These are the major recommendations of a recent community effort coordinated by the Computing Community Consortium and the Association for the Advancement of Artificial Intelligence to formulate a Roadmap for AI research and development over the next two decades.