Si parla di oggetti e relazioni: per esempio persone e la relazione "conosce". Qui x e y rappresentano persone, non bit 0 o 1, e "soddisfacibile" vuol dire che possiamo costruire almeno una situazione in cui la regola è vera.
Prendiamo la regola "esiste una persona che conosce tutti". In un mondo con una sola persona, Ada, che conosce se stessa, la regola è vera: scegli Ada e verifichi che conosca ogni persona di quel mondo. Abbiamo costruito un modello, cioè un insieme di oggetti con una descrizione delle relazioni fra loro.
In simboli la regola si scrive ∃x∀yConosce(x,y): esiste una persona x tale che, per ogni persona y, x conosce y. Nella forma generale ∃X∀Yφ, X e Y sono gruppi di variabili e φ è la condizione da verificare, fatta di proprietà e relazioni senza altri quantificatori. Tutte le scelte "esiste" vengono prima dei controlli "per tutti".
Una funzione come Padre(x) restituisce un oggetto, il padre di x, mentre una relazione come Conosce(x,y) dice se un collegamento è vero o falso. Il problema ammette relazioni e nomi di oggetti, ma non funzioni che producono oggetti a partire da altri.
Con queste restrizioni, se la regola è soddisfacibile basta un modello finito con almeno un elemento e al più tanti elementi quante sono le variabili esistenziali e i nomi di oggetti presenti. Si scelgono le relazioni e si controllano tutte le combinazioni dei valori di Y; le tabelle delle relazioni e i controlli possono richiedere tempo esponenziale.
Complemento e collegamenti
Nessun complemento associato.
- restringere la forma delle formule: da indecidibile a NEXP-completo
- entrambi NEXP-completi
Problemi NEXP-completi