Rintanen and Gretton 2013; Abdulaziz, Gretton, and Norrish Many techniques for solving problems defined on transition 2015; Abdulaziz, Gretton, and Norrish 2017; Abdulaziz systems, like SATbased planning (Kautz and Selman 2019). Such compositional methods are currently the only 1992) and bounded model checking (Biere et al. 1999), benefit practically viable method to compute bounds on plan lengths from knowledge of upper bounds on the lengths of solution or the state space diameter. Compositional approaches provide transition sequences, aka completeness thresholds. If N useful approximations of plan bounds using smaller is such a bound, and if a solution exists, then that solution computational effort, since only explicit representations of need not comprise more than N transitions.

Recently, a growing number of researchers have applied machine learning to assist users of interactive theorem provers. However, the expressive nature of underlying logics and esoteric structures of proof documents impede machine learning practitioners, who often do not have much expertise in formal logic, let alone Isabelle/HOL, from achieving a large scale success in this field. In this data description, we present a simple dataset that contains data on over 400k proof method applications along with over 100 extracted features for each in a format that can be processed easily without any knowledge about formal logic. Our simple data format allows machine learning practitioners to try machine learning tools to predict proof methods in Isabelle/HOL without requiring domain expertise in logic.

Markov decision processes are of major interest in the planning community as well as in the model checking community. But in spite of the similarity in the considered formal models, the development of new techniques and methods happened largely independently in both communities. This work is intended as a beginning to unite the two research branches. We consider goal-reachability analysis as a common basis between both communities. The core of this paper is the translation from Jani, an overarching input language for quantitative model checkers, into the probabilistic planning domain definition language (PPDDL), and vice versa from PPDDL into Jani. These translations allow the creation of an overarching benchmark collection, including existing case studies from the model checking community, as well as benchmarks from the international probabilistic planning competitions (IPPC). We use this benchmark set as a basis for an extensive empirical comparison of various approaches from the model checking community, variants of value iteration, and MDP heuristic search algorithms developed by the AI planning community. On a per benchmark domain basis, techniques from one community can achieve state-ofthe-art performance in benchmarks of the other community. Across all benchmark domains of one community, the performance comparison is however in favor of the solvers and algorithms of that particular community. Reasons are the design of the benchmarks, as well as tool-related limitations. Our translation methods and benchmark collection foster crossfertilization between both communities, pointing out specific opportunities for widening the scope of solvers to different kinds of models, as well as for exchanging and adopting algorithms across communities.

AlphaZero learns to play go, chess and shogi at a superhuman level through self play given only the rules of the game. This raises the question of whether a similar thing could be done for mathematics -- a MathZero. MathZero would require a formal foundation and an objective. We propose the foundation of set-theoretic dependent type theory and an objective defined in terms of the classification problem -- the problem of classifying concept instances up to isomorphism. The natural numbers arise as the solution to the classification problem for finite sets. Here we generalize classical Bourbaki set-theoretic isomorphism to set-theoretic dependent type theory. To our knowledge we give the first isomorphism inference rules for set-theoretic dependent type theory with propositional set-theoretic equality. The presentation is intended to be accessible to mathematicians with no prior exposure to type theory.

Reasoning over streams of input data is an essential part of human intelligence. During the last decade {\em stream reasoning} has emerged as a research area within the AI-community with many potential applications. In fact, the increased availability of streaming data via services like Google and Facebook has raised the need for reasoning engines coping with data that changes at high rate. Recently, the rule-based formalism {\em LARS} for non-monotonic stream reasoning under the answer set semantics has been introduced. Syntactically, LARS programs are logic programs with negation incorporating operators for temporal reasoning, most notably {\em window operators} for selecting relevant time points. Unfortunately, by preselecting {\em fixed} intervals for the semantic evaluation of programs, the rigid semantics of LARS programs is not flexible enough to {\em constructively} cope with rapidly changing data dependencies. Moreover, we show that defining the answer set semantics of LARS in terms of FLP reducts leads to undesirable circular justifications similar to other ASP extensions. This paper fixes all of the aforementioned shortcomings of LARS. More precisely, we contribute to the foundations of stream reasoning by providing an operational fixed point semantics for a fully flexible variant of LARS and we show that our semantics is sound and constructive in the sense that answer sets are derivable bottom-up and free of circular justifications.

Recent work in proof theory has shed some light on the possibility of modeling reasoning while avoiding undesirable formal paradoxes. Based on category theory and inspired by the seminal work of J. Lambek, monoidal logics were introduced as a foundational framework that allows to treat a wide range of formal systems, including substructural logics (e.g., the syntactic calculus, linear logic, relevant logic, etc.), algebras (e.g., Kleene algebra) as well as intuitionistic, intermediate, and classical logic. This framework has been extended to modal logics and has been used to model normative reasoning, actions and knowledge, and it has been shown that non-classical logics better deal with the formal problems that are usually related to these notions. As such, non-classical systems of modal logics were proposed to model reasoning, actions and knowledge, but unresolved problems remained as to how to deal with conflicting obligations when facing normative inconsistencies. In this paper, we expose this problem and sketch an avenue for future research that might overcome this limitation.

We can break symmetry by eliminating solutions within a symmetry class that are not least in the lexicographical ordering. This is often referred to as the lex-leader method. Unfortunately, as symmetry groups can be large, the lexleader method is not tractable in general. We prove that using other total orderings besides the usual lexicographical ordering will not reduce the computational complexity of breaking symmetry in general. It follows that breaking symmetry with other orderings like the Gray code ordering or the Snake-Lex ordering is intractable in general.

The Natural Language Inference (NLI) task is an important task in modern NLP, as it asks a broad question to which many other tasks may be reducible: Given a pair of sentences, does the first entail the second? Although the state-of-the-art on current benchmark datasets for NLI are deep learning-based, it is worthwhile to use other techniques to examine the logical structure of the NLI task. We do so by testing how well a logically-controlled natural language (Attempto Controlled English) can be used to parse NLI sentences, and how well automated theorem provers can reason over the resulting formulae. To improve performance, we develop a set of syntactic and semantic transformation rules. We report their performance, and discuss implications for NLI and logic-based NLP.

There is an increasing interest in applying recent advances in AI to automated reasoning, as it may provide useful heuristics in reasoning over formalisms in first-order, second-order, or even meta-logics. To facilitate this research, we present MATR, a new framework for automated theorem proving explicitly designed to easily adapt to unusual logics or integrate new reasoning processes. MATR is formalism-agnostic, highly modular, and programmer-friendly. We explain the high-level design of MATR as well as some details of its implementation. To demonstrate MATR's utility, we then describe a formalized metalogic suitable for proofs of Gödel's Incompleteness Theorems, and report on our progress using our metalogic in MATR to semi-autonomously generate proofs of both the First and Second Incompleteness Theorems.

Boolean functional synthesis is a fundamental problem in computer science with wide-ranging applications and has witnessed a surge of interest resulting in progressively improved techniques over the past decade. Despite intense algorithmic development, a large number of problems remain beyond the reach of the state of the art techniques. Motivated by the progress in machine learning, we propose Manthan, a novel data-driven approach to Boolean functional synthesis. Manthan views functional synthesis as a classification problem, relying on advances in constrained sampling for data generation, and advances in automated reasoning for a novel proof-guided refinement and provable verification. On an extensive and rigorous evaluation over 609 benchmarks, we demonstrate that Manthan significantly improves upon the current state of the art, solving 356 benchmarks in comparison to 280, which is the most solved by a state of the art technique; thereby, we demonstrate an increase of 76 benchmarks over the current state of the art. Furthermore, Manthan solves 60 benchmarks that none of the current state of the art techniques could solve. The significant performance improvements, along with our detailed analysis, highlights several interesting avenues of future work at the intersection of machine learning, constrained sampling, and automated reasoning.