ABSTRACT. We present an abstract development of Gödel’s incompleteness theorems, performed with the help of the Isabelle/HOL theorem prover. We analyze sufficient conditions for the theorems’ applicability to a partially specified logic. In addition to the usual benefits of generality, our abstract perspective enables a comparison between alternative approaches from the literature. These include Rosser’s variation of the first theorem, Jeroslow’s variation of the second theorem, and the Swierczkowski–Paulson semantics-based approach. As part of our framework's validation, we upgrade Paulson’s Isabelle proof to produce a mechanization of the second theorem that does not assume soundness in the standard model, and in fact does not rely on any notion of model or semantic interpretation.

ABSTRACT. Vampire is an automatic theorem prover for first-order logic. During proof search in given-clause algorithms, Vampire repeatedly selects clauses from either an age or a weight queue in a fixed, but configurable age/weight ratio (AWR). We show that an optimal fixed value of this ratio can produce proofs significantly more quickly on a given problem, and further that varying AWR during proof search can improve upon a fixed ratio. Based on these observations we develop several new modes for Vampire which vary AWR according to a “shape” during proof search. The modes solve a number of new problems in the TPTP benchmark.

ABSTRACT. We describe an efficient implementation of clause guidance in saturation-based automated theorem provers extending the ENIGMA approach. Unlike in the first ENIGMA implementation where fast linear classifier is trained and used together with manually engineered features, we have started to experiment with more sophisticated state-of-the-art machine learning methods such as gradient boosted trees and recursive neural networks. In particular the latter approach poses challenges in terms of efficiency of clause evaluation, however we show that deep integration of the neural evaluation with the ATP data-structures can largely amortize this cost and lead to competitive real-time results. Both methods are evaluated on a large dataset of theorem proving problems and compared with the previous approaches. The resulting methods improve on the manually designed clause guidance, providing the first practically convincing application of gradient-boosted and neural clause guidance in saturation-style automated theorem provers.

ABSTRACT. First order theorem proving with large knowledge bases makes it necessary to select those parts of the knowledge base, which are necessary to prove the theorem at hand. We propose to extend syntactic axiom selection procedures like SInE to the use of the semantics of symbol names. For this not only occurrences of symbol names but also similar names are taken into account. We propose to use a similarity measure based on word embeddings like ConceptNet Numberbatch. An evaluation of this similarity based SInE is given by using problem sets from TPTP's CSR problem class and Adimen-SUMO. This evaluation is done with two very different systems, namely the HYPER tableau prover and the saturation based system E.

ABSTRACT. Many applications of theorem proving, for example program verification and analysis, require first-order reasoning with both quantifiers and theories such as arithmetic and datatypes. There is no complete procedure for reasoning in such theories but the state-of-the-art in automated theorem proving is still able to reason effectively with real-world problems from this rich domain. In this paper we introduce a missing part of the puzzle: automated induction inside a saturation-based theorem prover. Our goal is to incorporate lightweight automated induction in a way that complements the saturation-based approach, allowing us to solve problems requiring a combination of first-order reasoning, theory reasoning, and inductive reasoning. We implement a number of techniques and heuristics and evaluate them within the Vampire theorem prover. Our results show that these new techniques enjoy practical success on real-world problems.

ABSTRACT. The aspect calculus for reasoning about states and actions has some advantages over existing situation calculus formalisms for theorem proving applications, and also provides an application domain and a source of problems for first-order theorem provers. The aspect calculus provides a representation for reasoning about states and actions that is suited to modular domains. An aspect names a portion of a state, that is, a substate, such as a room in a building or a city in a country. Aspects may have aspects of their own. A state is assumed to be either a {\em leaf state} that cannot be further decomposed, or to be composed of substates, and actions associated with one substate do not influence other, disjoint substates. This feature can reduce the number of frame axioms that are needed if the domain has a modular structure. It can also permit planning problems on independent substates to be solved independently to some degree. However, interactions between independent substates are also permitted.

ABSTRACT. We build a Default Logic variant on Intuitionistic Propositional Logic and develop a sound, complete, and terminating, tableaux calculus for it. We also present an implementation of the calculus. We motivate and illustrate the technical elements of our work with examples.

ABSTRACT. Forgetting refers to an ontology engineering technology that seeks to produce views of description logic ontologies. This is achieved by eliminating a set of concept and role names from ontologies in such a way that all logical consequences up to the remaining signature are preserved. In this paper, we describe FAME(Q), a Java-based implementation of a semantic forgetting method developed recently for eliminating concept and role names from ALCOQH-ontologies. FAME(Q) is so far the only tool for concept forgetting in description logics with number restrictions and nominals, and the only tool for role forgetting in description logics with number restrictions. FAME(Q) can be used as a standalone tool or a Java library for forgetting or related tasks. An evaluation of \fameq on a large corpus of biomedical ontologies showed the tool was able to compute forgetting solutions in nearly 90% of the test cases, and in most of these cases, the solutions were computed within a few seconds.

ABSTRACT. This paper introduces GKC, a resolution prover optimized for search in large knowledge bases. The system is built upon a shared memory graph database Whitedb, enabling it to solve multiple different queries without a need to repeatedly parse or load the large parsed knowledge base from the disk. Due to the relatively shallow and simple structure of most of the literals in the knowledge base, the indexing methods used are mostly hash-based. While GKC performs well on large problems from the TPTP set, the system is built for use as a core system for developing a toolset of commonsense reasoning functionalities.

ABSTRACT. We describe a new tool, AGES, which is able to automatically generate models for order-sorted first-order theories. The tool systematically exploits (and relies on) the use of convex domains to associate domains to the different sorts; we use them to interpret the ranked symbols of order-sorted signatures and also the (also ranked) predicate symbols in the language by means of appropriately adapted piecewise convex matrix interpretations. Relations interpreting binary predicates can be specified to be well-founded as an additional requirement for the generation of the model. The system is available as a web application.

ABSTRACT. E 2.3 is a theorem prover for many-sorted first-order logic with equality. We describe the basic logical and software architecture of the system, as well as core features of the implementation. We particularly discuss recently added features and extensions, including the extension to many-sorted logic, optional limited support for higher-order logic, and the integration of SAT techniques via PicoSAT. Minor additions include improved support for TPTP standard features, always-on internal proof objects, and lazy orphan removal. The paper also gives an overview of the performance of the system, and describes ongoing and future work.

ABSTRACT. This paper describes an ATP system, named JGXYZ, for some gap and glut logics. JGXYZ is based on an equi-provable translation to FOL, followed by use of an existing ATP system for FOL. A key feature of JGXYZ is that the translation to FOL is data-driven, in the sense that it requires only the addition of a new logic's truth tables for the unary and binary connectives in order to produce an ATP system for the logic. Experimental results from JGXYZ illustrate the differences between the logics and translated problems, both technically and in terms of a quasi-real-world use case.