scholarly journals Automated Reasoning in the Simulation of Evolvable Systems

10.29007/jj86 ◽  
2018 ◽  
Author(s):  
Djihed Afifi ◽  
David Rydeheard ◽  
Howard Barringer
Keyword(s):  
Theorem Proving ◽  
Automated Theorem Proving ◽  
Rapid Assessment ◽  
Theorem Prover ◽  
System Description ◽  
Large Sets ◽  
Simulation Engine ◽  
Meta Level ◽  
Almost All ◽  
Computational Systems

We present a novel application of automated theorem proving for the simulation of computational systems. The computational systems we consider are evolvable, i.e. may reconfigure their structure and programs at run-time. In [1], a logical framework for describing such systems is introduced. The underlying logic of this framework allows us to build a simulation engine for executing system specifications. This engine makes intensive use of automated theorem proving – when running a simulation, almost all computational steps are those of a theorem prover. In this paper, we present this novel combination of a logical setting involving meta-level logics and large sets of formulae for system description, together with theorem proving requirements which involve often slowly changing specifications with the need for rapid assessment of deducibility and consistency. We will evaluate the suitability of several theorem provers for this application.

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.

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 Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics

10.29007/kvb1 ◽  
2018 ◽  
Author(s):  
Negin Arhami ◽  
Geoff Sutcliffe
Keyword(s):  
Theorem Proving ◽  
Automated Theorem Proving ◽  
The Other ◽  
Theorem Prover ◽  
Trade Off ◽  
Other Hand ◽  
Automated Theorem Prover

Many Automated Theorem Prover (ATP) systems for different logics, andtranslators for translating different logics from one to another, havebeen developed and are now available.Some logics are more expressive than others, and it is easier to expressproblems in those logics.On the other hand, the ATP systems for less expressive logics have beenunder development for many years, and are more powerful and reliable.There is a trade-off between expressivity of a logic, and the power andreliability of the available ATP systems.Translators and ATP systems can be combined to try to solvea problem.In this research, an experiment has been carried out to compare theperformance of difference combinations of translators and ATP systems.

scholarly journals Checking the quality of clinical guidelines using automated reasoning tools

2008 ◽  
Vol 8 (5-6) ◽  
pp. 611-641 ◽  
Author(s):  
ARJEN HOMMERSOM ◽  
PETER J. F. LUCAS ◽  
PATRICK VAN BOMMEL
Keyword(s):  
Theorem Proving ◽  
Clinical Guidelines ◽  
Automated Reasoning ◽  
Automated Theorem Proving ◽  
Interactive Theorem Proving ◽  
Theorem Prover ◽  
First Order ◽  
Medical Quality ◽  
Diabetes Mellitus 2

AbstractRequirements about the quality of clinical guidelines can be represented by schemata borrowed from the theory of abductive diagnosis, using temporal logic to model the time-oriented aspects expressed in a guideline. Previously, we have shown that these requirements can be verified using interactive theorem proving techniques. In this paper, we investigate how this approach can be mapped to the facilities of a resolution-based theorem prover,otterand a complementary program that searches for finite models of first-order statements,mace-2. It is shown that the reasoning required for checking the quality of a guideline can be mapped to such a fully automated theorem-proving facilities. The medical quality of an actual guideline concerning diabetes mellitus 2 is investigated in this way.

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