Affordable Access

Publisher Website

The decidability of a fragment ofBB ′ IW-logic

Authors
Journal
Theoretical Computer Science
0304-3975
Publisher
Elsevier
Publication Date
Volume
318
Issue
3
Identifiers
DOI: 10.1016/j.tcs.2004.02.002

Abstract

Abstract Despite its simple formulation, the decidability of the logic BB ′ IW has remained an open problem. We present here a decision procedure for a fragment of it, called the arity-1 formulas. The decidability proof is based on a representation of formulas called formula-trees, which is coupled with a proof method that computes long normal λ-terms that inhabit a formula. A rewriting-system is associated with such λ-terms, and we show that a formula admits a BB ′ IW - λ-term if and only if the associated rewriting-system terminates. The fact that termination is decidable is proved using a result on the finiteness of non-ascending sequences of n-tuples in N n , which is equivalent to Kripke's Lemma.

There are no comments yet on this publication. Be the first to share your thoughts.