Dimostrazione, teoria della
Jean-Yves Girard
La teoria della dimostrazione nasce negli anni Venti del Novecento come strumento di realizzazione del programma di David Hilbert per la fondazione della [...] , cioè sequenti p1,…,pn⇒ q1,….,qm dove le pie qjsono atomiche (diverse dal falso ⊥). Di fatto, la tecnica è veramente efficace solo nel caso delle clausolediHorn, vale a dire clausole della forma p1,…,pn⇒q, e per dei goal del tipo ∃y1,…,∃up A, dove ...
Leggi Tutto
LOGICA E INFORMATICA
Carlo Cellucci
I. McCarthy (1963) afferma che è ragionevole sperare che le relazioni tra l'i. e la l. matematica nel prossimo secolo saranno altrettanto fruttuose di quelle tra [...] AnÁB1,...,Bm che significa: (B1 e...e Bm) implica (A1 oppure ... oppure An). Nel caso delle clausolediHorndi solito si preferisce questa notazione. In particolare: a) le clausole definite vengono scritte AÁB1,...,Bm se m≥1, oppure AÁ se m=0; b) le ...
Leggi Tutto
Modelli, Teoria dei
Silvio Bozzi
Malgrado le modeste origini che ne hanno segnato la nascita, la teoria dei modelli ha sviluppato nel corso del tempo idee e metodi che l'hanno resa uno dei settori più [...] xn ((A1∧…∧Ak)→Ak+1) dove ogni Aj è atomica. Sono queste le formule note come formule universali diHorn e coincidono con le clausolediHorn note agli informatici. Il fatto interessante, come mostrerà Mal'cev, è che esse costituiscono la famiglia più ...
Leggi Tutto