TABLEAUX EXAMPLES

Propositional

Κατ' αρχήν θα χρειαστούμε inference rules:

Conjunction (C)

 1.      P and Q
 2(1,C). P
 3(1,C). Q

Negation elimination (NE)

 1.        not not P
 2. (1,NE) P

Disjunction (D)

         1. P or Q
       /           \
 1a(1,D). P    1b(1,D). Q

που σε plain text είναι πιο ευανάγνωστο αν χρησιμοποιήσετε indentation
για να δείξετε τα branches:

1. P or Q
2a(1,D). P
    2b(1,D). Q

Προφανώς ισχύουν όλα τα αξιώματα της άλγεβρας Boole, μπορείτε να
χρησιμοποιήσετε το γράμμα (B) για αφαρμόσετε De Morgan ή ορισμούς
connectives. Ειδικά για το implies, παρότι θα μπορούσατε να εφαρμόσετε
πρώτα τον ορισμό και μετά το disjunction μπορείτε να εφαρμόσετε και το
παρακάτω απευθείας:

1. P -> Q
2a(1,I). not P
    2b(1,I). Q



Δείτε τώρα το παρακάτω statement:

P -> (Q and R), not Q or not R |= not P

Δηλαδή, ότι αν έχουμε ένα knowledge base με τα παρακάτω δύο
statements:

not Q or not R
P -> (Q and R)

αυτό supports ότι not P. Σημασιολογικά εύκολα βλέπετε ότι ισχύει:
Αφού τουλάχιστον ένα από τα Q,R είναι ψευδές, το (Q and R) δεν μπορεί
να ισχύει. Αλλά τότε δεν μπορεί να ισχύει ούτε το P, γιατί αν ίσχυε το
P θα ίσχυε και το (Q and R). Άρα το not P ισχύει.

Θα χρησιμοποιήσουμε tableaux για να αποδείξουμε το ίδιο, δηλαδή ότι

P -> (Q and R), not Q or not R |- not P

όπου το |- σημαίνει "αποδεικνύεται με tableaux".


Για να αποδείξουμε ότι το not P είναι valid, θα προσθέσουμε στην KB το
statement not not P και θα κλείσουμε το tableau.

1.       P -> (Q and R)
2.       not Q or not R
3.       not not P
4(3,NE). P
5b(1,I). Q and R
    5a(1,I). not P
    CLOSED(4,5a)
6(5b,C). Q
7(5b,C). R
8a(2,D). not Q
CLOSED(6,8a)
    8b(2,D). not R
    CLOSED(7,8b)

Παρατηρώ ότι όλα τα branches κλείνουν, άρα το tableaux είναι
inconsistent. Άρα κάπου υπάρχει ένα statement που είναι ψευδές.
Προφανώς δεν μπορεί να είναι το KB, ούτε αυτά που παρήγαγα, άρα είναι
η γραμμή 3 που πρόσθεσα. Άρα το not not P είναι inconsistent (δλδ
είναι ψευδές σε όλα τα models του KB). Άρα το not P είναι valid (δλδ
είναι αληθές σε όλα τα models του KB).

Προσέξτε ότι στην γραμμή 5 έβαλα το 5a να είναι indented αντί για το
5b, γιατί ήξερα πως θα κλείσει νωρίς και δεν ήθελα να έχω indented το
branch που μένει ανοιχτό πιο πολύ, για να αποφύγω πολλαπλά indentions.
Αν είχα βάλει τα a,b με την αναμενώμενη σειρά, θα είχα:

1.       P -> (Q and R)
2.       not Q or not R
3.       not not P
4(3,NE). P
5a(1,I). not P
CLOSED(4,5a)
    5b(1,I). Q and R
    6(5b,C). Q
    7(5b,C). R
    8a(2,D). not Q
    CLOSED(6,8a)
        8b(2,D). not R
        CLOSED(7,8b)


Αν έγραφα στον πίνακα θα έγραφα:

              1.       P -> (Q and R)
              2.       not Q or not R
              3.       not not P
              4(3,NE). P
                 /        \
5a(1,I). not P          5b(1,I) Q and R
         CLOSED(4,5a)   6(5b,C) Q
                        7(5b,C) R
                        /       \
           8a(2,D) not Q    8b(2,D) not R
           CLOSED(6,8a)     CLOSED(7,8b)

Προσέξτε επίσης πως στις 6,7 δεν έβαλα 6b,7b γιατί το branch a έχει
κλείσει οπότε δεν υπάρχουν 6a,7a. Αν δεν είχε κλείσει, η γραμμή 7
θα λέγονταν 7b και τα branches που ανοίγουν μετά 8ba και 8bb.

Παράδειγμα:

1. not Q or not R
2. P -> (Q and R)
3. not Q -> P

Ισχύθει το Q; Προσθέτω και συνεχίζω:

4. not Q
    5a(3,I). not not Q
    6a(5a,NE). Q
    CLOSED(4,6a)
5b(3,I). P
    6ba(2,I). not P
    CLOSED(5b,6ba)
6bb(2,I). Q and R
7(6bb,C). Q
8(6bb,C). R
CLOSED(4,7)


Quantifiers

Η πιο απλή περίπτωση είναι όταν όλα τα predicates είναι universally
quantified.

1. forall X. not Q(X,X) or not R(X,X)
2. forall X,Y. P(X) -> not Q(X,Y) or R(Y,X)
3. forall Y. Q(a,Y)

Θέλουμε να αποδείξουμε ότι:

not P(a)

άρα προσθέτουμε:

5. not not P(a)

Ο κανόνας quantifier elimination (QE) μας επιτρέπει να αντικαταστήσουμε
μία universally quantified μεταβλητή X με οποιοδήποτε σύμβολο: αφού
ισχύει για κάθε X, θα ισχύει και για αυτή την τιμή του X. Σχεδόν
πάντα η αντικατάσταση είναι προφανής και δεν χρειάζεται να την
σημειώνουμε.

6(5,NE).  P(a)
7(3,QE).  Q(a,a)
8(1,QE).  not Q(a,a) or not R(a,a)
    9a(7,D). not Q(a,a)
    CLOSED(7,9a)
8b(7,D).  not R(a,a)
9b(2,QE). P(a) -> not Q(a,a) or R(a,a)
    10ba(9b,I). not P(a)
    CLOSED(6,10ba)
10bb(9b,I). not Q(a,a) or R(a,a)
11bba(10bb,D). not Q(a,a)
CLOSED(7,11a)
    11bbb(10bb,D). R(a,a)
    CLOSED(8b,11b)


Ο κανόνας του Skolem (SK) μας επιτρέπει να αντικαταστήσουμε μία
existentilly quantified μεταβλητή με νέο σύμβολο: αφού υπάρχει ένα
entity (για το οποίο δεν ξέρω τίποτα άλλο) με αυτή την ιδιότητα, του
δίνω ένα νέο όνομα ώστε να μην έχει καμιά άλλη ιδιότητα. Προφανώς (α)
το QE μπορεί να χρησιμοποιήσει το νέο όνομα, αφού ισχύει για όλα τα
σύμβολα. (β) μπορεί τελικά να αποδειχθεί πως το skolem symbol είναι
ίσο με άλλο σύμβολο.

Το νέο σύμβολο μπορεί να το δείτε να αναφέρεται ως "Skolem variable",
το οποίο το αποφεύγω (αν και νομίζω πως μου ξέφυγε μία φορά στο
μάθημα) γιατί δεν είναι variable με την έννοια που χρησιμοποιούμε εδώ
τη λέξη variable. Ας το λέμε "Skolem name" ή "Skolem entity".

1. forall X exists Y. P(X) -> Q(X,Y)
2. forall X,Y. Q(X,Y) -> R(X)
3. P(a)

Θέλουμε να αποδείξουμε πως R(a).

4. not R(a)
5(1,QE). exists Y. P(a) -> Q(a,Y)
6(5,SK). P(a) -> Q(a,sk0)
   7a(6,I). not P(a)
   CLOSED(3,7a)
7b(6,I). Q(a,sk0)
8(2,QE). Q(a,sk0) -> R(a)
9a(8,I). not Q(a,sk0)
CLOSED(7b,9a)
    9b(8,I). R(a)
    CLOSED(4,9b)