"I think the best hope for human-level AI is logical AI, based on the formalizing of commonsense knowledge and reasoning in mathematical logic. Formalizing common sense requires extensions to mathematical logic including nonmonotonic reasoning and extensive reification, e.g., of concepts and also contexts. The reifications require appropriate reflection schemas."
– from The Future of AI—A Manifesto by John McCarthy. AI Magazine 26(4), (2005).
One of the fastest advancing areas of modern science is functional genomics. This science seeks to understand how the complete complement of molecular components of living organisms (nucleic acid, protein, small molecules, and so on) interact together to form living organisms. Functional genomics is of interest to AI because the relationship between machines and living organisms is central to AI and because the field is an instructive and fun domain to apply and sharpen AI tools and ideas, requiring complex knowledge representation, reasoning, learning, and so on. This article describes two machine learning (inductive logic programming [ILP])-based approaches to the bioinformatic problem of predicting protein function from amino acid sequence. The first approach is based on using ILP as a way of bootstrapping from conventional sequence-based homology methods.
Doug Lenat has worked in diverse parts of AI – natural language understanding and generation, automatic program synthesis, expert systems, machine learning, etc. – for going on 40 years now, just long enough to dare to write this article. His 1976 Stanford PhD thesis, AM, demonstrated that creative discoveries in mathematics could be produced by a computer program (a theorem proposer, rather than a theorem prover) guided by a corpus of hundreds of heuristic rules for deciding which experiments to perform and judging "interestingness" of their outcomes. That work earned him the IJCAI Computers and Thought Award, and sparked a renaissance in machine learning research. Dr. Lenat was on the CS faculty at CMU and Stanford, was one of the founders of Teknowledge, and was in the first batch of AAAI Fellows. He worked with Bill Gates and Nathan Myhrvold to launch Microsoft Research Labs, and to this day he remains the only person to have served on the technical advisory boards of both Apple and Microsoft.
This book represents a selection of papers presented at the Inductive Logic Programming (ILP) workshop held at Cumberland Lodge, Great Windsor Park. The collection marks two decades since the first ILP workshop in 1991. During this period the area has developed into the main forum for work on logic-based machine learning. The chapters cover a wide variety of topics, ranging from theory and ILP implementations to state-of-the-art applications in real-world domains. The international contributors represent leaders in the field from prestigious institutions in Europe, North America and Asia.
Many systems are naturally modeled as Markov Decision Processes (MDPs), combining probabilities and strategic actions. Given a model of a system as an MDP and some logical specification of system behavior, the goal of synthesis is to find a policy that maximizes the probability of achieving this behavior. A popular choice for defining behaviors is Linear Temporal Logic (LTL). Policy synthesis on MDPs for properties specified in LTL has been well studied. LTL, however, is defined over infinite traces, while many properties of interest are inherently finite. Linear Temporal Logic over finite traces (LTLf) has been used to express such properties, but no tools exist to solve policy synthesis for MDP behaviors given finite-trace properties. We present two algorithms for solving this synthesis problem: the first via reduction of LTLf to LTL and the second using native tools for LTLf. We compare the scalability of these two approaches for synthesis and show that the native approach offers better scalability compared to existing automaton generation tools for LTL.
We consider weighted structures, which extend ordinary relational structures by assigning weights, i.e. elements from a particular group or ring, to tuples present in the structure. We introduce an extension of first-order logic that allows to aggregate weights of tuples, compare such aggregates, and use them to build more complex formulas. We provide locality properties of fragments of this logic including Feferman-Vaught decompositions and a Gaifman normal form for a fragment called FOW1, as well as a localisation theorem for a larger fragment called FOWA1. This fragment can express concepts from various machine learning scenarios. Using the locality properties, we show that concepts definable in FOWA1 over a weighted background structure of at most polylogarithmic degree are agnostically PAC-learnable in polylogarithmic time after pseudo-linear time preprocessing.
Autonomous Intelligent Systems are designed to reduce the need for human intervention in our daily life. However, the full benefit of these new systems will be attained only if they are aligned with society's values and ethical principles. Adopting ethical approaches to building such systems has been attracting a lot of attention in the recent years. The global concern about the ethical behavior of this kind of technologies has manifested in many initiatives at different levels. As examples, we mention: the IEEE initiative for ethically aligned design of autonomous intelligent systems ('Ethics in Action'
We study a dynamic version of multi-agent path finding problem (called D-MAPF) where existing agents may leave and new agents may join the team at different times. We introduce a new method to solve D-MAPF based on conflict-resolution. The idea is, when a set of new agents joins the team and there are conflicts, instead of replanning for the whole team, to replan only for a minimal subset of agents whose plans conflict with each other. We utilize answer set programming as part of our method for planning, replanning and identifying minimal set of conflicts.
Answer set programming (ASP) is a well-established knowledge representation formalism. Most ASP solvers are based on (extensions of) technology from Boolean satisfiability solving. While these solvers have shown to be very successful in many practical applications, their strength is limited by their underlying proof system, resolution. In this paper, we present a new tool LP2PB that translates ASP programs into pseudo-Boolean theories, for which solvers based on the (stronger) cutting plane proof system exist. We evaluate our tool, and the potential of cutting-plane-based solving for ASP on traditional ASP benchmarks as well as benchmarks from pseudo-Boolean solving. Our results are mixed: overall, traditional ASP solvers still outperform our translational approach, but several benchmark families are identified where the balance shifts the other way, thereby suggesting that further investigation into a stronger proof system for ASP is valuable.
Answer Set Programming (ASP) [13, 12, 4] is a successful paradigm for Knowledge Representation and problem solving. Under this paradigm, the programmer represents a problem as a logic program formed by a set of rules and obtains solutions to that problem in terms of models of the program called answer sets. Thanks to the availability of efficient solvers, ASP is nowadays applied in a wide variety of areas including robotics, bioinformatics, music composition [7, 5, 3], and many more. An ASP program does not contain information about the method to obtain the answer sets, something that is completely delegated to the ASP solver. This, of course, has the advantage of making ASP a fully declarative language, where the programmer must concentrate on specification rather than on design of search algorithms.
Paraconsistent logics constitute an important class of formalisms dealing with non-trivial reasoning from inconsistent premisses. In this paper, we introduce uniform axiomatisations for a family of nonmonotonic paraconsistent logics based on minimal inconsistency in terms of sequent-type proof systems. The latter are prominent and widely-used forms of calculi well-suited for analysing proof search. In particular, we provide sequent-type calculi for Priest's three-valued minimally inconsistent logic of paradox, and for four-valued paraconsistent inference relations due to Arieli and Avron. Our calculi follow the sequent method first introduced in the context of nonmonotonic reasoning by Bonatti and Olivetti, whose distinguishing feature is the use of a so-called rejection calculus for axiomatising invalid formulas. In fact, we present a general method to obtain sequent systems for any many-valued logic based on minimal inconsistency, yielding the calculi for the logics of Priest and of Arieli and Avron as special instances.