Using LJF as a Framework for Proof Systems - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport Technique) Année : 2010

Using LJF as a Framework for Proof Systems

Résumé

In this work we show how to use the focused intuitionistic logic system LJF as a framework for encoding several different intuitionistic and classical proof systems. The proof systems are encoded in a strong level of adequacy, namely the level of (open) derivations. Furthermore we show how to prove relative completeness between the different systems. By relative completeness we mean that the systems prove the same formulas. The proofs of relative completeness exploit the encodings to give, in most cases, fairly simple proofs. This work is heavily based on the recent work by Nigam and Miller, which uses the focused linear logic system LLF to encode the same proof systems as we do. Our work shows that the features of linear logic are not needed for the full adequacy result, and furthermore we show that even though encoding in LLF is more generic and streamlined, the encoding in LJF sometimes gives simpler, more natural encodings and easier proofs.

Domaines

Informatique
Fichier principal
Vignette du fichier
LJF-framework.pdf (308.66 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00442159 , version 1 (18-12-2009)
inria-00442159 , version 2 (20-01-2010)

Identifiants

  • HAL Id : inria-00442159 , version 2

Citer

Anders Starcke Henriksen. Using LJF as a Framework for Proof Systems. [Technical Report] 2010. ⟨inria-00442159v2⟩

Collections

LARA
190 Consultations
189 Téléchargements

Partager

Gmail Facebook X LinkedIn More