The decidability of a fragment of BB ' IW-logic

• Tipo: Artigo em Revista Científica Internacional
• Data: 2004

Autores

Broda, S (Autor) FCUP; Damas, L (Autor) FCUP; Finger, M (Autor) Outra; Silva, PSE (Autor) Outra

Revista

Título: Theoretical Computer Science

Vol. 318

Páginas: 373-408

ISSN: 0304-3975

Editora: Elsevier

Indexação

ISI Web of Knowledge - 4 Citações

Scopus - 5 Citações

Classificação Científica

FOS: Ciências exactas e naturais > Ciências da computação e da informação

Outras Informações

ID Authenticus: 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.

Idioma: Inglês

Tipo (Avaliação Docente): Científica

Nº de páginas: 36