The decidability of a fragment of BB ' IW-logic

• Type: Article in International Scientific Journal
• Date: 2004

Authors

Broda, S (Author) FCUP; Damas, L (Author) FCUP; Finger, M (Author) Other; Silva, PSE (Author) Other

Journal

Title: Theoretical Computer Science

Vol. 318

Pages: 373-408

ISSN: 0304-3975

Publisher: Elsevier

Indexing

ISI Web of Knowledge - 4 Citations

Scopus - 5 Citations

Scientific classification

FOS: Natural sciences > Computer and information sciences

Other information

Authenticus ID: P-000-9ZW

DOI: 10.1016/j.tcs.2004.02.002

Abstract (EN): 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 A-terms that inhabit a formula. A rewriting-system is associated with such lambda-terms, and we show that a formula admits a BB'IW-lambda-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.

Language: English

Type (Professor's evaluation): Scientific

No. of pages: 36