Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Klauzulární logika Vlastnosti klauzulí, negace
Šárka Vavrečková Ústav informatiky, Filozoficko-přírodovědecká fakulta Slezské univerzity v Opavě
[email protected]
27. října 2008
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Věta o transferu bázového atomu p& q p
r p
q-r
q - r p&q
r
Postup: přesuneme tento atom na druhou stranu implikace, odstraníme negaci.
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Věta o transferu bázového atomu p& q p
r p
q-r
q - r p&q
r
Postup: přesuneme tento atom na druhou stranu implikace, odstraníme negaci.
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Věta o transferu bázového atomu p& q p
r p
q-r
q - r p&q
r
Postup: přesuneme tento atom na druhou stranu implikace, odstraníme negaci.
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklady 1
„Tráva není fialová.ÿ barva(trava, f ialova) barva(trava, f ialova)
2
„Když nefouká vítr, drak spadne.ÿ pocasi(vitr) pozice(drak, pada) pocasi(vitr), pozice(drak, pada)
3
„V neděli bratr nejde do školy.ÿ den v tydnu(nedele) jde(bratr, skola) den v tydnu(nedele), jde(bratr, skola)
4
„Když na mě zaútočí medvěd a nemám zbraň, neutíkám.ÿ utok(medved, ja), ma(ja, zbran) utika(ja) utok(medved, ja), utika(ja) ma(ja, zbran)
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklady 1
„Tráva není fialová.ÿ barva(trava, f ialova) barva(trava, f ialova)
2
„Když nefouká vítr, drak spadne.ÿ pocasi(vitr) pozice(drak, pada) pocasi(vitr), pozice(drak, pada)
3
„V neděli bratr nejde do školy.ÿ den v tydnu(nedele) jde(bratr, skola) den v tydnu(nedele), jde(bratr, skola)
4
„Když na mě zaútočí medvěd a nemám zbraň, neutíkám.ÿ utok(medved, ja), ma(ja, zbran) utika(ja) utok(medved, ja), utika(ja) ma(ja, zbran)
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklady 1
„Tráva není fialová.ÿ barva(trava, f ialova) barva(trava, f ialova)
2
„Když nefouká vítr, drak spadne.ÿ pocasi(vitr) pozice(drak, pada) pocasi(vitr), pozice(drak, pada)
3
„V neděli bratr nejde do školy.ÿ den v tydnu(nedele) jde(bratr, skola) den v tydnu(nedele), jde(bratr, skola)
4
„Když na mě zaútočí medvěd a nemám zbraň, neutíkám.ÿ utok(medved, ja), ma(ja, zbran) utika(ja) utok(medved, ja), utika(ja) ma(ja, zbran)
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklady 1
„Tráva není fialová.ÿ barva(trava, f ialova) barva(trava, f ialova)
2
„Když nefouká vítr, drak spadne.ÿ pocasi(vitr) pozice(drak, pada) pocasi(vitr), pozice(drak, pada)
3
„V neděli bratr nejde do školy.ÿ den v tydnu(nedele) jde(bratr, skola) den v tydnu(nedele), jde(bratr, skola)
4
„Když na mě zaútočí medvěd a nemám zbraň, neutíkám.ÿ utok(medved, ja), ma(ja, zbran) utika(ja) utok(medved, ja), utika(ja) ma(ja, zbran)
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Postup §c( A) ∀x( A) ∀x(p(x) ∀x(p(x) p(X)
(∀cA) (§xA)
r(x) - (§u q(x, u))) ∀x∀u(p(x) r(x) - (∀u q(x, u))) ∀x§u(p(x)
p(X) r(X), q(X, U ) r(X), q(X, @U (X))
r(x) - q(x, u)) r(x) - q(x, u))
p(X), q(X, U ) r(X) p(X), q(X, @U (X)) r(X)
existenční term nahradíme novou proměnnou, proměnnou nahradíme novou existenční konstantou nebo existenčním funktorem podle výsledku skolemizace, negaci (teď už přímo u predikátu) řešíme postupem stejným jako u bázových atomů.
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Postup §c( A) ∀x( A) ∀x(p(x) ∀x(p(x) p(X)
(∀cA) (§xA)
r(x) - (§u q(x, u))) ∀x∀u(p(x) r(x) - (∀u q(x, u))) ∀x§u(p(x)
p(X) r(X), q(X, U ) r(X), q(X, @U (X))
r(x) - q(x, u)) r(x) - q(x, u))
p(X), q(X, U ) r(X) p(X), q(X, @U (X)) r(X)
existenční term nahradíme novou proměnnou, proměnnou nahradíme novou existenční konstantou nebo existenčním funktorem podle výsledku skolemizace, negaci (teď už přímo u predikátu) řešíme postupem stejným jako u bázových atomů.
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Postup §c( A) ∀x( A) ∀x(p(x) ∀x(p(x) p(X)
(∀cA) (§xA)
r(x) - (§u q(x, u))) ∀x∀u(p(x) r(x) - (∀u q(x, u))) ∀x§u(p(x)
p(X) r(X), q(X, U ) r(X), q(X, @U (X))
r(x) - q(x, u)) r(x) - q(x, u))
p(X), q(X, U ) r(X) p(X), q(X, @U (X)) r(X)
existenční term nahradíme novou proměnnou, proměnnou nahradíme novou existenční konstantou nebo existenčním funktorem podle výsledku skolemizace, negaci (teď už přímo u predikátu) řešíme postupem stejným jako u bázových atomů.
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Postup §c( A) ∀x( A) ∀x(p(x) ∀x(p(x) p(X)
(∀cA) (§xA)
r(x) - (§u q(x, u))) ∀x∀u(p(x) r(x) - (∀u q(x, u))) ∀x§u(p(x)
p(X) r(X), q(X, U ) r(X), q(X, @U (X))
r(x) - q(x, u)) r(x) - q(x, u))
p(X), q(X, U ) r(X) p(X), q(X, @U (X)) r(X)
existenční term nahradíme novou proměnnou, proměnnou nahradíme novou existenční konstantou nebo existenčním funktorem podle výsledku skolemizace, negaci (teď už přímo u predikátu) řešíme postupem stejným jako u bázových atomů.
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Postup §c( A) ∀x( A) ∀x(p(x) ∀x(p(x) p(X)
(∀cA) (§xA)
r(x) - (§u q(x, u))) ∀x∀u(p(x) r(x) - (∀u q(x, u))) ∀x§u(p(x)
p(X) r(X), q(X, U ) r(X), q(X, @U (X))
r(x) - q(x, u)) r(x) - q(x, u))
p(X), q(X, U ) r(X) p(X), q(X, @U (X)) r(X)
existenční term nahradíme novou proměnnou, proměnnou nahradíme novou existenční konstantou nebo existenčním funktorem podle výsledku skolemizace, negaci (teď už přímo u predikátu) řešíme postupem stejným jako u bázových atomů.
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Postup §c( A) ∀x( A) ∀x(p(x) ∀x(p(x) p(X)
(∀cA) (§xA)
r(x) - (§u q(x, u))) ∀x∀u(p(x) r(x) - (∀u q(x, u))) ∀x§u(p(x)
p(X) r(X), q(X, U ) r(X), q(X, @U (X))
r(x) - q(x, u)) r(x) - q(x, u))
p(X), q(X, U ) r(X) p(X), q(X, @U (X)) r(X)
existenční term nahradíme novou proměnnou, proměnnou nahradíme novou existenční konstantou nebo existenčním funktorem podle výsledku skolemizace, negaci (teď už přímo u predikátu) řešíme postupem stejným jako u bázových atomů.
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklady 1
Někdo nemá jedničku z logiky. (∀c znamka(c, logika, 1)) §c znamka(c, logika, 1) znamka(@c, logika, 1)
2
Nikdo nemá jedničku z logiky. (§x znamka(x, logika, 1)) ∀x znamka(x, logika, 1) znamka(X, logika, 1)
3
Nikdo v neděli nechodí do školy. den v tydnu(nedele), jde(X, skola)
4
Rostliny, které nejsou byliny ani keře, jsou stromy. ∀X(rostlina(X) & bylina(X) & ker(X) strom(X)) rostlina(X) bylina(X), ker(X), strom(X)
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklady 1
Někdo nemá jedničku z logiky. (∀c znamka(c, logika, 1)) §c znamka(c, logika, 1) znamka(@c, logika, 1)
2
Nikdo nemá jedničku z logiky. (§x znamka(x, logika, 1)) ∀x znamka(x, logika, 1) znamka(X, logika, 1)
3
Nikdo v neděli nechodí do školy. den v tydnu(nedele), jde(X, skola)
4
Rostliny, které nejsou byliny ani keře, jsou stromy. ∀X(rostlina(X) & bylina(X) & ker(X) strom(X)) rostlina(X) bylina(X), ker(X), strom(X)
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklady 1
Někdo nemá jedničku z logiky. (∀c znamka(c, logika, 1)) §c znamka(c, logika, 1) znamka(@c, logika, 1)
2
Nikdo nemá jedničku z logiky. (§x znamka(x, logika, 1)) ∀x znamka(x, logika, 1) znamka(X, logika, 1)
3
Nikdo v neděli nechodí do školy. den v tydnu(nedele), jde(X, skola)
4
Rostliny, které nejsou byliny ani keře, jsou stromy. ∀X(rostlina(X) & bylina(X) & ker(X) strom(X)) rostlina(X) bylina(X), ker(X), strom(X)
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklady 1
Někdo nemá jedničku z logiky. (∀c znamka(c, logika, 1)) §c znamka(c, logika, 1) znamka(@c, logika, 1)
2
Nikdo nemá jedničku z logiky. (§x znamka(x, logika, 1)) ∀x znamka(x, logika, 1) znamka(X, logika, 1)
3
Nikdo v neděli nechodí do školy. den v tydnu(nedele), jde(X, skola)
4
Rostliny, které nejsou byliny ani keře, jsou stromy. ∀X(rostlina(X) & bylina(X) & ker(X) strom(X)) rostlina(X) bylina(X), ker(X), strom(X)
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Vytvoření popírající množiny klauzule A = p 1 & p 2 & . . . & pn , K = q1 - q2 - . . . - qm . (A
Klauzulární logika
K)
A K
(A & K) ... q1 q2 ... qm
p1 p2 pn UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Vytvoření popírající množiny klauzule A = p 1 & p 2 & . . . & pn , K = q1 - q2 - . . . - qm . (A
Klauzulární logika
K)
A K
(A & K) ... q1 q2 ... qm
p1 p2 pn UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Vytvoření popírající množiny klauzule A = p 1 & p 2 & . . . & pn , K = q1 - q2 - . . . - qm . (A
Klauzulární logika
K)
A K
(A & K) ... q1 q2 ... qm
p1 p2 pn UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklad 1 1
Každé vadné zboží je reklamováno. Klauzule: zbozi(X), vadny(X)
Klauzulární logika
reklamace(X)
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklad 1 1
Každé vadné zboží je reklamováno. Klauzule: zbozi(X), vadny(X)
reklamace(X)
Predikátová logika: ∀v((zbozi(v) & vadny(v)) reklamace(v)) §v((zbozi(v) & vadny(v)) & reklamace(v)) §v(zbozi(v) & vadny(v) & reklamace(v))
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklad 1 1
Každé vadné zboží je reklamováno. Klauzule: zbozi(X), vadny(X)
reklamace(X)
Predikátová logika: ∀v((zbozi(v) & vadny(v)) reklamace(v)) §v((zbozi(v) & vadny(v)) & reklamace(v)) §v(zbozi(v) & vadny(v) & reklamace(v)) Negovaná klauzule: zbozi(@c) vadny(@c) reklamace(@c) Negovaná věta: Některé vadné zboží není reklamováno. Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklad 1 2
Některé hračky mají rády všechny děti. Klauzule: dite(X), hracka(@h)
Klauzulární logika
rad(X, @h)
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklad 1 2
Některé hračky mají rády všechny děti. Klauzule: dite(X), hracka(@h)
rad(X, @h)
Predikátová logika: (§h∀d(dite(d) & hracka(h) rad(d, h)) ∀h§d(dite(d) & hracka(h) & rad(d, h))
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklad 1 2
Některé hračky mají rády všechny děti. Klauzule: dite(X), hracka(@h)
rad(X, @h)
Predikátová logika: (§h∀d(dite(d) & hracka(h) rad(d, h)) ∀h§d(dite(d) & hracka(h) & rad(d, h)) Negovaná klauzule: dite(@f (Y )) hracka(Y ) rad(@f (Y ), Y ) Negovaná věta: Pro každou hračku existuje dítě, které ji nemá rádo. Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklad 2 Pokud je někdo uvnitř, pak dům není prázdný.
Predikátová logika: (§N uvnitr(N, dum)) prazdny(dum) ( §N uvnitr(N, dum)) - prazdny(dum) (∀N uvnitr(N, dum)) - prazdny(dum) ∀N ( uvnitr(N, dum) - prazdny(dum)) ∀N (f alse ( uvnitr(N, dum) - prazdny(dum)))
Klauzulární logika: uvnitr(N, dum), prazdny(dum)
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklad 2 Pokud je někdo uvnitř, pak dům není prázdný.
Predikátová logika: (§N uvnitr(N, dum)) prazdny(dum) ( §N uvnitr(N, dum)) - prazdny(dum) (∀N uvnitr(N, dum)) - prazdny(dum) ∀N ( uvnitr(N, dum) - prazdny(dum)) ∀N (f alse ( uvnitr(N, dum) - prazdny(dum)))
Klauzulární logika: uvnitr(N, dum), prazdny(dum)
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklad 2 Pokud je někdo uvnitř, pak dům není prázdný.
Predikátová logika: (§N uvnitr(N, dum)) prazdny(dum) ( §N uvnitr(N, dum)) - prazdny(dum) (∀N uvnitr(N, dum)) - prazdny(dum) ∀N ( uvnitr(N, dum) - prazdny(dum)) ∀N (f alse ( uvnitr(N, dum) - prazdny(dum)))
Klauzulární logika: uvnitr(N, dum), prazdny(dum)
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklad 2 Pokud je někdo uvnitř, pak dům není prázdný.
Predikátová logika: (§N uvnitr(N, dum)) prazdny(dum) ( §N uvnitr(N, dum)) - prazdny(dum) (∀N uvnitr(N, dum)) - prazdny(dum) ∀N ( uvnitr(N, dum) - prazdny(dum)) ∀N (f alse ( uvnitr(N, dum) - prazdny(dum)))
Klauzulární logika: uvnitr(N, dum), prazdny(dum)
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklad 2 Pokud je někdo uvnitř, pak dům není prázdný.
Predikátová logika: (§N uvnitr(N, dum)) prazdny(dum) ( §N uvnitr(N, dum)) - prazdny(dum) (∀N uvnitr(N, dum)) - prazdny(dum) ∀N ( uvnitr(N, dum) - prazdny(dum)) ∀N (f alse ( uvnitr(N, dum) - prazdny(dum)))
Klauzulární logika: uvnitr(N, dum), prazdny(dum)
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklad 2 Pokud je někdo uvnitř, pak dům není prázdný.
Predikátová logika: (§N uvnitr(N, dum)) prazdny(dum) ( §N uvnitr(N, dum)) - prazdny(dum) (∀N uvnitr(N, dum)) - prazdny(dum) ∀N ( uvnitr(N, dum) - prazdny(dum)) ∀N (f alse ( uvnitr(N, dum) - prazdny(dum)))
Klauzulární logika: uvnitr(N, dum), prazdny(dum)
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklad 2 Pokud je někdo uvnitř, pak dům není prázdný.
Predikátová logika: (§N uvnitr(N, dum)) prazdny(dum) ( §N uvnitr(N, dum)) - prazdny(dum) (∀N uvnitr(N, dum)) - prazdny(dum) ∀N ( uvnitr(N, dum) - prazdny(dum)) ∀N (f alse ( uvnitr(N, dum) - prazdny(dum)))
Klauzulární logika: uvnitr(N, dum), prazdny(dum)
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklad 2 Není pravda, že pokud je někdo uvnitř, pak dům není prázdný.
Negace v predikátové logice: (∀N ( uvnitr(N, dum) - prazdny(dum))) §N ( uvnitr(N, dum) - prazdny(dum)) §N (uvnitr(N, dum) & prazdny(dum)) §N (f alse (uvnitr(N, dum) & prazdny(dum)))
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklad 2 Není pravda, že pokud je někdo uvnitř, pak dům není prázdný.
Negace v predikátové logice: (∀N ( uvnitr(N, dum) - prazdny(dum))) §N ( uvnitr(N, dum) - prazdny(dum)) §N (uvnitr(N, dum) & prazdny(dum)) §N (f alse (uvnitr(N, dum) & prazdny(dum)))
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklad 2 Není pravda, že pokud je někdo uvnitř, pak dům není prázdný.
Negace v predikátové logice: (∀N ( uvnitr(N, dum) - prazdny(dum))) §N ( uvnitr(N, dum) - prazdny(dum)) §N (uvnitr(N, dum) & prazdny(dum)) §N (f alse (uvnitr(N, dum) & prazdny(dum)))
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklad 2 Není pravda, že pokud je někdo uvnitř, pak dům není prázdný.
Negace v predikátové logice: (∀N ( uvnitr(N, dum) - prazdny(dum))) §N ( uvnitr(N, dum) - prazdny(dum)) §N (uvnitr(N, dum) & prazdny(dum)) §N (f alse (uvnitr(N, dum) & prazdny(dum)))
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklad 2 Není pravda, že pokud je někdo uvnitř, pak dům není prázdný.
Negace v predikátové logice: (∀N ( uvnitr(N, dum) - prazdny(dum))) §N ( uvnitr(N, dum) - prazdny(dum)) §N (uvnitr(N, dum) & prazdny(dum)) §N (f alse (uvnitr(N, dum) & prazdny(dum)))
Negace v klauzulární logice: uvnitr(@N, dum) prazdny(dum) (Někdo je uvnitř a zároveň je dům prázdný.) Původní klauzule: uvnitr(N, dum), prazdny(dum) Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Postup pro bázovou klauzuli: Mezi klauzulemi v množině je vztah konjunkce, podle toho postupujeme při ekvivalentních úpravách. Cíl: konjunkce jako hlavní spojka ve formuli, v podformulích jsou hlavními spojkami implikace, atd. Pro množinu dvou klauzulí: ((A1 K1 ) & (A2 K2 )) (A1
K1 ) - (A2
K2 )
(A1 & K1 ) - (A2 & K2 ) (A1 - (A2 & K2 )) & ( K1 - (A2 & K2 )) (A1 - A2 ) & (A1 - K2 ) & ( K1 - A2 ) & ( K1 - K2 ) ( A1
Klauzulární logika
A2 ) & (K2
A1 ) & (K1
A2 ) & (K1
K2 )
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Postup pro bázovou klauzuli: Mezi klauzulemi v množině je vztah konjunkce, podle toho postupujeme při ekvivalentních úpravách. Cíl: konjunkce jako hlavní spojka ve formuli, v podformulích jsou hlavními spojkami implikace, atd. Pro množinu dvou klauzulí: ((A1 K1 ) & (A2 K2 )) (A1
K1 ) - (A2
K2 )
(A1 & K1 ) - (A2 & K2 ) (A1 - (A2 & K2 )) & ( K1 - (A2 & K2 )) (A1 - A2 ) & (A1 - K2 ) & ( K1 - A2 ) & ( K1 - K2 ) ( A1
Klauzulární logika
A2 ) & (K2
A1 ) & (K1
A2 ) & (K1
K2 )
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Postup pro bázovou klauzuli: Mezi klauzulemi v množině je vztah konjunkce, podle toho postupujeme při ekvivalentních úpravách. Cíl: konjunkce jako hlavní spojka ve formuli, v podformulích jsou hlavními spojkami implikace, atd. Pro množinu dvou klauzulí: ((A1 K1 ) & (A2 K2 )) (A1
K1 ) - (A2
K2 )
(A1 & K1 ) - (A2 & K2 ) (A1 - (A2 & K2 )) & ( K1 - (A2 & K2 )) (A1 - A2 ) & (A1 - K2 ) & ( K1 - A2 ) & ( K1 - K2 ) ( A1
Klauzulární logika
A2 ) & (K2
A1 ) & (K1
A2 ) & (K1
K2 )
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Postup pro bázovou klauzuli: Mezi klauzulemi v množině je vztah konjunkce, podle toho postupujeme při ekvivalentních úpravách. Cíl: konjunkce jako hlavní spojka ve formuli, v podformulích jsou hlavními spojkami implikace, atd. Pro množinu dvou klauzulí: ((A1 K1 ) & (A2 K2 )) (A1
K1 ) - (A2
K2 )
(A1 & K1 ) - (A2 & K2 ) (A1 - (A2 & K2 )) & ( K1 - (A2 & K2 )) (A1 - A2 ) & (A1 - K2 ) & ( K1 - A2 ) & ( K1 - K2 ) ( A1
Klauzulární logika
A2 ) & (K2
A1 ) & (K1
A2 ) & (K1
K2 )
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Postup pro bázovou klauzuli: Mezi klauzulemi v množině je vztah konjunkce, podle toho postupujeme při ekvivalentních úpravách. Cíl: konjunkce jako hlavní spojka ve formuli, v podformulích jsou hlavními spojkami implikace, atd. Pro množinu dvou klauzulí: ((A1 K1 ) & (A2 K2 )) (A1
K1 ) - (A2
K2 )
(A1 & K1 ) - (A2 & K2 ) (A1 - (A2 & K2 )) & ( K1 - (A2 & K2 )) (A1 - A2 ) & (A1 - K2 ) & ( K1 - A2 ) & ( K1 - K2 ) ( A1
Klauzulární logika
A2 ) & (K2
A1 ) & (K1
A2 ) & (K1
K2 )
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Postup pro bázovou klauzuli: Mezi klauzulemi v množině je vztah konjunkce, podle toho postupujeme při ekvivalentních úpravách. Cíl: konjunkce jako hlavní spojka ve formuli, v podformulích jsou hlavními spojkami implikace, atd. Pro množinu dvou klauzulí: ((A1 K1 ) & (A2 K2 )) (A1
K1 ) - (A2
K2 )
(A1 & K1 ) - (A2 & K2 ) (A1 - (A2 & K2 )) & ( K1 - (A2 & K2 )) (A1 - A2 ) & (A1 - K2 ) & ( K1 - A2 ) & ( K1 - K2 ) ( A1
Klauzulární logika
A2 ) & (K2
A1 ) & (K1
A2 ) & (K1
K2 )
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Postup pro bázovou klauzuli: Mezi klauzulemi v množině je vztah konjunkce, podle toho postupujeme při ekvivalentních úpravách. Cíl: konjunkce jako hlavní spojka ve formuli, v podformulích jsou hlavními spojkami implikace, atd. Pro množinu dvou klauzulí: ((A1 K1 ) & (A2 K2 )) (A1
K1 ) - (A2
K2 )
(A1 & K1 ) - (A2 & K2 ) (A1 - (A2 & K2 )) & ( K1 - (A2 & K2 )) (A1 - A2 ) & (A1 - K2 ) & ( K1 - A2 ) & ( K1 - K2 ) ( A1
Klauzulární logika
A2 ) & (K2
A1 ) & (K1
A2 ) & (K1
K2 )
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklad včetně proměnných Pokud je někdo uvnitř, pak dům není prázdný. Někdo není uvnitř.
Bez negace Predikátová logika: ( §N uvnitr(N, dum)) - prazdny(dum)) & §X uvnitr(X, dum) Klauzulární logika: uvnitr(N, dum), prazdny(dum) uvnitr(@X, dum)
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklad včetně proměnných Pokud je někdo uvnitř, pak dům není prázdný. Někdo není uvnitř.
Bez negace Predikátová logika: ( §N uvnitr(N, dum)) - prazdny(dum)) & §X uvnitr(X, dum) Klauzulární logika: uvnitr(N, dum), prazdny(dum) uvnitr(@X, dum)
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklad včetně proměnných Pokud je někdo uvnitř, pak dům není prázdný. Někdo není uvnitř.
Bez negace Predikátová logika: ( §N uvnitr(N, dum)) - prazdny(dum)) & §X uvnitr(X, dum) Klauzulární logika: uvnitr(N, dum), prazdny(dum) uvnitr(@X, dum)
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklad včetně proměnných Pokud je někdo uvnitř, pak dům není prázdný. Někdo není uvnitř.
Negace: (§N uvnitr(N, dum) & prazdny(dum)) - (∀X uvnitr(X, dum)) §N ∀X((uvnitr(N, dum) - uvnitr(X, dum)) & & ∀X(prazdny(dum) - uvnitr(X, dum))) Do klauzulární logiky: uvnitr(@N, dum), uvnitr(X, dum) prazdny(dum), uvnitr(X, dum) Původní klauzule: uvnitr(N, dum), prazdny(dum) uvnitr(@X, dum) Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklad včetně proměnných Pokud je někdo uvnitř, pak dům není prázdný. Někdo není uvnitř.
Negace: (§N uvnitr(N, dum) & prazdny(dum)) - (∀X uvnitr(X, dum)) §N ∀X((uvnitr(N, dum) - uvnitr(X, dum)) & & ∀X(prazdny(dum) - uvnitr(X, dum))) Do klauzulární logiky: uvnitr(@N, dum), uvnitr(X, dum) prazdny(dum), uvnitr(X, dum) Původní klauzule: uvnitr(N, dum), prazdny(dum) uvnitr(@X, dum) Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklad včetně proměnných Pokud je někdo uvnitř, pak dům není prázdný. Někdo není uvnitř.
Negace: (§N uvnitr(N, dum) & prazdny(dum)) - (∀X uvnitr(X, dum)) §N ∀X((uvnitr(N, dum) - uvnitr(X, dum)) & & ∀X(prazdny(dum) - uvnitr(X, dum))) Do klauzulární logiky: uvnitr(@N, dum), uvnitr(X, dum) prazdny(dum), uvnitr(X, dum) Původní klauzule: uvnitr(N, dum), prazdny(dum) uvnitr(@X, dum) Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklad včetně proměnných Pokud je někdo uvnitř, pak dům není prázdný. Někdo není uvnitř.
Negace: (§N uvnitr(N, dum) & prazdny(dum)) - (∀X uvnitr(X, dum)) §N ∀X((uvnitr(N, dum) - uvnitr(X, dum)) & & ∀X(prazdny(dum) - uvnitr(X, dum))) Do klauzulární logiky: uvnitr(@N, dum), uvnitr(X, dum) prazdny(dum), uvnitr(X, dum) Původní klauzule: uvnitr(N, dum), prazdny(dum) uvnitr(@X, dum) Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Predikát rovnosti vrací true, jestliže jsou oba argumenty (po interpretaci) shodné, tvar 1 2
postfixový: = (argument1, argument2) infixový: argument1 = argument2
další podobné relační operátory: <, A, atd.
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Predikát rovnosti vrací true, jestliže jsou oba argumenty (po interpretaci) shodné, tvar 1 2
postfixový: = (argument1, argument2) infixový: argument1 = argument2
další podobné relační operátory: <, A, atd.
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Predikát rovnosti vrací true, jestliže jsou oba argumenty (po interpretaci) shodné, tvar 1 2
postfixový: = (argument1, argument2) infixový: argument1 = argument2
další podobné relační operátory: <, A, atd.
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklady 1
Slepic je 25. pocet(slepice, 25) nebo pocet(slepice) = 25
2
Barva zralých jahod je červená. jahoda(X), zraly(X) barva(X) = cervena nebo jahoda(X), zraly(X) barva(X, cervena) nebo X = jahoda, zraly(X) barva(X) = cervena
3
Kuchařka potřebuje vařechu. kucharka(X) potrebuje(X, varecha) nebo X = kucharka potrebuje(X, varecha) ŠPATNĚ: kucharka(X) potrebuje(X) = varecha
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklady 1
Slepic je 25. pocet(slepice, 25) nebo pocet(slepice) = 25
2
Barva zralých jahod je červená. jahoda(X), zraly(X) barva(X) = cervena nebo jahoda(X), zraly(X) barva(X, cervena) nebo X = jahoda, zraly(X) barva(X) = cervena
3
Kuchařka potřebuje vařechu. kucharka(X) potrebuje(X, varecha) nebo X = kucharka potrebuje(X, varecha) ŠPATNĚ: kucharka(X) potrebuje(X) = varecha
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklady 1
Slepic je 25. pocet(slepice, 25) nebo pocet(slepice) = 25
2
Barva zralých jahod je červená. jahoda(X), zraly(X) barva(X) = cervena nebo jahoda(X), zraly(X) barva(X, cervena) nebo X = jahoda, zraly(X) barva(X) = cervena
3
Kuchařka potřebuje vařechu. kucharka(X) potrebuje(X, varecha) nebo X = kucharka potrebuje(X, varecha) ŠPATNĚ: kucharka(X) potrebuje(X) = varecha
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklady 4
Pes má uši. pes(X) ma(X, usi) nebo X = pes ma(X, usi) ŠPATNĚ: pes(X) ma(X) = usi
5
Jestliže je nějaké číslo dvojnásobkem jiného celého čísla, pak je sudé. Predikátová logika: ∀X((§N (cele(N ) & X = 2 ċ N )) sude(X)) ∀X( (§N (cele(N ) & X = 2 ċ N )) - sude(X)) ∀X∀N ( cele(N ) - (X = 2 ċ N ) - sude(X)) ∀X∀N (true cele(N ) - (X = 2 ċ N ) - sude(X)) Klauzule: cele(X), X = 2 ċ N sude(X)
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklady 4
Pes má uši. pes(X) ma(X, usi) nebo X = pes ma(X, usi) ŠPATNĚ: pes(X) ma(X) = usi
5
Jestliže je nějaké číslo dvojnásobkem jiného celého čísla, pak je sudé. Predikátová logika: ∀X((§N (cele(N ) & X = 2 ċ N )) sude(X)) ∀X( (§N (cele(N ) & X = 2 ċ N )) - sude(X)) ∀X∀N ( cele(N ) - (X = 2 ċ N ) - sude(X)) ∀X∀N (true cele(N ) - (X = 2 ċ N ) - sude(X)) Klauzule: cele(X), X = 2 ċ N sude(X)
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklady 4
Pes má uši. pes(X) ma(X, usi) nebo X = pes ma(X, usi) ŠPATNĚ: pes(X) ma(X) = usi
5
Jestliže je nějaké číslo dvojnásobkem jiného celého čísla, pak je sudé. Predikátová logika: ∀X((§N (cele(N ) & X = 2 ċ N )) sude(X)) ∀X( (§N (cele(N ) & X = 2 ċ N )) - sude(X)) ∀X∀N ( cele(N ) - (X = 2 ċ N ) - sude(X)) ∀X∀N (true cele(N ) - (X = 2 ċ N ) - sude(X)) Klauzule: cele(X), X = 2 ċ N sude(X)
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklady 4
Pes má uši. pes(X) ma(X, usi) nebo X = pes ma(X, usi) ŠPATNĚ: pes(X) ma(X) = usi
5
Jestliže je nějaké číslo dvojnásobkem jiného celého čísla, pak je sudé. Predikátová logika: ∀X((§N (cele(N ) & X = 2 ċ N )) sude(X)) ∀X( (§N (cele(N ) & X = 2 ċ N )) - sude(X)) ∀X∀N ( cele(N ) - (X = 2 ċ N ) - sude(X)) ∀X∀N (true cele(N ) - (X = 2 ċ N ) - sude(X)) Klauzule: cele(X), X = 2 ċ N sude(X)
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklady 4
Pes má uši. pes(X) ma(X, usi) nebo X = pes ma(X, usi) ŠPATNĚ: pes(X) ma(X) = usi
5
Jestliže je nějaké číslo dvojnásobkem jiného celého čísla, pak je sudé. Predikátová logika: ∀X((§N (cele(N ) & X = 2 ċ N )) sude(X)) ∀X( (§N (cele(N ) & X = 2 ċ N )) - sude(X)) ∀X∀N ( cele(N ) - (X = 2 ċ N ) - sude(X)) ∀X∀N (true cele(N ) - (X = 2 ċ N ) - sude(X)) Klauzule: cele(X), X = 2 ċ N sude(X)
Klauzulární logika
UI FPF SU
Negace bázového atomu
Negace atomu s existenčním termem
Negace klauzule
Negace množiny klauzulí
Predikát rovnosti
Příklady 4
Pes má uši. pes(X) ma(X, usi) nebo X = pes ma(X, usi) ŠPATNĚ: pes(X) ma(X) = usi
5
Jestliže je nějaké číslo dvojnásobkem jiného celého čísla, pak je sudé. Predikátová logika: ∀X((§N (cele(N ) & X = 2 ċ N )) sude(X)) ∀X( (§N (cele(N ) & X = 2 ċ N )) - sude(X)) ∀X∀N ( cele(N ) - (X = 2 ċ N ) - sude(X)) ∀X∀N (true cele(N ) - (X = 2 ċ N ) - sude(X)) Klauzule: cele(X), X = 2 ċ N sude(X)
Klauzulární logika
UI FPF SU
