Chyba pri kontrole rezolvencie

[crnkjck]

V jazyku

C = { a } F = { f/1, g/1 } G = { p/2 }

som spravil takyto „dokaz“:

1. p(f(x),x) ∨ p(y, a) – assum
2. p(f(a), a) – factoring 1 { x -> a, y -> f(a) }
3. ¬p(y, g(z)) ∨ p(z, y) – assum
4. p(v, a) ∨ p(z, f(x)) ∨ -p(f(x),f(x)) – resolution 1 { y -> v } 3 { y -> f(x), x -> g(z) }

V 4. kroku je editor spokojny zo vsetkym, co je syntakticky spravne.

[crnkjck]

Hm, vyzera, ze je to len nejaky problem s tym, ako sa validuje. Lebo zrazu mi to zacalo pisat, ze to nie je rezolventa. Ale neviem zial povedat, co som zmenil.

Kazdopadne by bolo dobre, aby sa po zmene cohokolvek v kroku prevalidoval cely krok. Hlavne aby sa vzdy validovalo, ci je formula rezolventa/faktor. Ak sa to neda urcit, lebo v premenovani, premise, unifikatore je chyba alebo premisa je prazdna, treba to povedat aj pri formule, napr. DependencyError: Can't validate if the formula is a resolvent/factor. Bolo by dobre vyznacit aj to, ze premisy su prazdne ako chybu.

[crnkjck]

Celkom som sa zapotil, kym som prisiel na to, co je vlastne spravna rezolventa v 4. kroku. Nakoniec som pouzil Robinson ;-)

• p(v, a) ∨ p(z, f(g(z))) – resolution 1 { y -> v }, 2 { x -> g(z), y -> f(g(z)) }

Okrem toho sa 3 da zrezolvovat sama so sebou:

• ¬p(g(z), g(y)) ∨ p(z, y) – resolution 3 { y -> v, z -> x }, 3 { v -> g(z), x -> y }

[crnkjck]

Dohodi sme sa na refaktorizacii validacie.

Validacne funkcie pre komponenty kroku (vacsina uz funguje takto):

• Dostanu svoju cast stavu + id kroku.
• Ocakavaju, ze v stave je uz nastavena nova hodnota .input.
• Zvaliduju, zapisu chybu do .error alebo sparsovanu hodnotu do .object.
• Vratia dvojprvkove pole: boolean indikujuci, ci je vsetko v poriadu + novu cast stavu.

Tieto funkcie sa nebudu volat zo step, ale z validateStep. Sucasny validateStep by sa asi mal premenovat na validateRule.

Novy validateStep by mal postupne zavolat validaciu vsetkych komponentov (bez ohladu na to, ci sa zmenili alebo nie). Ak vsetky prejdu, zavola validateRule. Nakoniec posklada vsetky ciastocne stavy do noveho stavu a vrati ho.