scholarly journals Defining the meaning of TPTP formatted proofs

10.29007/xtc2 ◽  
2018 ◽  
Author(s):  
Roberto Blanco ◽  
Tomer Libal ◽  
Dale Miller
Keyword(s):  
Theorem Proving ◽  
Automated Theorem Proving ◽  
Inference Rules ◽  
First Order ◽  
Theorem Provers

The TPTP library is one of the leading problem libraries in the automated theorem proving community. Along the years, support was added for problems beyond those in first-order clausal form. Another addition was the augmentation of the language to support proofs outputted from theorem provers and the maintenance of a proof library, called TSTP. In this paper we propose another augmentation of the language for the support of the semantics of the inference rules used in these proofs.

scholarly journals Integer Induction in Saturation

2021 ◽  
pp. 361-377
Author(s):  
Petra Hozzová ◽  
Laura Kovács ◽  
Andrei Voronkov
Keyword(s):  
Theorem Proving ◽  
Program Analysis ◽  
State Of The Art ◽  
Inductive Reasoning ◽  
Theorem Prover ◽  
Inference Rules ◽  
First Order ◽  
Theorem Provers ◽  
Mathematical Properties

AbstractIntegers are ubiquitous in programming and therefore also in applications of program analysis and verification. Such applications often require some sort of inductive reasoning. In this paper we analyze the challenge of automating inductive reasoning with integers. We introduce inference rules for integer induction within the saturation framework of first-order theorem proving. We implemented these rules in the theorem prover Vampire and evaluated our work against other state-of-the-art theorem provers. Our results demonstrate the strength of our approach by solving new problems coming from program analysis and mathematical properties of integers.

scholarly journals Understanding LEO-II’s proofs

10.29007/x9c9 ◽  
2018 ◽  
Author(s):  
Nik Sultana ◽  
Christoph Benzmüller
Keyword(s):  
Theorem Proving ◽  
Automated Theorem Proving ◽  
Higher Order ◽  
Target Audience ◽  
Theorem Prover ◽  
First Order

The LEO and LEO-II provers have pioneered the integration of higher-order and first-order automated theorem proving. To date, the LEO-II system is, to our knowledge, the only automated higher-order theorem prover which is capable of generating joint higher-order–first-order proof objects in TPTP format. This paper discusses LEO-II’s proof objects. The target audience are practitioners with an interest in using LEO-II proofs within other systems.

scholarly journals Checkable Proofs for First-Order Theorem Proving

10.29007/s6d1 ◽  
2018 ◽  
Author(s):  
Giles Reger ◽  
Martin Suda
Keyword(s):  
Theorem Proving ◽  
Critical Mass ◽  
Current Situation ◽  
Boolean Satisfiability ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Theorem Provers ◽  
Interactive Theorem Provers ◽  
Theory Reasoning

Inspired by the success of the DRAT proof format for certification of boolean satisfiability (SAT),we argue that a similar goal of having unified automatically checkable proofs should be soughtby the developers of automated first-order theorem provers (ATPs). This would not onlyhelp to further increase assurance about the correctness of prover results,but would also be indispensable for tools which rely on ATPs,such as ``hammers'' employed within interactive theorem provers.The current situation, represented by the TSTP format is unsatisfactory,because this format does not have a standardised semantics and thus cannot be checked automatically.Providing such semantics, however, is a challenging endeavour. One would ideallylike to have a proof format which covers only-satisfiability-preserving operations such as Skolemisationand is versatile enough to encompass various proving methods (i.e. not just superposition)or is perhaps even open ended towards yet to be conceived methods or at least easily extendable in principle.Going beyond pure first-order logic to theory reasoning in the style of SMT orbeyond proofs to certification of satisfiability are further interesting challenges.Although several projects have already provided partial solutions in this direction,we would like to use the opportunity of ARCADE to further promote the idea andgather critical mass needed for its satisfactory realisation.

scholarly journals Problem Libraries for Non-Classical Logics

10.29007/mkdw ◽  
2018 ◽  
Author(s):  
Jens Otten ◽  
Thomas Raths
Keyword(s):  
Theorem Proving ◽  
General Problem ◽  
Crucial Role ◽  
Automated Theorem Proving ◽  
Modal Logics ◽  
First Order ◽  
Problem Library ◽  
Future Plans

Problem libraries for automated theorem proving (ATP) systems play a crucial role when developing, testing, benchmarking and evaluating ATP systems for classical and non-classical logics. We provide an overview of existing problem libraries for some important non-classical logics, namely first-order intuitionistic and first-order modal logics. We suggest future plans to extend these existing libraries and discuss ideas for a general problem library platform for non-classical logics.

scholarly journals Different Proofs are Good Proofs

10.29007/kwk9 ◽  
2018 ◽  
Author(s):  
Geoff Sutcliffe ◽  
Cynthia Chang ◽  
Li Ding ◽  
Deborah McGuinness ◽  
Paulo Pinheiro da Silva
Keyword(s):  
Theorem Proving ◽  
Automated Theorem Proving ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Problem Library

In order to compare the quality of proofs, it is necessary to measure artifacts of the proofs, and evaluate the measurements to determine differences between the proofs. This paper discounts the approach of ranking measurements of proof artifacts, and takes the position that different proofs are good proofs. The position is based on proofs in the TSTP solution library, which are generated by Automated Theorem Proving (ATP) systems applied to first-order logic problems in the TPTP problem library.

STRATEGY PARALLELISM IN AUTOMATED THEOREM PROVING

1999 ◽  
Vol 13 (02) ◽  
pp. 219-245 ◽  
Author(s):  
ANDREAS WOLF ◽  
REINHOLD LETZ
Keyword(s):  
Theorem Proving ◽  
Experimental Evaluation ◽  
Automated Theorem Proving ◽  
Search Strategies ◽  
Theorem Prover ◽  
Strategy Selection ◽  
Theorem Provers ◽  
Initial Strategy ◽  
Basic Concepts ◽  
Run Time

Automated theorem provers use search strategies. Unfortunately, there is no unique strategy which is uniformly successful on all problems. This motivates us to apply different strategies in parallel, in a competitive manner. In this paper, we discuss properties, problems, and perspectives of strategy parallelism in theorem proving. We develop basic concepts like the complementarity and the overlap value of strategy sets. Some of the problems such as initial strategy selection and run-time strategy exchange are discussed in more detail. The paper also contains the description of an implementation of a strategy parallel theorem prover (p-SETHEO) and an experimental evaluation.

scholarly journals The Thousands of Models for Theorem Provers (TMTP) Model Library - First Steps

10.29007/7dg5 ◽  
2018 ◽  
Author(s):  
Geoff Sutcliffe ◽  
Stephan Schulz
Keyword(s):  
Theorem Proving ◽  
Automated Theorem Proving ◽  
Theorem Provers ◽  
Model Library ◽  
Problems And Solutions ◽  
Model Finding ◽  
Problem Library

The TPTP World is a well established infrastructure that supports research,development, and deployment of Automated Theorem Proving (ATP) systems forclassical logics.The TPTP world includes the TPTP problem library, the TSTP solution library,standards for writing ATP problems and reporting ATP solutions, and itprovides tools and services for processing ATP problems and solutions.This work describes a new component of the TPTP world - the Thousands ofModels for Theorem Provers (TMTP) Model Library.This is a library of models for identified axiomatizations built fromaxiom sets in the TPTP problem library, along with functions for efficientlyevaluating formulae wrt models, and tools for examining and processingthe models.The TMTP supports the development of semantically guided theorem provingATP systems, provide examples for developers of model finding ATP systems,and provides insights into the semantics of axiomatizations.

scholarly journals SGGS Theorem Proving: an Exposition

10.29007/m2vf ◽  
2018 ◽  
Author(s):  
Maria Paola Bonacina ◽  
David Plaisted
Keyword(s):  
Theorem Proving ◽  
Order Logic ◽  
First Order Logic ◽  
Candidate Model ◽  
Narrative Style ◽  
First Order ◽  
The Core ◽  
Theorem Provers ◽  
Instance Generation ◽  
Main Ideas

We present in expository style the main ideas in SGGS, which stands for Semantically-Guided Goal-Sensitive theorem proving. SGGS uses sequences of constrained clauses to represent models, instance generation to go from a candidate model to the next, and resolution as well as other inferences to repair the model. SGGS is refutationally complete for first-order logic, DPLL-style model based, semantically guided, goal sensitive, and proof confluent, which appears to be a rare combination of features. In this paper we describe the core of SGGS in a narrative style, emphasizing ideas and trying to keep technicalities to a minimum, in order to advertise it to builders and users of theorem provers.

scholarly journals Automated Theorem Proving using the TPTP Process Instruction Language

10.29007/f997 ◽  
2018 ◽  
Author(s):  
Muhammad Nassar ◽  
Geoff Sutcliffe
Keyword(s):  
Theorem Proving ◽  
Automated Theorem Proving ◽  
Input Output ◽  
Theorem Provers ◽  
And Control

The TPTP (Thousands of Problems for Theorem Provers) World is a well established infrastructure for Automated Theorem Proving (ATP). In the context of the TPTP World, the TPTP Process Instruction (TPI) language provides capabilities to input, output and organize logical formulae, and control the execution of ATP systems. This paper reviews the TPI language, describes a shell interpreter for the language, and demonstrates their use in theorem proving.

Sign in / Sign up

Export Citation Format

Share Document