A case study in automated theorem proving: Finding sages in combinatory logic

1987 ◽  
Vol 3 (1) ◽  
pp. 91-107 ◽  
Author(s):  
William McCune ◽  
Larry Wos
Keyword(s):  
Theorem Proving ◽  
Automated Theorem Proving ◽  
Combinatory Logic

scholarly journals Bayesian Optimisation for Heuristic Configuration in Automated Theorem Proving

10.29007/q91g ◽  
2020 ◽  
Author(s):  
Agnieszka Słowik ◽  
Chaitanya Mangla ◽  
Mateja Jamnik ◽  
Sean Holden ◽  
Lawrence Paulson
Keyword(s):  
Theorem Proving ◽  
Automated Theorem Proving ◽  
Probabilistic Framework ◽  
Selection Algorithm ◽  
Formal Proofs ◽  
Proof Search ◽  
Minimum Number ◽  
Selection Algorithms

Modern theorem provers such as Vampire utilise premise selection algorithms to control the proof search explosion. Premise selection heuristics often employ an array of continuous and discrete parameters. The quality of recommended premises varies depending on the parameter assignment. In this work, we introduce a principled probabilistic framework for optimisation of a premise selection algorithm. We present results using Sumo Inference Engine (SInE) and the Archive of Formal Proofs (AFP) as a case study. Our approach can be used to optimise heuristics on large theories in minimum number of steps.

scholarly journals Bayesian Optimisation for Premise Selection in Automated Theorem Proving (Student Abstract)

2020 ◽  
Vol 34 (10) ◽  
pp. 13919-13920
Author(s):  
Agnieszka Słowik ◽  
Chaitanya Mangla ◽  
Mateja Jamnik ◽  
Sean B. Holden ◽  
Lawrence C. Paulson
Keyword(s):  
Parameter Space ◽  
Theorem Proving ◽  
Automated Theorem Proving ◽  
Search Space ◽  
Large Set ◽  
Probabilistic Framework ◽  
Formal Proofs ◽  
Dimensional Parameter ◽  
Theorem Provers

Modern theorem provers utilise a wide array of heuristics to control the search space explosion, thereby requiring optimisation of a large set of parameters. An exhaustive search in this multi-dimensional parameter space is intractable in most cases, yet the performance of the provers is highly dependent on the parameter assignment. In this work, we introduce a principled probabilistic framework for heuristic optimisation in theorem provers. We present results using a heuristic for premise selection and the Archive of Formal Proofs (AFP) as a case study.

The 10th IJCAR automated theorem proving system competition – CASC-J10

2021 ◽  
pp. 1-15
Author(s):  
Geoff Sutcliffe
Keyword(s):  
Theorem Proving ◽  
Classical Logic ◽  
Automated Theorem Proving ◽  
Fully Automatic

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

Retrieval System and Dynamic Algorithm Looking for Axioms of Notions Defined by Programs

1993 ◽  
Vol 19 (3-4) ◽  
pp. 275-301
Author(s):  
Andrzej Biela
Keyword(s):  
Theorem Proving ◽  
Dynamic Process ◽  
Functional Equations ◽  
Automated Theorem Proving ◽  
Retrieval System ◽  
Formal System ◽  
Dynamic Algorithm ◽  
Algorithmic Logic ◽  
Correctness Of Programs

In this paper we shall introduce a formal system of algorithmic logic which enables us to formulate some problems connected with a retrieval system which provides a comprehensive tool in automated theorem proving of theorems consisting of programs, procedures and functions. The procedures and functions may occur in considered theorems while the program of the above mentioned system is being executed. We can get an answer whether some relations defined by programs hold and we can prove functional equations in a dynamic way by looking for a special set of axioms /assumptions/ during the execution of system. We formulate RS-algorithm which enables us to construct the set of axioms for proving some properties of functions and relations defined by programs. By RS-algorithm we get the dynamic process of proving functional equations and we can answer the question whether some relations defined by programs hold. It enables us to solve some problems concerning the correctness of programs. This system can be used for giving an expert appraisement. We shall provide the major structures and a sketch of an implementation of the above formal system.

Sign in / Sign up

Export Citation Format

Share Document