System Description: TPS: A Theorem Proving System for Type Theory

AbstractSubformula linking is an interactive theorem proving technique that was initially proposed for (classical) linear logic. It is based on truth and context preserving rewrites of a conjecture that are triggered by a user indicating links between subformulas, which can be done by direct manipulation, without the need of tactics or proof languages. The system guarantees that a true conjecture can always be rewritten to a known, usually trivial, theorem. In this work, we extend subformula linking to intuitionistic first-order logic with simply typed lambda-terms as the term language of this logic. We then use a well known embedding of intuitionistic type theory into this logic to demonstrate one way to extend linking to type theory.

Download Full-text

HYPNO: Theorem Proving with Hypersequent Calculi for Non-normal Modal Logics (System Description)

Automated Reasoning - Lecture Notes in Computer Science ◽

10.1007/978-3-030-51054-1_23 ◽

2020 ◽

pp. 378-387 ◽

Cited By ~ 1

Author(s):

Tiziano Dalmonte ◽

Nicola Olivetti ◽

Gian Luca Pozzato

Keyword(s):

Theorem Proving ◽

Modal Logics ◽

System Description ◽

Hypersequent Calculi ◽

Normal Modal Logics

Download Full-text

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.

Download Full-text