Automated theorem proving has long been a key task of artificial intelligence. Proofs form the bedrock of rigorous scientific inquiry. Many tools for both partially and fully automating their derivations have been developed over the last half a century. Some examples of state-of-the-art provers are E (Schulz, 2013), VAMPIRE (Kov\'acs & Voronkov, 2013), and Prover9 (McCune, 2005-2010). Newer theorem provers, such as E, use superposition calculus in place of more traditional resolution and tableau based methods. There have also been a number of past attempts to apply machine learning methods to guiding proof search. Suttner & Ertel proposed a multilayer-perceptron based method using hand-engineered features as far back as 1990; Urban et al (2011) apply machine learning to tableau calculus; and Loos et al (2017) recently proposed a method for guiding the E theorem prover using deep nerual networks. All of this prior work, however, has one common limitation: they all rely on the axioms of classical first-order logic. Very little attention has been paid to automated theorem proving for non-classical logics. One of the only recent examples is McLaughlin & Pfenning (2008) who applied the polarized inverse method to intuitionistic propositional logic. The literature is otherwise mostly silent. This is truly unfortunate, as there are many reasons to desire non-classical proofs over classical. Constructive/intuitionistic proofs should be of particular interest to computer scientists thanks to the well-known Curry-Howard correspondence (Howard, 1980) which tells us that all terminating programs correspond to a proof in intuitionistic logic and vice versa. This work explores using Q-learning (Watkins, 1989) to inform proof search for a specific system called non-classical logic called Core Logic (Tennant, 2017).

The theory of abstract argumentation frameworks (afs) has, in the main, focused on finite structures, though there are many significant contexts where argumentation can be regarded as a process involving infinite objects. To address this limitation, in this paper we propose a novel approach for describing infinite afs using tools from formal language theory. In particular, the possibly infinite set of arguments is specified through the language recognized by a deterministic finite automaton while a suitable formalism, called attack expression, is introduced to describe the relation of attack between arguments. The proposed approach is shown to satisfy some desirable properties which can not be achieved through other "naive" uses of formal languages. In particular, the approach is shown to be expressive enough to capture (besides any arbitrary finite structure) a large variety of infinite afs including two major examples from previous literature and two sample cases from the domains of multi-agent negotiation and ambient intelligence. On the computational side, we show that several decision and construction problems which are known to be polynomial time solvable in finite afs are decidable in the context of the proposed formalism and we provide the relevant algorithms. Moreover we obtain additional results concerning the case of finitary afs.

Good parameter settings are crucial to achieve high performance in many areas of artificial intelligence (AI), such as propositional satisfiability solving, AI planning, scheduling, and machine learning (in particular deep learning). Automated algorithm configuration methods have recently received much attention in the AI community since they replace tedious, irreproducible and error-prone manual parameter tuning and can lead to new state-of-the-art performance. However, practical applications of algorithm configuration are prone to several (often subtle) pitfalls in the experimental design that can render the procedure ineffective. We identify several common issues and propose best practices for avoiding them. As one possibility for automatically handling as many of these as possible, we also propose a tool called GenericWrapper4AC.

This paper builds upon our prior formalisation of R^n in ACL2(r) by presenting a set of theorems for reasoning about convex functions. This is a demonstration of the higher-dimensional analytical reasoning possible in our metric space formalisation of R^n. Among the introduced theorems is a set of equivalent conditions for convex functions with Lipschitz continuous gradients from Yurii Nesterov's classic text on convex optimisation. To the best of our knowledge a full proof of the theorem has yet to be published in a single piece of literature. We also explore "proof engineering" issues, such as how to state Nesterov's theorem in a manner that is both clear and useful.

In this paper, we study the model theoretical aspects of Weakly Aggregative Modal Logic (WAL), which is a collection of disguised polyadic modal logics with $n$-ary modalities whose arguments are all the same. We give a van-Benthem-Rosen characterization theorem of WAL based on an intuitive notion of bisimulation, and show that WAL has Craig Interpolation.

Abstract-- In hierarchical planning for Markov decision processes (MDPs), temporal abstraction allows planning with macro-actions that take place at different time scale in form of sequential composition. In this paper, we propose a novel approach to compositional reasoning and hierarchical planning for MDPs under temporal logic constraints. In addition to sequential composition, we introduce a composition of policies based on generalized logic composition: Given sub-policies for sub-tasks and a new task expressed as logic compositions of subtasks, a semi-optimal policy, which is optimal in planning with only sub-policies, can be obtained by simply composing sub-polices. Thus, a synthesis algorithm is developed to compute optimal policies efficiently by planning with primitive actions, policies for sub-tasks, and the compositions of sub-policies, for maximizing the probability of satisfying temporal logic specifications. We demonstrate the correctness and efficiency of the proposed method in stochastic planning examples with a single agent and multiple task specifications. I. INTRODUCTION Temporal logic is an expressive language to describe desired system properties: safety, reachability, obligation, stability, and liveness [18]. The algorithms for planning and probabilistic verification with temporal logic constraints have developed, with both centralized [2], [7], [17] and distributed methods [10]. Yet, there are two main barriers to practical applications: 1) The issue of scalability: In temporal logic constrained control problems, it is often necessary to introduce additional memory states for keeping track of the evolution of state variables with respect to these temporal logic constraints. The additional memory states grow exponentially (or double exponentially depending on the class of temporal logic) in the length of a specification [11] and make synthesis computational extensive.

This paper presents a practical application of Answer Set Programming to the understanding of narratives about restaurants. While this task was investigated in depth by Erik Mueller, exceptional scenarios remained a serious challenge for his script-based story comprehension system. We present a methodology that remedies this issue by modeling characters in a restaurant episode as intentional agents. We focus especially on the refinement of certain components of this methodology in order to increase coverage and performance. We present a restaurant story corpus that we created to design and evaluate our methodology.

Merging beliefs requires the plausibility of the sources of the information to be merged. They are typically assumed equally reliable when nothing suggests otherwise. A recent line of research has spun from the idea of deriving this information from the revision process itself. In particular, the history of previous revisions and previous merging examples provide information for performing subsequent merging operations. Yet, no examples or previous revisions may be available. In spite of the apparent lack of information, something can still be inferred by a try-and-check approach: a relative reliability ordering is assumed, the sources are integrated according to it and the result is compared with the original information. The final check may contradict the original ordering, like when the result of merging implies the negation of a formula coming from a source initially assumed reliable, or it implies a formula coming from a source assumed unreliable. In such cases, the reliability ordering assumed in the first place can be excluded from consideration. Such a scenario is proved real under the classifications of source reliability and definitions of belief integration considered in this article: sources divided in two, three or multiple reliability classes; integration is mostly by maximal consistent subsets but also weighted distance is considered.

The Weak Completion Semantics is a novel cognitive theory which has been successfully applied to the suppression task, the selection task, syllogistic reasoning, the belief bias effect, spatial reasoning as well as reasoning with conditionals. It is based on logic programming with skeptical abduction. Each program admits a least model under the three-valued Lukasiewicz logic, which can be computed as the least fixed point of an appropriate semantic operator. The semantic operator can be represented by a three-layer feed-forward network using the core method. Its least fixed point is the unique stable state of a recursive network which is obtained from the three-layer feed-forward core by mapping the activation of the output layer back to the input layer. The recursive network is embedded into a novel network to compute skeptical abduction. This paper presents a fully connectionist realization of the Weak Completion Semantics.

Propositional Typicality Logic (PTL) is a recently proposed logic, obtained by enriching classical propositional logic with a typicality operator capturing the most typical (alias normal or conventional) situations in which a given sentence holds. The semantics of PTL is in terms of ranked models as studied in the well-known KLM approach to preferential reasoning and therefore KLM-style rational consequence relations can be embedded in PTL. In spite of the non-monotonic features introduced by the semantics adopted for the typicality operator, the obvious Tarskian definition of entailment for PTL remains monotonic and is therefore not appropriate in many contexts. Our first important result is an impossibility theorem showing that a set of proposed postulates that at first all seem appropriate for a notion of entailment with regard to typicality cannot be satisfied simultaneously. Closer inspection reveals that this result is best interpreted as an argument for advocating the development of more than one type of PTL entailment. In the spirit of this interpretation, we investigate three different (semantic) versions of entailment for PTL, each one based on the definition of rational closure as introduced by Lehmann and Magidor for KLM-style conditionals, and constructed using different notions of minimality.