Dom 18 Agosto, 06:46:02 - 2019

Autore Topic: esame dell'11 gennaio 2013 (Artificial Intelligence I)  (Letto 734 volte)

0 Utenti e 1 Visitatore stanno visualizzando questo topic.

Offline andrea89

  • Author
  • Professore Ordinario
  • **
  • Post: 733
  • FeedBack: +76/-17
    • Mostra profilo
esame dell'11 gennaio 2013 (Artificial Intelligence I)
« il: Sab 09 Febbraio, 16:14:37 - 2013 »
ragazzi qualcuno sarebbe cosi gentile da spiegarmi i procedimenti con cui viene risolto questo esercizio? non è chiarissima la soluzione!

Consider the following first order formulas:
I. ∀x Equal(x, x)
II. ∀x∀y (Equal(x, y)→Equal(y, x))
III. ∀x∀y∀z ((Equal(x, y) ∧ Equal(y, z))→Equal(x, z))
Starting from I. II. and III. prove by refutation with resolution the following: ∀x∀y∀z ((Equal(x, y) ∧ ¬Equal(y, z))→¬Equal(x, z))
Solution:
Transform into normal form the original formulas plus the negation of the thesis (A,B,C are Skolem constants):
1) Equal(x1, x1)
2) Equal(x2, x3) ∨ ¬Equal(x3, x2)
3) Equal(x4, x5) ∨ ¬Equal(x4, x6) ∨ ¬Equal(x6, x5) 4) Equal(A, B)
5) ¬Equal(B, C)
6) Equal(A, C)
We can get the empty clause, for instance, as follows:
7) Equal(B, A) resolution from (2) and (4) (substitution {x3/A, x2/B})
8) ¬Equal(A, x5) ∨ Equal(B, x5) resolution from(3) and (7) (substitution {x6/A, x4/B}) 9) Equal(B,C) resolution from (6) and (8) (substitution {x5/C})
10) {} resolution from (5) and (9)
ll computer non è una macchina intelligente che aiuta le persone
stupide, anzi è una macchina stupida che funziona solo nelle mani delle persone intelligenti (Umberto Eco).

Offline andrea89

  • Author
  • Professore Ordinario
  • **
  • Post: 733
  • FeedBack: +76/-17
    • Mostra profilo
Re:esame dell'11 gennaio 2013 (Artificial Intelligence I)
« Risposta #1 il: Sab 09 Febbraio, 16:22:46 - 2013 »
Inoltre volevo chiedervi non avendo seguito il corso se qualcuno ha materiale (appunti, slide diverse da quelle del corso o altro) utile a capire l'utilizzo dei Tableau!
ll computer non è una macchina intelligente che aiuta le persone
stupide, anzi è una macchina stupida che funziona solo nelle mani delle persone intelligenti (Umberto Eco).

Offline vinkia

  • Guru
  • Professore Associato
  • *****
  • Post: 696
  • FeedBack: +70/-30
  • http://teamend.altervista.org/chi-siamo
    • Mostra profilo
    • TeamEnd applicazioni per Android e non solo...
Re:esame dell'11 gennaio 2013 (Artificial Intelligence I)
« Risposta #2 il: Dom 10 Febbraio, 09:23:18 - 2013 »
Guarda per il primo esercizio, praticamente usa il metodo di risoluzione per la logica del primo ordine: prima di tutto prendo le ipotesi iniziali e le trasformo in CNF per la logica del primo ordine(trovi il procedimento sul libro nel capitolo 9), poi le mette in and con la negazione della tesi. Tutto questo perchè se tu vuoi dimostrare che, date due formule alfa e beta, alfa implica beta, ti basta dire che alfa e not(beta) è insoddisfacibile.

Una volta trasformato in CNF, inizi ad applicare la risoluzione per la logica del primo ordine(trovi il procedimento sempre sul capitolo 9), ovvero prendi le formule che hai ottenuto e applichi la risoluzione a due a due, eliminando le clausole che unificano e sono opposte, come ad esempio:

2)Equal(x2, x3) ∨ ¬Equal(x3, x2)  risoluzione con 4)Equal(A,B)

hai che ¬Equal(x3, x2) e Equal(A,B) unificano, ma sono una il negato dell'altra, quindi riscrivi una nuova clausola che è l'unione di 1) e 2), ma senza le clausole che ho scritto prima e ottieni:
7)Equal(x2,x3), ma ricordando che per fare questo hai unificato sostituendo A=x3 e B=x2, in realtà hai Equal(B,A)

Iterando il ragionamento, arrivi ad una clausola vuota===> hai dimostrato la tesi iniziale.

Non preoccuparti solo di essere migliore dei tuoi contemporanei o dei tuoi predecessori. Cerca solo di essere migliore di te stesso.

http://teamend.altervista.org/chi-siamo