% Zotriedenie literalov v klauzulach
%    [[p(a), n(b)], [p(w), p(q)]] -> [[n(b), p(a)], [p(q), p(w)]]
% Pri hladani rovnakych klauzul nebude potrebne uvazovat rozlicne
% mozne poradia literalov, pre urcenie zhodnosti klauzul postaci
% porovnanie dvoch zoznamov.
zotried_literaly([],[]).
zotried_literaly([NezotriedenaKlauzula|NK],[ZotriedenaKlauzula|ZK]) :-
    sort(NezotriedenaKlauzula,ZotriedenaKlauzula),
    zotried_literaly(NK,ZK).

% Potvrdenie vyskytu komplementarneho literalu v klauzule
%    p(a), [n(q), n(a)] -> true
%    p(a), [n(q), p(a)] -> false
%    p(a), [n(q), n(w)] -> false
potvrd_komplement(p(S),[n(S)|_]) :- !.
potvrd_komplement(n(S),[p(S)|_]) :- !.
potvrd_komplement(Literal,[_|OstatneLiteraly]) :-
    potvrd_komplement(Literal,OstatneLiteraly).

% Vyhladanie symbolov, ktore v zadanych dvoch klauzulach vystupuju
% v podobe komplementarnych literalov
%    [p(a), p(b)], [n(a), n(b)] -> [a, b]
%    [p(a), p(b)], [n(a), p(b)] -> [a]
%    [p(a), p(b)], [p(a), p(b)] -> []
% Pre symbol kazdeho literalu z prvej klauzuly sa kontroluje, ci
% sa v druhej klauzule vyskytuje komplementarny literal.
komplementarne_symboly([],_,[]).
komplementarne_symboly([p(S)|OstatneLiteraly],Klauzula,[S|OstatneSymboly]) :-
    potvrd_komplement(p(S),Klauzula),
    komplementarne_symboly(OstatneLiteraly,Klauzula,OstatneSymboly), !.
komplementarne_symboly([n(S)|OstatneLiteraly],Klauzula,[S|OstatneSymboly]) :-
    potvrd_komplement(n(S),Klauzula),
    komplementarne_symboly(OstatneLiteraly,Klauzula,OstatneSymboly), !.
komplementarne_symboly([_|OstatneLiteraly],Klauzula,OstatneSymboly) :-
    komplementarne_symboly(OstatneLiteraly,Klauzula,OstatneSymboly).

% Z klauzuly sa vypustia vsetky literaly, ktore su odvodene od zadaneho
% symbolu
%    [p(a), n(b)], s -> [p(a), n(b)]
%    [p(a), n(b)], a -> [n(b)]
%    [p(a), n(b)], b -> [p(a)]
vyhod([],_,[]).
vyhod([p(Symbol)|OstatneLiteraly],Symbol,RedukovaneLiteraly) :-
    vyhod(OstatneLiteraly,Symbol,RedukovaneLiteraly), !.
vyhod([n(Symbol)|OstatneLiteraly],Symbol,RedukovaneLiteraly) :-
    vyhod(OstatneLiteraly,Symbol,RedukovaneLiteraly), !.
vyhod([InySymbol|OstatneLiteraly],Symbol,[InySymbol|RedukovaneLiteraly]) :-
    vyhod(OstatneLiteraly,Symbol,RedukovaneLiteraly).

% Z klauzuly sa vypusti viacnasobny vyskyt literalov, z kazdeho
% pritomneho literalu ostane iba jeden vyskyt
%    [p(a), p(b), p(a), p(b)] -> [p(a), p(b)]
%    [p(a), p(b), n(a), p(b)] -> [p(a), n(a), p(b)]
faktoring([],[]).
faktoring([Literal|OstatneLiteraly],[Literal|FaktorovaneLiteraly]) :-
    not( member(Literal,OstatneLiteraly) ),
    faktoring(OstatneLiteraly,FaktorovaneLiteraly), !.
faktoring([_|OstatneLiteraly],FaktorovaneLiteraly) :-
    faktoring(OstatneLiteraly,FaktorovaneLiteraly).

% Zo zoznamu klauzul sa vypustia tie, ktore obsahuju literal aj
% k nemu komplementarny literal
%    [[p(a), p(b), n(a)], [n(b)]] -> [[n(b)]]
% Kedze klauzula s dvojicou komplementarnych literalov je vzdy pravdiva,
% neda sa pomocou nej odvodit spor.
vypusti_true_rezolventy([],[]).
vypusti_true_rezolventy([Rezolventa|IneRezolventy],OstavajuceRezolventy) :-
    member(p(S),Rezolventa),
    member(n(S),Rezolventa),
    vypusti_true_rezolventy(IneRezolventy,OstavajuceRezolventy), !.
vypusti_true_rezolventy([Rezolventa|IneRezolventy],
                        [Rezolventa|OstavajuceRezolventy]) :-
    vypusti_true_rezolventy(IneRezolventy,OstavajuceRezolventy), !.

% Rezolucia dvoch klauzul pri znamom zozname symbolov, ktore su
% v klauzulach v oboch podobach
%    [p(a), p(b)], [n(a), n(b)], [a, b] -> [[n(b), p(b)], [n(a), p(a)]]
%    [p(a), p(b)], [n(a), p(b)], [a] -> [[p(b)]]
%    [p(a)], [n(b)], [] -> []
%    [p(a)], [n(a)], [a] -> [[]]
% Pre kazdy z komplementarne sa vyskytujucich symbolov sa vytvori
% jedna rezolventa, ktora je faktorovana a jej literaly su zotriedene.
% Vystupom je teda zoznam rezolvent.
rezolucia(_,_,[],[]).
rezolucia(KlauzulaX,KlauzulaY,[Komplement|IneKomplementy],
                              [Rezolventa|IneRezolventy]) :-
    vyhod(KlauzulaX,Komplement,RedukovanaX),
    vyhod(KlauzulaY,Komplement,RedukovanaY),
    append(RedukovanaX,RedukovanaY,RawRezolventa),
    faktoring(RawRezolventa,FaktorovanaRezolventa),
    sort(FaktorovanaRezolventa,Rezolventa),
    rezolucia(KlauzulaX,KlauzulaY,IneKomplementy,IneRezolventy), !.

% Rezolucia dvoch klauzul
%    [p(a), p(b)], [n(a), n(c)] -> [[n(c), p(b)]]
%    [p(a), p(b)], [n(a), n(b)] -> []
%    [p(a), p(b)], [n(q), n(w)] -> []
% Najprv sa zistia symboly, z ktorych kazdy je v jednej z klauzul
% v pozitivnom zatial co v druhej z klauzul v negativnom tvare.
% Samotna rezolucia sa urobi podla tychto symbolov. Zo zoznamu
% rezolvent sa vypustia tie, ktore su vzdy splnene.
rezolucia_dvojice_klauzul(KlauzulaX,KlauzulaY,Rezolventy) :-
    komplementarne_symboly(KlauzulaX,KlauzulaY,Symboly),
    rezolucia(KlauzulaX,KlauzulaY,Symboly,NoveRezolventy),
    vypusti_true_rezolventy(NoveRezolventy,Rezolventy), !.

% Generovanie rezolvent medzi klauzulou a zoznamom klauzul
%    [p(a), p(b)], [[n(a), n(c)], [n(q), n(w)]] -> [[n(c), p(b)]]
% Generuje sa pre danu klauzulu a kazdu jednu klauzulu zo zoznamu.
klauzula_vs_predosle(_,[],[]).
klauzula_vs_predosle(Klauzula,[PredoslaKlauzula|OstatnePredosle],Odvodene) :-
    rezolucia_dvojice_klauzul(Klauzula,PredoslaKlauzula,Rezolventy),
    klauzula_vs_predosle(Klauzula,OstatnePredosle,OstatneRezolventy),
    append(Rezolventy,OstatneRezolventy,Odvodene), !.

% Generovanie rezolvent medzi dvomi zoznamami klauzul
%    [[p(a), p(b)], [n(a), n(c)]], [[n(a), p(c)]] ->
%                                [[p(b), p(c)], [n(c), p(b)], [n(a)]]
% Generuje sa medzi kazdou dvojicou klauzul, kde jedna je z prveho a druha
% z druheho zoznamu. Generuje sa aj medzi kazdou dvojicou klauzul
% z prveho zoznamu. Medzi klauzulami z druheho zoznamu sa negeneruje.
generuj_uroven([],_,[]).
generuj_uroven([Klauzula|Klauzuly],PredchadzajuceUrovne,Generovane) :-
    klauzula_vs_predosle(Klauzula,PredchadzajuceUrovne,NoveKlauzuly),
    generuj_uroven(Klauzuly,[Klauzula|PredchadzajuceUrovne],OstatneNove),
    append(NoveKlauzuly,OstatneNove,Generovane).

% Zo zoznamu vypusti vsetky klauzuly, ktore sa nachadzaju v inom zozname
% klauzul
%    [[p(a), p(b)], [n(a), n(c)]], [[p(a), p(b)]] -> [[n(a), n(c)]]
% V prvom zozname ostanu iba klauzuly, ktore sa v druhom zozname
% nevyskytuju.
redukuj([],_,[]).
redukuj([Klauzula|OstatneKlauzuly],ZoznamKlauzul,Redukovane) :-
    member(Klauzula,ZoznamKlauzul),
    redukuj(OstatneKlauzuly,ZoznamKlauzul,Redukovane), !.
redukuj([Klauzula|OstatneKlauzuly],ZoznamKlauzul,[Klauzula|Redukovane]) :-
    redukuj(OstatneKlauzuly,ZoznamKlauzul,Redukovane).

% Deduplikovanie zoznamu klauzul - ak niektora sa vyskytuje viackrat, ponecha
% sa iba jej jeden vyskyt
%    [[p(c)],[p(a),p(c)],[p(c)],[p(a),p(c)]] -> [[p(c)], [p(a), p(c)]]
vypusti_opakovane_rezolventy([],[]).
vypusti_opakovane_rezolventy([Rezolventa|Rezolventy],Jedinecne) :-
    member(Rezolventa,Rezolventy),
    vypusti_opakovane_rezolventy(Rezolventy,Jedinecne), !.
vypusti_opakovane_rezolventy([Rezolventa|Rezolventy],[Rezolventa|Jedinecne]) :-
    vypusti_opakovane_rezolventy(Rezolventy,Jedinecne).

% Tlac medzikroku pre sledovanie cinnosti algoritmu
tlac(NovaUroven,_PredchadzajuceUrovne,_AktualnaUroven) :-
    %print("---- Predchadzajuce ----"), nl,
    %print(_PredchadzajuceUrovne), nl,
    %print("---- Aktualna ----"), nl,
    %print(_AktualnaUroven), nl,
    %print("---- Nova ----"), nl,
    print(NovaUroven), nl,
    print("========"), nl.

% Kontrola, ci sa pri strategii do sirky najde spor alebo uz nie je mozne
% generovat ziadnu dosial neobjavenu klauzulu bez vyskytu sporu.
%   [],[[p(a), p(b)], [p(a), n(b)], [n(a), p(c)]] -> false (uz nic nove)
%   [],[[p(a), p(b)], [p(a), n(b)], [n(a), p(c)], [n(c)]] -> true (spor)
% Rezolvuju sa vzdy dvojice klauzul, kde jedna je z aktualnej
% urovne a jedna z aktualanej alebo predchadzajucich urovni. Generovane
% klauzuly sa redukuju kvoli opakovanemu vyskytu.
potvrd_spor(PredchadzajuceUrovne,AktualnaUroven) :-
    generuj_uroven(AktualnaUroven,PredchadzajuceUrovne,GenerovaneKlauzuly),
    vypusti_opakovane_rezolventy(GenerovaneKlauzuly,GenerovaneJedinecneKlauzuly),
    redukuj(GenerovaneJedinecneKlauzuly,AktualnaUroven,L1),
    redukuj(L1,PredchadzajuceUrovne,NovaUroven),
    tlac(NovaUroven,PredchadzajuceUrovne,AktualnaUroven),
    (member([],NovaUroven), !;
     NovaUroven == [], !, fail;
     append(AktualnaUroven,PredchadzajuceUrovne,NovePredchadzajuceUrovne),
     potvrd_spor(NovePredchadzajuceUrovne,NovaUroven)
     ), !.

% hladanie sporu
%   oporna mnozina - jedna z rezolvovanych klauzul je bud sucast
%                    negovanej hypotezy alebo jej potomok
%   do sirky - systeaticke parovanie vsetkych znamych klauzul
spor(do_sirky,KB,NegovanaHypoteza):-
    zotried_literaly(KB,ZotriedenaKB),
    zotried_literaly(NegovanaHypoteza,ZotriedenaNegovanaHypoteza),
    append(ZotriedenaNegovanaHypoteza,ZotriedenaKB,VsetkyKlauzuly),
    potvrd_spor([],VsetkyKlauzuly),
    print("SPOR POTVRDENY"),
    !, fail.
spor(oporna_mnozina,KB,NegovanaHypoteza):-
    zotried_literaly(KB,ZotriedenaKB),
    zotried_literaly(NegovanaHypoteza,ZotriedenaNegovanaHypoteza),
    potvrd_spor(ZotriedenaKB,ZotriedenaNegovanaHypoteza),
    print("SPOR POTVRDENY"),
    !, fail.
spor(_,_,_):-
    print("SPOR NEPOTVRDENY"),
    fail.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%

priklad_online(KB) :-
    KB = [[p(k),p(h)],[p(r),p(v)],[n(r),n(v)],[n(a),p(r)],
          [n(v),p(k)],[n(k),p(v)],[n(h),p(a)],[n(h),p(k)]].

% volanie:
%     ?- priklad_online(KB), spor(do_sirky,KB,NegovanaHypoteza).
%     ?- priklad_online(KB), spor(oporna_mnozina,KB,NegovanaHypoteza).
%
% Negovana hypoteza:
%    [[n(k)]]             pre hypotezu "klara je online" 
%    [[p(k)]]             pre hypotezu "klaza nie je online"
%    [[n(k), n(v)]]       pre hypotezu "klara aj Vladimir su online"
%    [[n(k)], [n(a)]]     pre hypotezu "klara alebo anna su online"