Quali erano le carenze della procedura di risoluzione di Robinson?
Paulson et alii. Da LCF a Isabelle / HOL dì:
Risoluzione per la logica del primo ordine, completa in linea di principio ma spesso deludente nella pratica.
Penso che completo significhi che possono dimostrare che qualsiasi formula vera nella logica del primo ordine è corretta. Nel Manuale del ragionamento automatico trovo:
La risoluzione è un metodo di dimostrazione di teoremi completo in modo confutativo: una contraddizione (cioè la clausola vuota) può essere dedotta da qualsiasi insieme di clausole insoddisfacenti.
Da Wikipedia:
Il tentativo di dimostrare che una formula soddisfacente del primo ordine non è soddisfacente può risultare in un calcolo senza fine
Perché è deludente?
Risposte
Sebbene "deludente in pratica" non sia certamente definibile formalmente, a differenza di "completo" (che in effetti significa "può eventualmente provare ogni vera formula"), è abbastanza facile trovare esempi in cui la risoluzione ingenua non è nemmeno lontanamente adeguata, ovvero esempi che dovrebbero essere facile da dimostrare ma quale risoluzione è estremamente lenta.
Un famoso esempio è una codifica del principio della buca per$n$ buchi nella logica proposizionale (che è l'affermazione "$n+1$ i piccioni non possono adattarsi $n$fori senza duplicati). Non vi è alcuna prova di questa affermazione utilizzando solo la risoluzione in tempo sotto-esponenziale in$n$.
Le cose vanno anche peggio nella logica dei predicati, dove è molto facile trovare affermazioni senza prove di risoluzione rapida.
Si noti che qualsiasi implementazione della risoluzione deve implementare una strategia per scegliere i risolventi, che è già un problema molto difficile, e un'area attiva di ricerca, poiché la maggior parte degli algoritmi pratici per la dimostrazione di teoremi sono miglioramenti della risoluzione ingenua, ad esempio l' iper-risoluzione .