System description: CardTAP: The first theorem prover on a smart card

1998 ◽  
pp. 47-50 ◽  
Author(s):  
Rajeev Goré ◽  
Joachim Posegga ◽  
Andrew Slater ◽  
Harald Vogt
Keyword(s):  
Smart Card ◽  
Theorem Prover ◽  
System Description

scholarly journals The Lean Theorem Prover (System Description)

2015 ◽  
pp. 378-388 ◽  
Author(s):  
Leonardo de Moura ◽  
Soonho Kong ◽  
Jeremy Avigad ◽  
Floris van Doorn ◽  
Jakob von Raumer
Keyword(s):  
Theorem Prover ◽  
System Description

scholarly journals Leo-III Version 1.1 (System description)

10.29007/grmx ◽  
2018 ◽  
Author(s):  
Christoph Benzmüller ◽  
Alexander Steen ◽  
Max Wisniewski
Keyword(s):  
Higher Order ◽  
Order Logic ◽  
Theorem Prover ◽  
Higher Order Logic ◽  
System Description ◽  
Agent Based ◽  
First Order ◽  
Theorem Provers ◽  
Automated Theorem Prover ◽  
Ordering Constraints

Leo-III is an automated theorem prover for (polymorphic) higher-order logic which supports all common TPTP dialects, including THF, TFF and FOF as well as their rank-1 polymorphic derivatives. It is based on a paramodulation calculus with ordering constraints and, in tradition of its predecessor LEO-II, heavily relies on cooperation with external first-order theorem provers.Unlike LEO-II, asynchronous cooperation with typed first-order provers and an agent-based internal cooperation scheme is supported. In this paper, we sketch Leo-III's underlying calculus, survey implementation details and give examples of use.

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.

Sign in / Sign up

Export Citation Format

Share Document