As a present to Mizar on its 50th anniversary, we develop an AI/TP system that automatically proves about 60% of the Mizar theorems in the hammer setting. We also automatically prove 75% of the Mizar theorems when the automated provers are helped by using only the premises used in the human-written Mizar proofs. We describe the methods and large-scale experiments leading to these results. This includes in particular the E and Vampire provers, their ENIGMA and Deepire learning modifications, a number of learning-based premise selection methods, and the incremental loop that interleaves growing a corpus of millions of ATP proofs with training increasingly strong AI/TP systems on them. We also present a selection of Mizar problems that were proved automatically.

Abstract Most users of proof assistants want more proof automation. Some proof assistants discharge goals by translating them to first-order logic and invoking an efficient prover on them, but much is lost in translation. Instead, we propose to extend first-order provers with native support for higher-order features. Building on our extension of E to $$\lambda $$ -free higher-order logic, we extend E to full higher-order logic. The result is the strongest prover on benchmarks exported from a proof assistant.

Abstract Decades of work have gone into developing efficient proof calculi, data structures, algorithms, and heuristics for first-order automatic theorem proving. Higher-order provers lag behind in terms of efficiency. Instead of developing a new higher-order prover from the ground up, we propose to start with the state-of-the-art superposition prover E and gradually enrich it with higher-order features. We explain how to extend the prover’s data structures, algorithms, and heuristics to $$\lambda $$ λ -free higher-order logic, a formalism that supports partial application and applied variables. Our extension outperforms the traditional encoding and appears promising as a stepping stone toward full higher-order logic.

This special issue of the Journal of Automated Reasoning is dedicated to selected papers presented at the 9th Joint Conference on Automated Reasoning (IJCAR 2018), held between July 14 and July 17, 2018 in Oxford, UK, as part of the Federated Logic Conference (FLOC) 2018.IJCAR is the premier international joint conference on all topics in automated reasoning and merges three leading events in automated reasoning: CADE (Conference on Automated Deduction), FroCoS (Symposium on Frontiers of Combining Systems), and TABLEAUX (Conference on Analytic Tableaux and Related Methods).The papers selected for this special issue underwent a two-round reviewing process.In the first round, the papers had been reviewed and accepted by at least three reviewers as part of the IJCAR 2018 reviewing process.We invited authors of top rated papers in the proceedings as evaluated by the reviewers to submit revised and extended versions of their papers to this special issue.In the second round, the submitted extended papers went through the reviewing process of the Journal of Automated Reasoning.Each paper was reviewed by two reviewers.The seven selected papers in this special issue cover a wide spectrum of topics in Automated Reasoning, from proof theory and theorem proving to formalization and mechanization of completeness or decidability results, from proof systems to analysis of complexity and decidability, from automated reasoning to the production of stateful ML programs together with proofs of correctness, from extensions of model checking techniques to the verification of some parameterized systems.The paper "Formalizing Bachmair and Ganzinger's Ordered Resolution Prover" presents a formalization of the first half of Bachmair and Ganzinger's chapter on resolution theorem proving in Isabelle/HOL, providing a refutationally complete first-order prover based on ordered resolution with literal selection.It proposes general infrastructure and methodology that can form the basis of completeness proofs for related calculi, including superposition.The paper "Constructive Decision via Redundancy-free Proof-Search" presents a constructive account of Kripke-Curry's method used to establish the decidability of Implicational Relevance Logic (R → ).The method is mechanized in axiom-free Coq, with the replacement of Kripke/Dickson's lemma by a constructive form of Ramsey's theorem and of König's B

Decades of work have gone into developing efficient proof calculi, data structures, algorithms, and heuristics for first-order automatic theorem proving. Higher-order provers lag behind in terms of efficiency. Instead of developing a new higher-order prover from the ground up, we propose to start with the state-of-the-art superposition-based prover E and gradually enrich it with higher-order features. We explain how to extend the prover’s data structures, algorithms, and heuristics to $$\lambda $$ -free higher-order logic, a formalism that supports partial application and applied variables. Our extension outperforms the traditional encoding and appears promising as a stepping stone towards full higher-order logic.

Program analysis and verification require decision procedures to reason on theories of data structures. Many problems can be reduced to the satisfiability of sets of ground literals in theory T . If a sound and complete inference system for first-order logic is guaranteed to terminate on T-satisfiability problems , any theorem-proving strategy with that system and a fair search plan is a T-satisfiability procedure . We prove termination of a rewrite-based first-order engine on the theories of records , integer offsets , integer offsets modulo and lists . We give a modularity theorem stating sufficient conditions for termination on a combination of theories , given termination on each. The above theories, as well as others, satisfy these conditions. We introduce several sets of benchmarks on these theories and their combinations, including both parametric synthetic benchmarks to test scalability , and real-world problems to test performances on huge sets of literals. We compare the rewrite-based theorem prover E with the validity checkers CVC and CVC Lite. Contrary to the folklore that a general-purpose prover cannot compete with reasoners with built-in theories, the experiments are overall favorable to the theorem prover, showing that not only the rewriting approach is elegant and conceptually simple, but has important practical implications.