Horn-soddisfacibilita
Horn-soddisfacibilità particolare connotazione della soddisfacibilità di una formula. In generale una formula si dice soddisfacibile se esiste una interpretazione delle variabili [...] che può essere in forma positiva (→ Horn, clausoladi). Il problema della Horn-soddisfacibilità (ovvero della soddisfacibilità delle formule diHorn) consiste nel determinare se, dato un insieme diclausolediHorn, è possibile assegnare alle lettere ...
Leggi Tutto
Horn, clausoladiHorn, clausoladi in logica, → clausola avente una particolare struttura. In una clausola si distinguono letterali negativi, se sono espressi in forma negativa, cioè preceduti dal connettivo [...] soddisfacibilità di un insieme diclausolediHorn (→ Horn-soddisfacibilità) in modo più efficiente, in termini di passi di calcolo e, quindi, di tempo, del ricorso alle tavole di verità. Per questo le clausolediHorn, introdotte dal logico di cui ...
Leggi Tutto
Logica matematica
Silvio Bozzi
Pur potendo vantare come erede della logica formale un'origine risalente almeno ad Aristotele, come disciplina scientifica la logica matematica è un acquisto recente. [...] atomiche o loro negazioni in cui al massimo una è una lettera proposizionale. Tanto l'algoritmo per le clausolediHorn che quello di risoluzione che si applica a formule qualsiasi, ma che non ha complessità polinomiale, si basano sul fatto che ...
Leggi Tutto
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
PROLOG
PROLOG acronimo di programmation en logique (programmazione logica), indica un linguaggio di programmazione elaborato nel 1972 nell’ambito dell’università di Aix-Marseille sulla base dell’impostazione [...] un letterale è positivo, cioè che contengono al più una sola conclusione: sono queste le cosiddette clausoledi → Horn. L’uso delle clausolediHorn, pur non togliendo nulla alla capacità espressiva del formalismo logico, rende molto più semplice il ...
Leggi Tutto
Kowalski
Kowalski Robert Anthony (Bridgeport, Connecticut, 1941) logico e informatico inglese di origine statunitense. Dopo gli studi di matematica negli Stati Uniti, ottenne il dottorato in computer [...] College di Londra. Si è in particolare interessato di intelligenza artificiale e della dimostrazione automatica dei teoremi e ha dato importanti contributi alla programmazione logica sviluppando una interpretazione procedurale delle clausolediHorn. ...
Leggi Tutto
HornHorn Alfred (New York 1918 - Los Angeles 2001) matematico e logico statunitense. Ha studiato in particolare la teoria dei reticoli e le algebre universali. Ha introdotto nel 1951 un particolare [...] tipo diclausole, spesso dette anche formule diHorn, che hanno trovato applicazione nella programmazione logica. Ha insegnato a Berkeley in California fino al suo pensionamento nel 2000. ...
Leggi Tutto
(A. T., 53-54-55; 56-57).
Geografia: Nome (p. 667); La moderna conoscenza geografica (p. 667); Situazione e confini (p. 668); Composizione litologica del suolo (p. 668); Struttura e forme del terreno [...] di Heilbronn, mentre le truppe svedesi, sotto il comando diHorn, di G. K. Bernardo di Weimar, di J. K. Banér, proseguivano le loro scorrerie. Decisivo fu di , e uno italo-austriaco con le clausole concernenti la questione balcanica (20 febbraio ...
Leggi Tutto