Τεχνητή Νοημοσύνη II: Κατηγορίαματική Λογική

Here are the study notes in Greek:

Εισαγωγή στην Τεχνητή Νοημοσύνη II

• Προβλήματα Κατηγορηματικής Λογικής (ΚΛ)

Επανάληψη Κατηγορηματικής Λογικής (ΚΛ)

• Παραδείγματα:
  • Bird(Tweedy) ∀x( Bird(x) Flies(x) )
  • ∀x∀y( ( Mother(x) = Mother(y) ⋀ ¬(x=y) ) Siblings(x,y) )

Σύμβολα ΚΛ

• Τελεστές: ¬, ⋀, ∨, , ⇥, ⇤, ⌅
• Παρενθέσεις: (, )
• Μεταβλητές: x1, x2,..., y,..., z,...
• Ίσοτητα: =

Σύμβολα Χρήστη

• Κατηγορήματα: P, Q, Flies, Bird,...
• Συναρτήσεις: Mother, Color,...
• Σταθερές: Jim, Mary, table,...

Όροι

• Κάθε σταθερά και κάθε μεταβλητή είναι όρος
• Αν τα t1,...tn είναι όροι, και το f n-μελής συνάρτηση, τότε και το f(t1,...,tn) είναι όρος

Ατομικοί Τύποι

• Κάθε ατομικός τύπος είναι και γενικός τύπος
• Αν τα t1,...tn είναι όροι, και το P n-μελές κατηγόρημα, τότε το P(t1,...,tn) είναι ατομικός τύπος
• Αν τα t1, t2 είναι όροι, τότε το t1 = t2 ατομικός τύπος

Γενικοί Τύποι

• Κάθε ατομικός τύπος είναι και γενικός τύπος
• Αν τα φ, ψ είναι τύποι, τότε και τα ¬φ, (φ⋀ψ), (φ∨ψ), (φ ψ), (φ⇥ψ) είναι τύποι
• Αν το x είναι μεταβλητή και το φ είναι τύπος, τότε και τα ∀x(φ), ∃x(φ) είναι τύποι

Ερμηνείες

• Μια ερμηνεία Μ για το αλφάβητο Α αποτελείται από:
  • ένα μη-κενό σύνολο |Μ| που ονομάζεται σύμπαν
  • ένα σύνολο από σχέσεις πάνω στο |Μ|
  • ένα σύνολο από συναρτήσεις πάνω στο |Μ|
  • μια συνάρτηση που αντιστοιχεί σε κάθε σταθερά c του Α

Αποτίμηση για μια ερμηνεία Μ του αλφαβήτου Α

• Αποτίμηση v που αντιστοιχεί κάθε μεταβλητή του Α σε ένα στοιχείο του |Μ|

Ορισμός Αληθείας του Tarski

• M, v ⊨ t1= t2 ανν v(t1) = v(t2)
• M, v ⊨ P(t1, t2,...tn) ανν (v(t1), v(t2),...v(tn)) ∈ PM

Ικανοποιήσιμοι και Έγκυροι Τύποι

• Ο τύπος φ είναι ικανοποιήσιμος ανν υπάρχει ερμηνεία M και αποτίμηση v τέτοιες ώστε M, v ⊨φ
• Η ερμηνεία M είναι μοντέλο του τύπου φ ( M ⊨φ) ανν για κάθε αποτίμηση v ισχύει M, v ⊨φ

ΘΕΩΡΗΜΑ

• Τ ⊨φ ανν Τ ∪ {¬φ} είναι μη-ικανοποιήσιμο### Μέλη Συλλόγου
• Τα μέλη του τοπικού ορειβατικού συλλόγου είναι ο Κώστας, η Μαρία, ο Γιάννης, και η Ελένη.
• ∀x∀y( siblings(x, y) ¬married(x,y) ) - Τα αδέρφια δεν είναι παντρεμένα μεταξύ τους.
• member(Κώστας) ⋀ member(Μαρία) ⋀ member(Γιάννης) ⋀ member(Ελένη) - Τα μέλη του συλλόγου.

Παντρεμένοι

• Ο Κώστας είναι παντρεμένος με την Μαρία.
• ∀x∀y∀z ( married(x, y) ⋀ married(x, z) y=z ) - Κανείς δεν μπορεί να είναι παντρεμένος με δύο άτομα同時.
• married(Κώστας, Μαρία) ⋀ siblings(Γιάννης, Ελένη) - Ο Κώστας είναι παντρεμένος με την Μαρία και ο Γιάννης είναι αδερφός της Ελένης.

Εγγραφή Παντρεμένων

• Τα παντρεμένα μέλη του συλλόγου εγγράφονται υποχρεωτικά με τον/την σύζυγό τους.
• ∀x∀y( member(x) ⋀ married(x, y) member(y) ) - Τα παντρεμένα μέλη εγγράφονται μαζί.
• ∀x (¬married(x,x) ) - Κανείς δεν μπορεί να είναι παντρεμένος με τον εαυτό του.### Αρχές Αναγωγής
• Η αναγωγή είναι μια μέθοδος για να αποδείξουμε ότι ένα σύνολο τύπων είναι μη-ικανοποιήσιμο.
• Προσθέτουμε αριθμούς κλασμάτων (clauses) στη βάση γνώσης μας και χρησιμοποιούμε κανόνες αναγωγής για να παράγουμε νέες κλάσεις.
• Ο σκοπός είναι να προκύψει ένα κενό σύνολο (empty set), το οποίο σημαίνει ότι το αρχικό σύνολο τύπων είναι μη-ικανοποιήσιμο.

Κανόνες Αναγωγής

• Ο κανόνας αναγωγής με ισότητα προσθέτει αξιώματα ισότητας στην βάση γνώσης μας.
• Τα αξιώματα αυτά είναι:
  • E1. ∀x (x = x)
  • E2. ∀x∀y (x=y y=x)
  • E3. ∀x∀y∀z (x=y ∧ y=z x=z)
  • E4.f. ∀x1...∀xn ∀y1...∀yn (x1=y1 ∧...∧ xn=yn f(x1,...,xn) = f(y1,...,yn))
  • E5.P. ∀x1...∀xn ∀y1...∀yn (x1=y1 ∧...∧ xn=yn P(x1,...,xn) ≡ P(y1,...,yn))

Παράδειγμα Αναγωγής με Ισότητα

• Το σύνολο S = {father(John) = Bill, ∀x (married(father(x), mother(x)), ¬married(Bill, mother(John))} είναι μη-ικανοποιήσιμο.
• Απαρίθμηση προτάσεων S ως clauses:
  1. {father(John) = Bill}
  2. {married(father(x1), mother(x1))}
  3. {¬married(Bill, mother(John))}
• Προσθήκη αξιωμάτων ισότητας στην Βάση Γνώσης.
• Αναγωγή: 4. {¬(x7=Bill), ¬(x8=mother(John)), ¬married(x7,x8)}, όπου y7/Bill, y8/mother(John) 5. {¬(x8=mother(John)), ¬married(father(John), x8)}, όπου x7/father(John) 6. {¬(mother(John)=mother(John))}, όπου x1/J

Επίλογος

• Η αναγωγή με ισότητα είναι μια ισχυρή μέθοδος για να αποδείξουμε ότι ένα σύνολο τύπων είναι μη-ικανοποιήσιμο.
• Χρησιμοποιώντας τους κανόνες αναγωγής και τα αξιώματα ισότητας, μπορούμε να προκύψει ένα κενό σύνολο, το οποίο σημαίνει ότι το αρχικό σύνολο τύπων είναι μη-ικανοποιήσιμο.