Análise da complexidade de espaço para um algoritmo de K(1)-Validade

Abstract

Apresenta-se neste trabalho a análise da complexidade de espaço do cálculo de resolução para K(1) proposto por Nalon e Dixon. Prova-se que este algoritmo, para o problema de K(1)-validade, tem complexidade de espaço de pior caso, pelo menos, exponencial, isto é, f(n) = (2n). Compara-se este resultado com a complexidade do algoritmo proposto por Ladner para o mesmo problema. Duas técnicas são sugeridas para uma melhora na complexidade de espaço. Prova-se, para isso, que é possível aplicar subsunção proposicional como parte do algoritmo baseado em resolução para K(1).