Gerard Vreeswijk
Automatisch redeneren
Vandaag 1. Recapitulatie DOS en DOB 2. Verschil tussen locaal (regel-gebaseerd) en globaal (argument-gebaseerd) redeneren. 3. Aggregeren van support op regelniveau (accrual) 4. Vertaling van zoekalgoritme naar dialoogvorm.
College 13 [16], Slide 1 [21]
Gerard Vreeswijk
Automatisch redeneren
College 13 [16], Slide 2 [21]
Taxonomie van regels en proposities Propositie Atomaire bewering, bv. “¬p”. 1. Bezit soms een DOB, verkregen door observatie of input van buiten het systeem. (Als DOB ontbreekt, dan DOB = 0 bij verstek.) 2. Bezit altijd een DOS, verkregen door een combinatie van DOB en inferentie. Altijd: DOS ≥ DOB. Regel Bijzonder soort propositie. Verbindt proposities door inferentie, bv. “a, ¬b, c −(s)→ ¬p”. Bezit, naast DOB en DOS, 1. Een regel- of implicatiesterkte, hier s: sterkte van verbinding tussen antecedent en consequent. 2. Een r-DOS: de support die door deze regel “stroomt”.
Gerard Vreeswijk
Automatisch redeneren
College 13 [16], Slide 3 [21]
Ondersteuning die een regel aan consequent geeft Laat r = “p1 , . . . , pn −(s)→ q” Laat alle voorwaarden bekend zijn voor de toepassing van r: - DOS(p1 ) , . . . , DOS(pn ) - DOS(r) - De implicatiesterkte s Dan wordt r’s support voor q gegeven door DOS(r; q) =Def s ∗ min{DOS(p1 ), . . . , DOS(pn ), DOS(r)}
Gerard Vreeswijk
Automatisch redeneren
College 13 [16], Slide 4 [21]
Voorbeeld van berekening van support-per-regel Propositie
DOB
r1
1.00
waarbij r1 = “b, c −(0.89)→ a”
r2
1.00
waarbij r2 = “d −(0.94)→ c”
a
0.00
b
0.97
c
0.00
d
0.98
Gerard Vreeswijk
Automatisch redeneren
College 13 [16], Slide 5 [21]
Voorbeeld van berekening DOS(r1 ; a) Volgens eerdere definitie: DOS(r1 ; a) = s ∗ min{DOS(r1 ), DOS(b), DOS(c)}. Er geldt: DOS(r1 ) = DOB(r1 ) = 1.00 DOS(b) = DOB(b) = 0.97 Dus DOS(r1 ; a) = 0.89 ∗ min{1.00, 0.97, DOS(c)}.
Gerard Vreeswijk
Automatisch redeneren
College 13 [16], Slide 6 [21]
DOS(r2 ; c) = 0.94 ∗ min{DOS(r2 ), DOS(d)} Er zijn geen regels die verder r2 of d ondersteunen, zodat DOS(d) = DOB(d) = 0.98, and DOS(r2 ) = DOB(r2 ) = 1.00. Dus DOS(r2 ; c) = 0.94 ∗ min{DOS(r2 ), DOS(d)} = 0.94 ∗ min{1.00, 0.98} = 0.92 Tenslotte kan support van r1 voor a berekend worden: DOS(r1 ; a) = 0.89 ∗ min{1.00, 0.97, 0.92} = 0.82
Gerard Vreeswijk
College 13 [16], Slide 7 [21]
Automatisch redeneren
Regels zijn (ook) proposities → bezitten ook DOB en DOS
c a, b −(0.97)→ (c, d, e, f −(0.89)→ g), i.e., d 0.89
g
e f
0.97
a, b Regel r1 = “a, b −(0.97)→ r2 ”, waarbij regel r2 = “c, d, e, f −(0.89)→ g”. De antecedent van r1 is a, b en de consequent van r1 is r2 . Het is mogelijk om bv. te zeggen: DOB(r1 ) = 0.45.
Gerard Vreeswijk
College 13 [16], Slide 8 [21]
Automatisch redeneren
DOS = 1
DOS < 1
strength = 1
Zekere deductieve regels. A-priori inferenties: “cirkel → rond”; “vrijgezel → niet-getrouwd”. Inductief a-posteriori: “In nieuwsbladen staan advertenties”.
Plausibele deductieve regels. Deductieve regels a-posteriori waarvoor (nog?) geen tegenvoorbeelden zijn gevonden: “alle Denen (die ik ontmoet heb) zijn aardig”.
strength < 1
Zekere regels met weerlegbare consequent. Regels a-priori met een plausibele conclusie: “het rollen van een dobbelsteen resulteert gewoonlijk niet in een zes”; inductief a-posteriori met massieve bevestiging: “meeste vogels vliegen”.
Plausibele regels met weerlegbare consequent. Weerlegbare regels a-posteriori: “de meeste Spaniels die ik ontmoet heb waren aardig, op een paar na”.
Gerard Vreeswijk
Automatisch redeneren
College 13 [16], Slide 9 [21]
Verschil tussen regels en redenen Regel Een inferentieschema r = “p1 , . . . , pn −(s)→ q” waar de volgende parameters bekend van zijn 1. Regelsterkte s Reden Een ge¨ınstantieerde regel. Naast (1) zijn ook de volgende parameters bekend: 2. DOS(r) 3. DOS(p1 ) , . . . , DOS(pn ) 4. Met 1e-orde regels: alle variabele-instanties.a Observatie: een sterke regel kan resulteren in een zwakke reden. a Gedaan
in argumentation engine ontwikkeld i.h.k. van Europees ASPIC project. (Zoek op internet met “argumentation service platform with integrated components”).
Gerard Vreeswijk
Automatisch redeneren
College 13 [16], Slide 10 [21]
Vorig college: argument-gebaseerd redeneren Argument-gebaseerd redeneren Eerst argumenten vormen, dan argumenten tegen elkaar uitspelen. Regel-gebaseerd redeneren Support van regels met strijdige conclusies combineren. Deze berekening is vindt locaal plaats: Voorbeeld: twee regels voor p en twee regels tegen p (voor ¬p): DOS(r4 , p) = 0.9 DOS(r1 , ¬p) = 0.8 DOS(r7 , p) = 0.5 DOS(r3 , ¬p) = 0.2 Het probleem is nu om het support van deze vier regels te combineren met DOB(p) en evt. DOB(¬p).
Gerard Vreeswijk
Automatisch redeneren
College 13 [16], Slide 11 [21]
Accrual of evidence (Ned.: ophoping van bewijs) Propositie
DOS
waarbij
h −(0.83)→ ¬j
1.00
h = hittegolf
r −(0.87)→ ¬j
1.00
r = het regent
h, r −(0.91)→ j
1.00
j = joggen is plezierig
h
1.00
r
1.00
Wat kun je zeggen over j als h en r.? Twee strijdige visies: 1. Meest specifieke regel wint: h, r −(0.91)→ j. 2. Bewijs uit de eerste twee regels kan gecombineerd worden: h −(0.83)→ ¬j en r −(0.87)→ ¬j levert support (0.83 + 0.87)/(1 + 0.83 ∗ 0.87) = 0.99.
Gerard Vreeswijk
Automatisch redeneren
College 13 [16], Slide 12 [21]
Ondersteuning door onafhankelijke regels Laat R = {r1 , . . . , rm } een verzameling onafhankelijke regels voor q zijn.a De ondersteuning van R voor q, notatie DOS(R; q), wordt gegeven door DOS(R; q) =Def DOS(r1 ; q) ⊕ · · · ⊕ DOS(rm ; q) waarbij “⊕” gedefinieerd is als x ⊕ y =Def (x + y)/(1 + xy). De hyperbolische som gedraagt zich als gewone optelling, met het verschil dat de sum altijd in [−1, 1] blijft. a Welke regels (on-)afhankelijk zijn valt in beginsel niet uit de regels zelf af te leiden en wordt
apart gespecificeerd in de kennisbank.
Gerard Vreeswijk
College 13 [16], Slide 13 [21]
Automatisch redeneren
Ondersteuning door verzameling afhankelijke regels Laat R een verzameling regels zijn voor q, en laat π = {R1 , . . . , Rm } een partitie zijn van R in onafhankelijke regel-verzamelingen. De ondersteuning van π voor q, notatie DOS(π; q), wordt gegeven door DOS(π; q) =Def max{DOS(R1 ; q), . . . , DOS(Rm ; q)} waarbij DOS(Ri ; q) gedefinieerd is als boven. Tekening: Als ri ∈ Ri en rj ∈ Rj , i 6= j dan zijn ri en rj afhankelijk.
R1 R2
R3
R4
Gerard Vreeswijk
College 13 [16], Slide 14 [21]
Automatisch redeneren
Afhankelijkheidsgraaf: regels met identieke consequent c m d
g
l
k
j
a i
b
e f h
p n q
Knoop (punt): regel voor α; kant (lijn): twee regels zijn afhankelijk. Omcirkelde knopen: een maximaal onafhankelijke verzameling regels voor α.
Gerard Vreeswijk
Automatisch redeneren
College 13 [16], Slide 15 [21]
(E´enzijdige) ondersteuning voor propositie (gross support) Laar R bestaan uit alle regels voor q. Dan GROSS (q)
=Def max{ DOS(π; q) | π is een onafhankelijke partitie van R }
Algoritme om GROSS (q) te berekenen: 1. Bereken DOS(R′ , q) voor iedere maximaal onafhankelijke verzameling R′ ⊆ R. 2. Neem de zwaarste verzameling uit (1). Komt neer op het oplossen van het maximum weighted independent set problem (MWIS). De algemene versie van dit probleem is NP-volledig.
Gerard Vreeswijk
Automatisch redeneren
College 13 [16], Slide 16 [21]
Tweezijdige ondersteuning voor propositie (nett support) Laat GROSS (p) als boven gedefinieerd zijn. Dan GROSS (p) als GROSS (p) ≥ GROSS (¬p) NETT (p) = 0 anders GROSS (¬p) als GROSS (p) < GROSS (¬p) NETT (¬p) = 0 anders. Merk op: 1. Nooit positieve support voor zowel propositie als negatie van propositie. 2. Alles-of-niets benadering ⇒ weerspiegelt karakter van argumentatie.
Gerard Vreeswijk
College 13 [16], Slide 17 [21]
Automatisch redeneren
Berekening van DOS(f ) [= NETT (f )] Prop.
DOB
Prop.
DOB
a
0.91
f
0.00
b
0.63
r1
1.00
waarbij r1 = “a, b −(0.89)→ f ”
c
0.74
r2
1.00
waarbij r2 = “b, c −(0.94)→ f ”
d
0.86
r3
1.00
waarbij r3 = “d −(0.88)→ ¬f ”
e
0.98
r4
1.00
waarbij r4 = “e −(0.73)→ ¬f ”
Te berekenen DOS(f ) en DOS(¬f ). Stap 1: GROSS (f ) en GROSS (¬f ) berekenen. Propositie f wordt ondersteund door regels r1 en r2 ; deze delen variabelen ⇒ onafhankelijkheid kan niet worden aangenomen.
Gerard Vreeswijk
College 13 [16], Slide 18 [21]
Automatisch redeneren
Berekening van DOS(f ) [= NETT (f )] (vervolg) Regels r1 en r2 zijn afhankelijk: GROSS (f )
= max{DOS(r1 ; f ), DOS(r2 ; f )} = max{min{0.91, 0.63} × 0.89, min{0.63, 0.74} × 0.94} = 0.59.
Regels r3 en r4 delen geen variabelen → we nemen onafhankelijkheid aan: GROSS (¬f )
= DOS(r1 ; f ) ⊕ DOS(r2 ; f ) = (0.86 × 0.88) ⊕ (0.98 × 0.73) = 0.96.
Stap 2: eenzijdig support combineren: DOS(f ) = DOS(¬f ) = NETT (¬f ) = 0.96.
NETT (f )
= 0.00 en
Gerard Vreeswijk
Automatisch redeneren
College 13 [16], Slide 19 [21]
Zoekalgoritme omzetten in dialoogvorm Idee: 1. Dialoog = trace zoekalgoritme. 2. Twee partijen: PRO en CON. - Prefix print statements met PRO als zoekacties positief verbonden zijn met hoofdthese. - Prefix print statements met CON, anders. 3. Wat je ziet: PRO probeert de hoofdthese met een onweerlegbare redena te verdedigen, CON tracht elke reden die PRO in de verdediging gebruikt te weerleggen (met andere redenen). Vreeswijk, G.A.W. (2001). Eight dialectic benchmarks discussed by two artificial localist disputors. Synthese, vol. 127, nr. 1-2, pp. 221-253. a Een
reden is een instantiatie van een inferentieregel.
Gerard Vreeswijk
Automatisch redeneren
College 13 [16], Slide 20 [21]
Dialoog op basis van lege database PRO probeert A te verdedigen: 1 0,0 pro: I claim that A holds. 2 1,0 con: Why? 3 0,0 pro: Um... upon closer inspection 4 0,0 pro: I see I have no grounds for A. - Eerste kolom: regelnummer. - Tweede kolom: diepte in zoekboom (= hoe vaak bewijslast is omgedraaid; vgl. aantal plies in schaak-zoekboom). - Derde kolom: diepte van de rechtvaardiging (vgl. lengte van compleet argument). - Uitspraken rechts: print-statements gesubjectiveerd naar PRO of CON.
Gerard Vreeswijk
Automatisch redeneren
College 13 [16], Slide 21 [21]
Dialoog op basis van e´ e´ n gegeven, t.w. DOB(A) = 0.98 1 0,0 pro: I claim that A holds. 2 1,0 con: Why? 3 0,0 pro: Simply because A is the case with DOS = 0.98 4 1,0 con: Frankly, I am willing to contest A: 5 1,0 con: I claim that ¬A holds. 6 2,0 pro: Why? 7 1,0 con: Um... upon closer inspection 8 1,0 con: I see I have no grounds for ¬A. 9 0,0 pro: That leaves me with A, obviously.
