Lógica de dos variables - Two-variable logic

En lógica matemática e informática , la lógica de dos variables es el fragmento de la lógica de primer orden donde las fórmulas se pueden escribir usando solo dos variables diferentes . Este fragmento generalmente se estudia sin símbolos de función .

Decidibilidad

Algunos problemas importantes sobre la lógica de dos variables, como la satisfacibilidad y la satisfacibilidad finita , son decidibles . Este resultado generaliza los resultados sobre la decidibilidad de fragmentos de lógica de dos variables, como ciertas lógicas de descripción ; sin embargo, algunos fragmentos de lógica de dos variables disfrutan de una complejidad computacional mucho menor para sus problemas de satisfacibilidad.

Por el contrario, para el fragmento de tres variables de lógica de primer orden sin símbolos de función, la satisfacibilidad es indecidible.

Contando cuantificadores

Se sabe que el fragmento de dos variables de lógica de primer orden sin símbolos de función es decidible incluso con la adición de cuantificadores de conteo y, por lo tanto, de cuantificación de unicidad . Este es un resultado más poderoso, ya que contar cuantificadores para valores numéricos altos no es expresable en esa lógica.

Los cuantificadores de conteo en realidad mejoran la expresividad de las lógicas de variables finitas, ya que permiten decir que hay un nodo con vecinos, a saber . Sin contar los cuantificadores , se necesitan variables para la misma fórmula.

Conexión al algoritmo Weisfeiler-Leman

Existe una fuerte conexión entre la lógica de dos variables y el algoritmo Weisfeiler-Leman (o refinamiento de color). Dados dos gráficos, dos nodos cualesquiera tienen el mismo color estable en el refinamiento del color si y solo si tienen el mismo tipo, es decir, satisfacen las mismas fórmulas en lógica de dos variables con conteo.

Referencias

  1. ^ L. Henkin. Sistemas lógicos que contienen solo un número finito de símbolos , Informe, Departamento de Matemáticas, Universidad de Montreal, 1967
  2. ^ E. Grädel, PG Kolaitis y M. Vardi, Sobre el problema de decisión para la lógica de primer orden de dos variables , The Bulletin of Symbolic Logic, vol. 3, No. 1 (marzo de 1997), págs. 53-69.
  3. ^ COMO Kahr, Edward F. Moore y Hao Wang. Entscheidungsproblem Reducido al caso ∀ ∃ ∀ , 1962, señalando que sus fórmulas ∀ ∃ ∀ utilizan sólo tres variables.
  4. ^ E. Grädel, M. Otto y E. Rosen. La lógica de dos variables con conteo es decidible. , Actas del Duodécimo Simposio Anual del IEEE sobre Lógica en Ciencias de la Computación, 1997.
  5. ^ Grohe, Martín. "Lógicas de variables finitas en la teoría descriptiva de la complejidad". Boletín de lógica simbólica 4.4 (1998): 345-398.