sign in
english version rss feed

inria-00442159, version 2

Using LJF as a Framework for Proof Systems

Anders Starcke Henriksen () 1

(2010)

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.

  • Domain : Cognitive science/Computer science
  • Keywords : LJF – Focusing – Encoded proof systems
  • Available versions :  v1 (2010-01-12) v2 (2010-01-20)
 
  • inria-00442159, version 2
  • oai:hal.inria.fr:inria-00442159
  • From: 
  • Submitted on: Wednesday, 20 January 2010 16:19:01
  • Updated on: Wednesday, 20 January 2010 16:58:49
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...