Di che cosa parliamo? Di oggetti e relazioni: per esempio persone e la relazione «conosce». Qui x e y rappresentano persone, non bit 0 o 1. «Soddisfacibile» significa che possiamo costruire almeno una situazione in cui la regola è vera.
Esempio: la regola è «esiste una persona che conosce tutti». Immagina un mondo con una sola persona, Ada, e stabilisci che Ada conosce se stessa. La regola è vera: scegli Ada e verifica che conosca ogni persona di quel mondo. Abbiamo costruito un modello: un insieme di oggetti e una descrizione delle relazioni fra loro.
Come si legge la notazione: ∃x∀yConosce(x,y) significa «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; φ è la condizione da verificare, composta da proprietà e relazioni, senza altri quantificatori. Tutte le scelte «esiste» vengono prima dei controlli «per tutti».
Che cosa escludiamo? Una funzione come Padre(x) restituisce un oggetto, il padre di x; una relazione come Conosce(x,y) dice invece se un collegamento è vero o falso. Questo problema ammette relazioni e nomi di oggetti, ma non funzioni che producono oggetti a partire da altri.
Queste restrizioni garantiscono che, se la regola è soddisfacibile, basta un modello finito con al più tanti elementi quanti le variabili esistenziali e i nomi di oggetti presenti, e almeno un elemento. 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