Newsgroup: it.comp.ia
Titolo: logica simbolica

ciao.
l'espressione "un uccello ha le ali" puo' essere espressa come una negazione:
~uccello(x) V ali(x)
e se non volessi usare la negazione ?
altre formulazioni possibili?
cosi, per curiosità.
premetto che non ci capisco molto, ho solo letto un articolo su una rivista.
grazie
ciao
Dave


uccello(x) --> ali(x) , che è la stessa cosa
cmq secondo me la formulazione giusta è l'enunciato Esiste x (~uccello(x) V
ali(x))

 altre formulazioni possibili?
Dipende da che logica usi, e da cosa vuoi dire. Ad esempio, col calcolo dei 
predicati, che pare tu stia usando, se vuoi dire "almeno un uccello ha le 
ali", scrivi "Esiste X : e'_uccello(X) -> ha_ali(X)", se vuoi dire "tutti 
gli uccelli hanno le ali", scrivi "Per ogni X : e'_uccello(X) -> 
ha_ali(X)".
-- 
Fighting for peace is like fucking for virginity
ObjectZone - 
http://space.tin.it/computer/csadun


Nella rivista NEWTON di febbraio 2000
c'era un articolo intitolato "la mente artificiale".
In quell'articolo veniva spiegato, molto semplicemente, come un software di I.A.
era in grado di fare delle deduzioni, e veniva mostrato questo procedimento:
si considerano i seguenti fatti:
(a) "il piccione è un uccello"
(b) "un uccello ha le ali"
PROBLEMA: il software deve dedurre che il piccione ha le ali.
utilizzando i simboli della logica, le frasi vegono cosi tradotte:
(a) uccello(piccione)
(b) ~uccello(x) V ali(x)      -che significa: "o X non è un uccello o X ha le ali"
a questo punto il software faceva il confronto tra (a) e (b) e
sostituendo la X si otteneva:
(b') ~uccello(piccione) V ali(piccione)      -che significa: "o il piccione non è un uccello o il piccione ha le ali"
Dato che il piccione è un uccello, dall'espressione (b') confrontata con l'espressione (a),
si arriva alla conclusione:
(c)  ali(piccione)      -che significa: "il piccione ha le ali"
Immagino che per voi queste cose sono banali,
ma mi chiedo se esistono altri procedimenti (logici) per arrivare alla medesima conclusione, cioè
se esistono altri metodi di approccio al problema.
Ad esempio, un dimostratore di teoremi ragionerebbe in questo modo?
help!
rigrazio tutti.
Dave
(la prossima volta che incontro un piccione giuro che lo strozzo... :-))


Inanzitutto le formalizzazioni che cercavi erano:
u(piccione)
Per ogni x (u(x) --> a(x))
con :
u(x) che vuol dire x è uccello
a(x) : x ha le ali
piccione è una costante
--> sta per implicazione logica (cioè ~A V B)
Premessa: non è il mio campo la dimostrazione di teoremi in modo automatico
Cmq esistono diversi metodi (o procedimenti) formali per fare "deduzioni"
logiche, alcuni che si prestano ad essere usati dall'uomo, altri che si
traducono molto facilmente in algoritmi. Io se dovessi partire da qualche
parte per fare un programma del genere cercherei di usare la procedura di
unificazione, che viene anche usata nel prolog. Anzi, se ti interessa un
linguaggio adatto a questi scopi ti consiglio proprio il prolog...

Ad esempio, un dimostratore di teoremi ragionerebbe in questo modo?
Ci sono molti modi diversi di fare inferenze. La logica del prim'ordine, 
che e' quella piu' nota e a cui probabilmente faceva riferimento il tuo 
articolo, e' solo uno.
Altre con brillanti successi applicativi sono logica fuzzy e reti 
bayesiane. Ci sono poi calcoli di ordine superiore, un sacco di logiche 
formali piu' o meno interessanti, e un buon numero di meccanismi che 
possono essere usati per fare inferenze (in soft computing, tipicamente, 
reti neurali e algoritmi genetici).


linguaggio adatto a questi scopi ti consiglio proprio il prolog...
In effetti il Prolog non è un theorem prover, si limita ad applicare
backward chaining su una base di conoscenza costituita solo e
unicamente da clausole di Horn.
Theorem provers più potenti, in grado di trattare qualsiasi tipo di
base di conscenza si possono costruire sfruttando la unit resolution.
L'idea in sè è relativamente semplice, si prende una KB e la si
riporta tutta in CNF (ogni proposizione viene riportata a AND di OR).
A questo punto se vogliamo dimostrare la proposizione alpha sarà
sufficiente costruire la nuova base di conoscenza KB' come KB' <- (KB
AND NOTalpha) se alpha è deducibile dalla KB allora applicando unit
resolution a KB' arriveremo a una contraddizione (alla clausola vuota
in pratica) e avremo dimostrato alpha, altrimenti potremo concludere
che alpha non è deducibile da KB (non che alpha sia falsa però).
In FOL l'applicazione di unit resolution è un po' piuù complessa di
quanto avvenga in logica proposizionale poichè per poterla applicare a
due proposizione occorre che possano unificare.
L'aspetto interessante della tecnica di risoluzione è che di fatto ci
permette di riportare il problema della dimostrazione di un teorema a
un caso abbastanza standard di problem solving, dove gli stati vengono
caratterizzati dall'evoluzione della KB via via che si deducono nuovi
fatti e la funzione successore sarà l'applicazione di unit resolution
stessa.
Augusto Pucci

ha_ali(X)".
Non sono sicuro che in quesa forma sia corretta, in effetti quel che
hai scritto equivale a:
"Esiste(X) : NOTè_uccello(X) OR ha_ali(X)"
ma questa è vera se esiste almeno un X che non è un uccello, in
effetti se usi una implicazione, o equivalenti, ti basta che sia falsa
la premessa per rendere vera l'intera implicazione a prescindere dalla
verità o meno della conseguenza.
Credo che in FOL "almeno un uccello ha le ali" sia più corretto
scriverla come:
"Esiste(X) : è_uccello(X) AND ha_ali(X)"
questa è vera solo se c'è almeno una istanza di X che soddisfa il
requisito di essere un uccello e di avere le ali.
Augusto Pucci

 [cut]
A proposito... guarda chi si rivede :-)
Augusto Pucci

 ha scritto nel messaggio news:fkv5fvs2l9dn6mjkv...@4ax.com...

CIAO! ciao a te e a tutti gli altri veterani delle guerre usenettiane!
hai notato? la "guerra" dei chatbot è finita, cosi sembra... :-)
Dave

>>
LISTENING--->  
* YES,FLOWER.

hai notato? la "guerra" dei chatbot è finita, cosi sembra... :-)
Meno male :) ma non svegliamo il can che dorme :)))
Augusto Pucci

ali", scrivi "Esiste X : e'_uccello(X) -> ha_ali(X)", 
Non sono del tutto sicuro che sia la corretta formulazione, sarebbe
equivalente a:
"Exists(X) : ~è_uccello(x) V ha_ali(X)"
ma questa è vera anche se esiste una sola entità (non necessariamente
un uccello) che ha le ali) a prescindere dal fatto che sia o meno un
uccello..sarebbe vera anche se c'è almeno un X che invalida la
premessa... renderebbe comunque vera la proposizione.
Credo che "almeno un uccello ha le ali" sia + corretto esprimerla (in
FOL) con:
"Exists(X): è_uccello(X) AND ha_ali(X)"
questa è vera se c'è almeno un X che soddisfa entrambe le condizioni.
Augusto Pucci

 "Esiste(X) : 鑏uccello(X) AND ha_ali(X)"
Si', hai ragione.


 Shrdlu
Per quel che ricordo, Winograd non segui' tecniche formali "teoretiche" 
particolari, o almeno cosi' accenna Hosftadter. Le espressioni sotto mi 
paiono lisplike o lambda calcolo, ma non e' che abbia letto il dialogo a 
fondo. :)
