Search

The CADE ATP System Competition (CASC) is the annual evaluation of fully automatic, classical logic, Automated Theorem Proving (ATP) systems – the world championship for such systems. CASC-29 was the twenty-eighth competition in the CASC series. Twenty-four ATP systems competed in the various divisions. This paper presents an outline of the competition design and a commentated summary of the results. [ABSTRACT FROM AUTHOR]

We present recent developments in the applications of automated theorem proving in the investigation of the Andrews–Curtis conjecture. We demonstrate previously unknown trivializations of group presentations from a parametric family MSn(w∗) of trivial group presentations for n=3,4,5,6,7,8 (subset of well-known Miller–Schupp family). Based on the human analysis of these trivializations we formulate two conjectures on the structure of simplifications for the infinite family MSn(w∗), n≥3.

This paper establishes a connection between control theory for partially observed discrete-event systems (DESs) and automated theorem proving (ATP) in the calculus of positively constructed formulas (PCFs). The language of PCFs is a complete first-order language providing a powerful tool for qualitative analysis of dynamical systems. Based on ATP in the PCF calculus, a new technique is suggested for checking observability as a property of formal languages, which is necessary for the existence of supervisory control of DESs. In the case of violation of observability, words causing a conflict can also be extracted with the help of a specially designed PCF. With an example of the problem of path planning by a robot in an unknown environment, we show the application of our approach at one of the levels of a robot control system. The prover Bootfrost developed to facilitate PCF refutation is also presented. The tests show positive results and perspectives for the presented approach. [ABSTRACT FROM AUTHOR]

The article is devoted to the development of an approach to solving the main problems of the theory of supervisory control of logical discrete-event systems (DES), based on their representation in the form of positively constructed formulas (PCF). We consider logical DESs in automata form, understood as generators of some regular languages. The PCF language is a complete first-order language, the formulas of which have a regular structure of alternating type quantifiers and do not contain a negation operator in the syntax. It was previously proven that any formula of the classical first-order predicate calculus can be represented as a PCF. PCFs have a visual tree representation and a natural question-and-answer procedure for searching for an inference using a single inference rule. It is shown how the PCF calculus, developed in the 1990s to solve some problems of control of dynamic systems, makes it possible to solve basic problems of the theory of supervisory control, such as checking the criteria for the existence of supervisory control, automatically modifying restrictions on the behavior of the controlled system, and implementing a supervisor. Due to some features of the PCF calculus, it is possible to use a non-monotonic inference. It is demonstrated how the presented PCF-based method allows for additional event processing during inference. The Bootfrost software system, or the so-called prover, designed to refute the obtained PCFs is also presented, and the features of its implementation are briefly described. As an illustrative example, we consider the problem of controlling an autonomous mobile robot.

The logico-pluralist LogiKEy knowledge engineering methodology and framework is applied to the modelling of a theory of legal balancing, in which legal knowledge (cases and laws) is encoded by utilising context-dependent value preferences. The theory obtained is then used to formalise, automatically evaluate, and reconstruct illustrative property law cases (involving the appropriation of wild animals) within the Isabelle/HOL proof assistant system, illustrating how LogiKEy can harness interactive and automated theorem-proving technology to provide a testbed for the development and formal verification of legal domain-specific languages and theories. Modelling value-oriented legal reasoning in that framework, we establish novel bridges between the latest research in knowledge representation and reasoning in non-classical logics, automated theorem proving, and applications in legal reasoning. [ABSTRACT FROM AUTHOR]

We present an automatic theorem prover for projective incidence geometry. This prover does not consider coordinates. Instead, it follows a combinatorial approach based on the concept of rank. This allows to deal only with sets of points and to capture relations between objects of the projective space (equality, collinearity, coplanarity, etc.) in a homogenous way. Taking advantage of the computational aspect of this approach, we automatically compute by saturation the ranks of all sets of the powerset of the points of the geometric configuration we consider. Upon completion of the saturation phase, our prover then retraces the proof process and generates the corresponding Coq code. This code is then formally checked by the Coq proof assistant, thus ensuring that the proof is actually correct. We use the prover to verify some well-known, non-trivial theorems in projective space geometry, among them: Desargues’ theorem and Dandelin–Gallucci’s theorem. [ABSTRACT FROM AUTHOR]

Computer assisted theorem proving is an increasingly important part of mathematical methodology, as well as a long-standing topic in artificial intelligence (AI) research. However, the current generation of theorem proving software have limited functioning in terms of providing new proofs. Importantly, they are not able to discriminate interesting theorems and proofs from trivial ones. In order for computers to develop further in theorem proving, there would need to be a radical change in how the software functions. Recently, machine learning results in solving mathematical tasks have shown early promise that deep artificial neural networks could learn symbolic mathematical processing. In this paper, I analyze the theoretical prospects of such neural networks in proving mathematical theorems. In particular, I focus on the question how such AI systems could be incorporated in practice to theorem proving and what consequences that could have. In the most optimistic scenario, this includes the possibility of autonomous automated theorem provers (AATP). Here I discuss whether such AI systems could, or should, become accepted as active agents in mathematical communities. [ABSTRACT FROM AUTHOR]

In this paper, we investigate some polynomial conditions that arise from Euclidean geometry. First we study polynomials related to quadrilaterals with supplementary angles, this includes convex cyclic quadrilaterals, as well as certain concave quadrilaterals. Then we consider polynomials associated with quadrilaterals with some equal angles, which include convex and concave tilted kites. Some of the results are proved using Groebner bases computations. [ABSTRACT FROM AUTHOR]

This paper establishes a connection between control theory for partially observed discrete-event systems (DESs) and automated theorem proving (ATP) in the calculus of positively constructed formulas (PCFs). The language of PCFs is a complete first-order language providing a powerful tool for qualitative analysis of dynamical systems. Based on ATP in the PCF calculus, a new technique is suggested for checking observability as a property of formal languages, which is necessary for the existence of supervisory control of DESs. In the case of violation of observability, words causing a conflict can also be extracted with the help of a specially designed PCF. With an example of the problem of path planning by a robot in an unknown environment, we show the application of our approach at one of the levels of a robot control system. The prover Bootfrost developed to facilitate PCF refutation is also presented. The tests show positive results and perspectives for the presented approach.

Jan von Plato proposed in 1998 an intuitionist axiomatization of ordered affine geometry consisting of 22 axioms. It is shown that axiom I.7, which is equivalent to a conjunction of four statements, two of which are redundant, can be replaced with a simpler axiom, which is von Plato's Theorem 3.10. [ABSTRACT FROM AUTHOR]

General mathematical reasoning is computationally undecidable, but humans routinely solve new problems. Moreover, discoveries developed over centuries are taught to subsequent generations quickly. What structure enables this, and how might that inform automated mathematical reasoning? We posit that central to both puzzles is the structure of procedural abstractions underlying mathematics. We explore this idea in a case study on five sections of beginning algebra on the Khan Academy platform. To define a computational foundation, we introduce Peano, a theorem-proving environment where the set of valid actions at any point is finite. We use Peano to formalize introductory algebra problems and axioms, obtaining well-defined search problems. We observe existing reinforcement learning methods for symbolic reasoning to be insufficient to solve harder problems. Adding the ability to induce reusable abstractions ('tactics') from its own solutions allows an agent to make steady progress, solving all problems. Furthermore, these abstractions induce an order to the problems, seen at random during training. The recovered order has significant agreement with the expert-designed Khan Academy curriculum, and second-generation agents trained on the recovered curriculum learn significantly faster. These results illustrate the synergistic role of abstractions and curricula in the cultural transmission of mathematics. This article is part of a discussion meeting issue 'Cognitive artificial intelligence'. [ABSTRACT FROM AUTHOR]

The CADE ATP System Competition (CASC) is the annual evaluation of fully automatic, classical logic, Automated Theorem Proving (ATP) systems. CASC-J11 was the twenty-seventh competition in the CASC series. Twenty-four ATP systems competed in the various competition divisions. This paper presents an outline of the competition design and a commentated summary of the results. [ABSTRACT FROM AUTHOR]

AVATAR is an elegant and effective way to split clauses in a saturation prover using a SAT solver. But is it refutationally complete? And how does it relate to other splitting architectures? To answer these questions, we present a unifying framework that extends a saturation calculus (e.g., superposition) with splitting and that embeds the result in a prover guided by a SAT solver. The framework also allows us to study locking, a subsumption-like mechanism based on the current propositional model. Various architectures are instances of the framework, including AVATAR, labeled splitting, and SMT with quantifiers. [ABSTRACT FROM AUTHOR]

Generally, the negation-limited inverters problem is a puzzle of constructing an inverter with AND gates and OR gates, and a few inverters. This paper introduces a curious new result about the effectiveness of two powerful ATP (Automated Theorem Proving) strategies in tackling negation-limited inverter problems. Two resolution strategies are UR (Unit Resulting) resolution and Hyper-Resolution. In the experiment, we cope with two kinds of automated circuit construction: three input/output inverters and four input/output BCD Counter Circuit. Both circuits are constructed with a few limited inverters. Curiously, it has been turned out that UR resolution is drastically faster than Hyper-Resolution in the measurement of the size of SoS (Set of Support). Besides, we discuss the syntactic and semantic criteria, which might cause a considerable difference in computation cost between UR resolution and Hyper-Resolution. [ABSTRACT FROM AUTHOR]

We introduce an experimental version of GeoGebra that successfully conjectures and proves a large scale of geometric inequalities by providing an easy-to-use graphical interface. GeoGebra Discovery includes an embedded version of the Tarski/QEPCAD B system which can solve a real quantifier elimination problem, so the input geometric construction can be translated into a semi-algebraic system, and after some algebraic manipulations, the obtained formula can be translated back to a precisely stated geometric inequality. We provide some non-trivial examples to illustrate the performance of GeoGebra Discovery when dealing with inequalities, as well as some technical difficulties. [ABSTRACT FROM AUTHOR]

In contrast to common automated theorem proving approaches, in which the search space is a set of some formulae and what is sought is again a (goal) formula, we propose an approach based on searching for a proof (of a given length) as a whole. Namely, a proof of a formula in a fixed logical setting can be encoded as a sequence of natural numbers meeting some conditions and a suitable constraint solver can find such a sequence. The sequence can then be decoded giving a proof in the original theory language. This approach leads to several unique features, for instance, it can provide shortest proofs. In this paper, we focus on proofs in coherent logic, an expressive fragment of first-order logic, and on SAT and SMT solvers for solving sets of constraints, but the approach could be tried in other contexts as well. We implemented the proposed method and we present its features, perspectives and performances. One of the features of the implemented prover is that it can generate human understandable proofs in natural language and also machine-verifiable proofs for the interactive prover Coq. [ABSTRACT FROM AUTHOR]

A crucial operation of saturation theorem provers is deletion of subsumed formulas. Designers of proof calculi, however, usually discuss this only informally, and the rare formal expositions tend to be clumsy. This is because the equivalence of dynamic and static refutational completeness holds only for derivations where all deleted formulas are redundant, but the standard notion of redundancy is too weak: A clause C does not make an instance C σ redundant. We present a framework for formal refutational completeness proofs of abstract provers that implement saturation calculi, such as ordered resolution and superposition. The framework modularly extends redundancy criteria derived via a familiar ground-to-nonground lifting. It allows us to extend redundancy criteria so that they cover subsumption, and also to model entire prover architectures so that the static refutational completeness of a calculus immediately implies the dynamic refutational completeness of a prover implementing the calculus within, for instance, an Otter or DISCOUNT loop. Our framework is mechanized in Isabelle/HOL. [ABSTRACT FROM AUTHOR]

In his regular column in the AAR Newsletter, Larry Wos typically posed challenges to the automated reasoning community. Some of these challenges concern general research objectives, but several of them concern specific problems relevant to his own experience and attempts to solve especially difficult problems, including open questions, with an automated theorem prover. This note honors Larry's memory by working through a solution to one of these challenges. [ABSTRACT FROM AUTHOR]

The TLA+ Proof System (TLAPS) allows users to verify proofs with the support of automated theorem provers, including SMT solvers. To increase trust in TLAPS, we revisited the encoding of TLA+ for SMT, whose implementation had become too complex. Our approach is based on a first-order axiomatization with E-matching patterns. The new encoding is available with TLAPS and achieves performances similar to the previous version, despite its simpler design. [ABSTRACT FROM AUTHOR]

Tarski showed in the 1950s that (first-order) questions in Euclidean geometry could be answered algorithmically. Algorithms for doing this have greatly improved over the decades but still have high complexity (in terms of time taken). We experiment using state-of-the-art software, specifically so-called SMT Solvers, to see how practical it is to prove classical Euclidean geometry results in this way. [ABSTRACT FROM AUTHOR]

Premise selection is a task that selects likely useful premises from a large-scale premise set, which is one of the challenges for automated theorem proving. Nowadays, using graph neural networks to encode logical formulae becomes more and more appealing, as graph representations demonstrate the ability to preserve the semantic and syntactic information of logical formulae. However, graph neural networks in the prior works iteratively update each node's embedding via information aggregated solely from its neighbors and always ignore the types of nodes. Besides, evidence shows that sharing and exchanging some information between formula pairs can ensure neural-based models more robust in measuring graph relevance. Unluckily, previous graph neural networks generate final graph embeddings independently in the premise selection task. To overcome these shortages, we propose a novel graph neural network, called ARCG-NN, for embedding the first-order logical formulae. The embedding model firstly takes the node types into full consideration and utilizes an attention mechanism based on newly proposed node types to compute weights in the message aggregation. Except for the message from the local neighborhood, ARCG-NN also dynamically exchange the cross-graph information of particular nodes along with the propagation rounds. Besides, an extra gate function on node types is used to filter out irrelevant information in the graph aggregation phase. To train, validate, and test our approach, we build balanced and unbalanced datasets based on the MPTP2078 benchmark. The experimental results demonstrate that the proposed graph neural architecture achieves state-of-the-art classification accuracy on the first-order premise selection task and helps the automated theorem prover E prove more problems in the test dataset. [ABSTRACT FROM AUTHOR]