Name
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 Nn, which is equivalent to Kripke's Lemma. |
Year | DOI | Venue |
|---|---|---|
2004 | 10.1016/j.tcs.2004.02.002 | Theor. Comput. Sci. |
Keywords | Field | DocType |
open problem,decision procedure,logic bb,decidability proof,arity-1 formula,associated rewriting-system terminates,non-ascending sequence,proof method,simple formulation | Discrete mathematics,Combinatorics,Open problem,Decidability,If and only if,Lemma (mathematics),Mathematics,Mathematical logic | Journal |
Volume | Issue | ISSN |
318 | 3 | Theoretical Computer Science |
Citations | PageRank | References |
2 | 0.50 | 3 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Sabine Broda | 1 | 64 | 13.83 |
| Luís Damas | 2 | 128 | 22.34 |
| Marcelo Finger | 3 | 365 | 48.82 |
| Paulo Silva e Silva | 4 | 2 | 0.50 |