Using LJF as a Framework for Proof Systems

Abstract : 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.
Type de document :
[Technical Report] 2010
Liste complète des métadonnées

Littérature citée [21 références]  Voir  Masquer  Télécharger
Contributeur : Anders Starcke Henriksen <>
Soumis le : mercredi 20 janvier 2010 - 16:19:01
Dernière modification le : vendredi 16 septembre 2016 - 15:07:18
Document(s) archivé(s) le : jeudi 23 septembre 2010 - 11:30:37


Fichiers produits par l'(les) auteur(s)


  • HAL Id : inria-00442159, version 2



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



Consultations de la notice


Téléchargements de fichiers