Logica a due variabili
Nella logica matematica e nell'informatica, la logica a due variabili è la parte della logica del primo ordine le cui formule possono essere scritte mediante due variabili[1] e solitamente senza simboli di funzione.
Soddisfacibilità e decidibilità
La sodisfacibilità logica finita è un problema decidibile.[2] Questo risultato generalizza ciò che era già noto per alcune logiche a due variabili come la logica descrittiva. I problemi di soddisfacibilità di alcune logiche a due variabili godono di una complessità computazionale molto inferiore rispetto alle altre.
Al contrario, per quanto concerne la logica del primo ordine a tre variabili e senza simboli di funzione, la soddisfacibilità è indecidibile.[3]
Counting quantifiers
La logica del primo ordine a due variabili e senza simboli di funzione è decidibile anche mediante l'impiego di counting quantifier[4] che ne quantificano l'unicità. Per valori numerici elevati, i counting quantifier non sono esprimibili nella logica a due variabili.
I counting quantifier migliorano effettivamente l'espressività delle logiche a variabili finite in quanto consentono di dire che esiste un nodo con altri nodi prossimali, vale a dire che (senza dover enunciare nella stessa formula i counting quantifier per le altre variabili).
Connessione con l'algoritmo di Weisfeiler-Leman
La logica a due variabili presenta una stretta connessione con l'algoritmo di Weisfeiler-Leman. Dati due grafi, due nodi qualsiasi presentano lo stesso colore stabile se e solo se hanno lo stesso tipo , cioè se soddisfano le medesime formule in una logica a due variabili che fa uso di counting quantifier.[5]
Note
- ↑ L. Henkin. Logical systems containing only a finite number of symbols, Report, Dipartimento di MAtematica, Università di Montreal, 1967
- ↑ E. Grädel, P.G. Kolaitis and M. Vardi, On the Decision Problem for Two-Variable First-Order Logic, The Bulletin of Symbolic Logic, Vol. 3, n. 1 (marzo 1997), pp. 53-69.
- ↑ A. S. Kahr, Edward F. Moore and Hao Wang. Entscheidungsproblem Reduced to the ∀ ∃ ∀ Case, 1962, notando che le loro formule con i simboli ∀ ∃ ∀ usano solo tre variabili.
- ↑ E. Grädel, M. Otto and E. Rosen. Two-Variable Logic with Counting is Decidable., Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science, 1997.
- ↑ Grohe, Martin. "Finite variable logics in descriptive complexity theory." Bulletin of Symbolic Logic 4.4 (1998): 345-398.