LUP - hw05

%% prove(-Formula, -Depth)
prove(Formula, Depth) :- !, my_prove([-Formula], Depth).

my_prove(_, 0) :- !, false.

%% Contradiction
my_prove(Set, _) :-
    select(A, Set, Set1),
    select(-A, Set1, _).

%% Double Negation
my_prove(Set, Depth) :-
    select( -( -A), Set, Set1),
    Depth2 is Depth-1,
    my_prove([A| Set1], Depth2).

%% Conjunction
my_prove(Set, Depth) :-
    select((A,B), Set, Set1),
    Depth2 is Depth-1,
    my_prove([A, B | Set1], Depth2).

%% Negated Conjunction
my_prove(Set, Depth) :-
    select( - (A,B), Set, Set1),
    Depth2 is Depth-1,
    my_prove([ -A | Set1], Depth2),
    my_prove([ -B | Set1], Depth2).

%% Box
my_prove(Set, Depth) :-
    select( - (box(A)), Set, Rest),
    maplist(unbox, Rest, Unboxed),
    Depth2 is Depth-1,
    my_prove([ -A | Unboxed], Depth2).

%% Subset
my_prove(Set, Depth) :-
    my_subset(A, Set),
    Depth2 is Depth-1,
    my_prove(A, Depth2).

unbox(box(X), X).