PriitJ: /* Lihtne resolutsioonil põhinev tõestaja */

2021-03-19T10:08:06Z

Lihtne resolutsioonil põhinev tõestaja

←Vanem redaktsioon		Redaktsioon: 19. märts 2021, kell 12:08
49. rida:		49. rida:

	Funktsioon <code>resolve(current, clause)</code> peab tagastama listi [[Iti0210lab72_resolve\|võimalikest tulemustest]], mida saadakse kahele disjunktile <code>current</code> ja <code>clause</code> resolutsioonireegli rakendamisel. See funktsioon kirjuta ise.		Funktsioon <code>resolve(current, clause)</code> peab tagastama listi [[Iti0210lab72_resolve\|võimalikest tulemustest]], mida saadakse kahele disjunktile <code>current</code> ja <code>clause</code> resolutsioonireegli rakendamisel. See funktsioon kirjuta ise.

			[[Iti0210lab72_resolve\|resolve() näited]]

	Katsetame seda algoritmi väikese ülesande peal:		Katsetame seda algoritmi väikese ülesande peal:

PriitJ: /* Ülesanne lahendamiseks */

2021-03-16T16:01:36Z

Ülesanne lahendamiseks

←Vanem redaktsioon		Redaktsioon: 16. märts 2021, kell 18:01
130. rida:		130. rida:
	== Ülesanne lahendamiseks ==		== Ülesanne lahendamiseks ==

	Meil on antud maja elektriskeem, kus on kaitsmed (''cb''), seinakontaktid (''p''), lambid (''l''), lülitid (''s'') ja juhtmed (''w''). Lepime kokku, et elektriskeem töötab nii:		Meil on antud maja elektriskeem, kus on kaitsmed (''cb''), seinakontaktid (''p''), lambid (''l''), lülitid (''s'') ja juhtmed (''w''). Valime iga elemendi - juhtme, kaitsme jne kohta ühe loogikasümboli ning ütleme, et kui näiteks ''w1'' on tõene, siis juhtmes 1 on vool. Lepime kokku, et elektriskeem töötab nii:
	# vool läbib kaitsmeid, kui need on korras (näiteks ''cb1'' on tõene). Lülitite puhul tähistab tõene ülemist asendit ja väär alumist asendit, skeemilt on näha kuidas vool neid sel juhul läbib.		# vool läbib kaitsmeid, kui need on korras (näiteks ''cb1'' on tõene). Lülitite puhul tähistab tõene ülemist asendit ja väär alumist asendit, skeemilt on näha kuidas vool neid sel juhul läbib.
	# kui juhtmes on vool, siis sellega otse ühendatud lamp põleb (ja vastupidi, põleva lambi puhul on vool juhtmes).		# kui juhtmes on vool, siis sellega otse ühendatud lamp põleb (ja vastupidi, põleva lambi puhul on vool juhtmes).

PriitJ: /* Ülesanne lahendamiseks */

2021-03-16T15:43:35Z

Ülesanne lahendamiseks

←Vanem redaktsioon		Redaktsioon: 16. märts 2021, kell 17:43
154. rida:		154. rida:

	Kuna reeglid peavad olema KNK (''CNF'') kujul, siis kasuta vajaduse korral teisendamiseks http://logictools.org/prop.html - nupp "Build" ja vali kõrvalt "clause normal form".		Kuna reeglid peavad olema KNK (''CNF'') kujul, siis kasuta vajaduse korral teisendamiseks http://logictools.org/prop.html - nupp "Build" ja vali kõrvalt "clause normal form".

			=== Esitamine ===

			Kui oled tõestustega hakkama saanud, siis README failis esita:
			# iga küsimuse juurde tehtud faktid, mis kirjeldavad antud situatsiooni
			# näide mõnest keerulisemast reeglist, võib olla nii algkujul kui KNK kujul. Kõiki reegleid pole tarvis tuua.

	[[Category:Iti0210]]		[[Category:Iti0210]]

PriitJ: Uus lehekülg: '= Resolutsioonimeetod = == Sissejuhatus == Ülesande eesmärgiks on õppida, kuidas toimib resolutsioonimeetod. Selleks: # programmeerime lihtsa versiooni resolutsioonil põhi...'

2021-03-16T15:39:11Z

Uus lehekülg: '= Resolutsioonimeetod = == Sissejuhatus == Ülesande eesmärgiks on õppida, kuidas toimib resolutsioonimeetod. Selleks: # programmeerime lihtsa versiooni resolutsioonil põhi...'

Uus lehekülg

= Resolutsioonimeetod =

== Sissejuhatus ==

Ülesande eesmärgiks on õppida, kuidas toimib resolutsioonimeetod.

Selleks:
# programmeerime lihtsa versiooni resolutsioonil põhinevast tõestajast
# testime seda ülesannete peal, kus on tarvis loogilist järeldamist

== Lihtne resolutsioonil põhinev tõestaja ==

Teadaolevate faktide (''KB'') pealt mingi lause ''alpha'' tõestamiseks piisab, kui näidata et ''KB & -alpha'' on vastuolu, ehk siis ei ole võimalik korraga väita, et ''KB'' kehtib ja ''alpha'' ei kehti. Lihtne algoritmi prototüüp selleks:

<pre>
def simple_resolution_solver(KB, neg_alpha):
# KB: list of known clauses
# clause example: a v b v -c v d
# choose your own representation, e.g. ("a", "b", "-c", "d")
# neg_alpha: query clause, already negated
# returns True if proof found, False otherwise

# initialize
todo = [neg_alpha]
done = KB.copy()

# process the todo list one by one
while todo:
current = todo.pop()

# combine current clause with all clauses we've already seen
for clause in done:
# apply resolution rule
resolvents = resolve(current, clause)
# handle new clauses generated by the resolution rule
for resolvent in resolvents:
# some important things that can happen here:
# 1. resolvent is empty: proof found that KB->alpha!
# 2. resolvent is always true: throw it away, useless clause
# ONLY if neither of these things happen:
todo.append(resolvent)

# we're done with this clause
done.append(current)

# loop ended without proof
return False
</pre>

Funktsioon <code>resolve(current, clause)</code> peab tagastama listi [[Iti0210lab72_resolve|võimalikest tulemustest]], mida saadakse kahele disjunktile <code>current</code> ja <code>clause</code> resolutsioonireegli rakendamisel. See funktsioon kirjuta ise.

Katsetame seda algoritmi väikese ülesande peal:

<pre>
P -> Q
L & M -> P
B & L -> M
A & P -> L
A & B -> L
A
B
</pre>

Tõesta, et nende reeglite ja faktide pealt järeldub ''Q''. Selleks pead reeglid kõigepealt CNF kujule viima, näiteks ''L & M -> P'' teisendub ''-L v -M v P''. Funktsioonile pead tõestatava asja ette andma eitusena (''-Q''). Pane tähele, et tõestatav asi on ka disjunkt/lause, isegi kui ta koosneb ainult ühest literaalist.

<div class="toccolours mw-collapsible mw-collapsed" style="width:400px; overflow:auto;">
'''Teooria''': ANL loop, set of support
<div class="mw-collapsible-content">
Toodud algoritm on küll lihtne, aga sisaldab juba õpiku kirjeldusega võrreldes olulisi optimisatsioone:
# [http://www.cs.miami.edu/home/geoff/Courses/CSC749-19F/Content/ANLLoop.shtml "ANL loop"] on algoritm, kus disjunktid jaotatakse "tegemata" ja "tehtud" listideks. Disjunkte võetakse ükshaaval tegemata listist ning proovitakse resolutsioonireeglit selle ja kõigi tehtud listi disjunktide vahel. Tekkinud uued disjunktid lisatakse tegemata listi. See garanteerib, et sama paari ei vaadata mitu korda.
# ''Set of support'' strateegia: kuna meil on eesmärgiks mingi fakti järeldumist kontrollida, siis see strateegia paneb "tegemata" listi ainult kontrollitava fakti ja "tehtud" listi kogu ülejäänud teadmise. Tegemata listi hakkavad siis tekkima ainult asjad, mis on kuidagi seotud meie kontrollitava faktiga. Näiteks, testülesande puhul on tegemata listis ''-Q'' ja kõik faktid tehtud listis, esimeses tsüklis tekiks kohe ''-P'' mis tähendab, et Q tõestamiseks peame esmalt tõestama P. Järgmisena leitakse P eeldused jne - see on väga sarnane ''backward chaining'' algoritmiga.
</div></div>

== Optimeeritud variant ==

Esialgne variant järeldusmootorist küll töötab, aga kui ta kohe järeldust ei leia, hakkab resolutsioonireegel piiramatult uusi disjunkte genereerima - proovi näiteks eemaldada testülesandest ''Q'' tõestamiseks vajalik fakt ''A'' ja vaata mis juhtub.

Lisame neeldumise kontrolli. Lihtsustatult öeldes kontrollitakse iga resolutsioonireegli poolt genereeritud disjunkti juures, kas oli juba enne olemas mingi disjunkt, mis sisaldab sama infot.

<pre>
def resolution_solver(KB, neg_alpha):
# KB: list of known clauses
# clause example: a v b v -c v d
# choose your own representation, e.g. ("a", "b", "-c", "d")
# neg_alpha: query clause, already negated
# returns True if proof found, False otherwise

# initialize
todo = [neg_alpha]
done = KB.copy()

# process the todo list one by one
while todo:
current = todo.pop()

# check if current is redundant
for clause in done + todo:
# if clause is a subset of current, then go back to the start of the loop
# to pick new current

# combine current clause with all clauses we've already seen
for clause in done:
# apply resolution rule
resolvents = resolve(current, clause)
# handle new clauses generated by the resolution rule
for resolvent in resolvents:
# some important things that can happen here:
# 1. resolvent is empty: proof found that KB->alpha!
# 2. resolvent is always true: throw it away, useless clause
# ONLY if neither of these things happen:
todo.append(resolvent)

# we're done with this clause
done.append(current)

# loop ended without proof
return False

</pre>

Nüüd peaks algoritm kiiresti tulemusi andma, kui tõestust ei leita. Proovi jälle testülesannet, eemaldades fakti ''A'' või vajaliku reegli ''A & B -> L''.

<div class="toccolours mw-collapsible mw-collapsed" style="width:400px; overflow:auto;">
'''Teooria''': neeldumine
<div class="mw-collapsible-content">
Kui meil on disjunktid ''A v B v C v D'' ja ''A v B v C'', siis neist esimese võib ära jätta - miks, seda saab hästi aru lühema näite pealt: ''a & (a v b)'' on ekvivalentne ''a''-ga. Resolutsioonimeetodi kontekstis nimetatakse seda tehnikat ''subsumption'', ehk neeldumine. Kui kontrollime neeldumist nii, et leiame kas üks disjunkt on teise alamhulk, siis sellega leitakse ka korduvad disjunktid.
</div></div>

== Ülesanne lahendamiseks ==

Meil on antud maja elektriskeem, kus on kaitsmed (''cb''), seinakontaktid (''p''), lambid (''l''), lülitid (''s'') ja juhtmed (''w''). Lepime kokku, et elektriskeem töötab nii:
# vool läbib kaitsmeid, kui need on korras (näiteks ''cb1'' on tõene). Lülitite puhul tähistab tõene ülemist asendit ja väär alumist asendit, skeemilt on näha kuidas vool neid sel juhul läbib.
# kui juhtmes on vool, siis sellega otse ühendatud lamp põleb (ja vastupidi, põleva lambi puhul on vool juhtmes).
# kui juhtmes on vool, siis selle küljes olevas seinakontaktis on vool - sama kehtib ka vastupidises suunas.
# juhul kui kaks juhet on omavahel lüliti või töötava kaitsmega ning ühes pole voolu, ei saa ka teises olla voolu.
# kui lamp on kustu või seinakontaktis pole voolu, siis ei saa ka nende küljes olevas juhtmes olla voolu.

[[Image:Iti0210_eldomain.png|300px|right|elektriskeem]]

''(pilt (c) D. Poole, A. Mackworth; [https://artint.info])''

'''Küsimused testimiseks'''

# Väline vool on olemas (''outside_power'') ning kaitse 2 on korras (''cb2''). Tõesta, et pistikus ''p2'' on vool.
# Väline vool on, kaitse 1 (''cb1'') on korras. Lüliti 1 (''s1'') on alumises asendis ja lüliti 2 (''s2'') ülemises asendis. Tõesta, et lamp ''l1'' ei põle.
# Väline vool on olemas, lülitid ''s1'' ja ''s2'' on samas asendis, näiteks ülemises. Lamp ''l1'' ei põle. Tõesta, et kaitse 1 (''cb1'') on katki/välja lülitunud.

Meil tuleb teha:

* reeglid, mis kirjeldavad, kuidas elektriskeem töötab
* faktid (iga küsimuse kohta eraldi).
* lause, mida hakatakse tõestama (tõestajale ette anda vastasmärgiga).

Kuna reeglid peavad olema KNK (''CNF'') kujul, siis kasuta vajaduse korral teisendamiseks http://logictools.org/prop.html - nupp "Build" ja vali kõrvalt "clause normal form".

[[Category:Iti0210]]

Iti0210lab74 - Redigeerimiste ajalugu

PriitJ: /* Lihtne resolutsioonil põhinev tõestaja */

PriitJ: /* Ülesanne lahendamiseks */

PriitJ: /* Ülesanne lahendamiseks */

PriitJ: Uus lehekülg: '= Resolutsioonimeetod = == Sissejuhatus == Ülesande eesmärgiks on õppida, kuidas toimib resolutsioonimeetod. Selleks: # programmeerime lihtsa versiooni resolutsioonil põhi...'