scholarly journals Rewriting and Well-Definedness within a Proof System

10.29007/b7wc ◽  
2018 ◽  
Author(s):  
Issam Maamria ◽  
Michael Butler
Keyword(s):  
Theorem Proving ◽  
Automated Theorem Proving ◽  
Term Rewriting ◽  
Proof System ◽  
Proof Technique ◽  
Partial Functions ◽  
Deductive Proof ◽  
Theorem Provers ◽  
Theoretical Foundations

Term rewriting has a significant presence in various areas, not least in automated theorem proving where it is used as a proof technique. Many theorem provers employ specialised proof tactics for rewriting. This results in an interleaving between deduction and computation (i.e., rewriting) steps. If the logic of reasoning supports partial functions, it is necessary that rewriting copes with potentially ill-defined terms. In this paper, we provide a basis for integrating rewriting with a deductive proof system that deals with well-definedness. The definitions and theorems presented in this paper are the theoretical foundations for an extensible rewriting-based prover that has been implemented for the set theoretical formalism Event-B.

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 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.

scholarly journals Proof simplification and automated theorem proving

2019 ◽  
Vol 377 (2140) ◽  
pp. 20180034 ◽  
Author(s):  
Michael Kinyon
Keyword(s):  
Theorem Proving ◽  
Simple Proof ◽  
Automated Theorem Proving ◽  
Theme Issue ◽  
Theorem Provers ◽  
Open Question

The proofs first generated by automated theorem provers are far from optimal by any measure of simplicity. In this paper, I describe a technique for simplifying automated proofs. Hopefully, this discussion will stimulate interest in the larger, still open, question of what reasonable measures of proof simplicity might be. This article is part of the theme issue ‘The notion of ‘simple proof’ - Hilbert's 24th problem’.

scholarly journals PROVA AUTOMATIZADA DE TEOREMA EM LÓGICA PROPOSICIONAL

e-xacta ◽  
2013 ◽  
Vol 6 (1) ◽  
pp. 83
Author(s):  
Frederico Martins Biber Sampaio ◽  
Moisés Henrique Ramos Pereira
Keyword(s):  
Theorem Proving ◽  
Propositional Logic ◽  
Automated Theorem Proving ◽  
Proof Methods ◽  
Operational Issues ◽  
Theoretical Foundations

<p align="justify">Este trabalho aborda o desenvolvimento de um sistema para prova automatizada de teoremas em lógica proposicional. O artigo apresenta os fundamentos teóricos gerais, questões operacionais e a estrutura de um software de prova de teoremas, elaborado com propósitos acadêmicos e didáticos, utilizando métodos de prova baseados em três tipos de tableaux semânticos: tableau de Smullyan, tableau com Lema e tableau KE. Experimentos foram realizados para verificar a correção dos resultados das provas, utilizando fórmulas geradas automaticamente.</p><p align="justify">Abstract</p><p align="justify">This work describes the development of an automated theorem proving system of propositional logic. The paper presents the theoretical foundations, operational issues and structure of a theorem proving software, developed with academic and didactic purposes, using proof methods based on three semantics tableaux: Smullyan tableau, Lema tableau e KE tableau. Experiments were performed to verify the correctness of the results of the proofs, using automatically generating formulas.</p>

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.

scholarly journals The term rewriting approach to automated theorem proving

1992 ◽  
Vol 14 (1-2) ◽  
pp. 71-99 ◽  
Author(s):  
Jieh Hsiang ◽  
Hélène Kirchner ◽  
Pierre Lescanne ◽  
Michaël Rusinowitch
Keyword(s):  
Theorem Proving ◽  
Automated Theorem Proving ◽  
Term Rewriting

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.

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.

Sign in / Sign up

Export Citation Format

Share Document