One of the exercises consisted of performing some abductive reasoning, about boolean circuits where some logical gates could be broken (there were ~5 gates in the circuit). And it was tedious... And I was always making an error somewhere... So I decided: “enough is enough,” and wrote a Prolog program to solve this task for me.
And it was a great success: it took me only a day to write a program that solves a task it would take two hours to solve it (provided you were extremely pedantic).
(However, I've included my program into the assignment and I suspect it may have boosted the mark I received.) ;-)
:- op(1200, xfx, ====>).
% Give all the possible explanations for Goal in KB, as conjunctive clauses
explanations(Goal, KB, Explanations) :-
prime_implicates(KB, Implications),
no_goal(Goal, Implications, NoGs),
findall(Explanation, (member(X, NoGs), negate_all(X, Explanation)), Explanations).
% find all the prime implicates from KB
prime_implicates(KB, Implicates) :-
resolution(KB, Cons),
findall(Imp, (member(Imp, Cons), prime_implicate_(Imp, Cons)), Implicates).
prime_implicate_(_, []).
prime_implicate_(I, [H|Set]) :-
( \+subset(H,I)
; I ==H),
prime_implicate_(I, Set).
% resolution(KB, AllResolvents).
resolution(List, Solution) :-
% we have to sort the clauses in order to obtain the
% “canonical” form (useful to remove duplicates).
findall(Sorted, (member(L,List), sort(L,Sorted)), SortedList),
resolution2(SortedList, Solution).
resolution2(List,Solution) :-
member(A, List),
member(B, List),
A \==B,
print(A),
resolve(A, B, R1),
sort(R1, R),
\+ smember(R, List),
pretty(A,B,R),
resolution2([R|List], Solution)
;
List=Solution.
resolve(XX,YY,Z) :-
new_var(XX,X),
new_var(YY,Y),
member(Rx,X),
member(Ry, Y),
% ( Rx=not(Ry)
% ; Ry=not(Rx)),
% We must use sound unification (no cyclic terms)
( unify_with_occurs_check(Rx, not(Ry))
; unify_with_occurs_check(Ry, not(Rx))),
select(Ry,Y, NewY),
select(Rx, X, NewX),
sunion(NewX, NewY, Z).
% prover by resolution for Horn Clauses
% hresolution(+Goal, +KB, -ResolutionTrail)
% prove Goal in KB
hresolution(Goal, KB, Sol) :-
negate(Goal, NG),
hresolution_(NG, KB, Sol).
hresolution_(_,[],[]).
hresolution_(X, KB, [X/Y====>Resolvent|Rest]) :-
member(Y,KB),
resolve(X,Y, Resolvent),
( Resolvent = [],
Rest=[]
;
select(Y,KB, NewKB),
hresolution_(Resolvent, NewKB, Rest)).
/* *************************
* *
* Tool predicates: *
* *
***************************/
% put brand new new variables in the clause
new_var(X,Y) :-
assert(p(X)),
retract(p(Y)).
pretty(A,B,C) :- print(A/B====>C), nl, nl.
% like select, but uses sound unification and succeeds if El is not in
% the List
minus(_, [], []).
minus(X, [X1|Tail], Tail) :-
sunifiable(X, X1).
minus(Elem, [Head|Tail], [Head|Rest]) :-
minus(Elem, Tail, Rest).
% sound-unifiable
sunifiable(X,Y) :-
\+ \+ unify_with_occurs_check(X,Y).
% like member, but tests identity instead of unification (we don't
% want to instantiate X in f(X) to 1 by checking if f(r) is already in
% the KB)
smember(X,[H|_]) :-
%X==H.
sunifiable(X, H).
smember(X, [_|Rest]) :-
smember(X, Rest).
sunion([], L, L1) :-
unify_with_occurs_check(L, L1),
!.
sunion([H|T], L, R) :-
smember(H, L), !,
sunion(T, L, R).
sunion([H|T], L, [H|R]) :-
sunion(T, L, R).
negate(not(X), X) :- !.
negate(X,not(X)).
% negate all literals in an disjunctive clause, giving a conjunctive clause
negate_all([],[]).
negate_all([H|T],[NH|NT]) :-
negate(H, NH),
negate_all(T, NT).
% eliminate the goal Goal form the clause
no_goal(_, [], []).
no_goal(Goal, [H|T], [NH|NT]) :-
minus(Goal, H, NH),
no_goal(Goal, T, NT).
test(Z):-
List = [
[not(tennis_elbow), sore_elbow],
[not(tennis_elbow), tennis_player],
[not(arthritis), treated, sore_joints],
[sore_elbow, not(sore_joints)],
[not(sore_joints), sore_hips]
],
List2 = [
[not(p), not(q), not(r), g],
[p, not(q), g],
[q, not(r), g]
],
explanations(g, List2,Z).
test_nonprovable(A) :-
List = [[p(X)], [p(X)]],
resolution(List, A).
test_plus(Solution, Result) :-
A=[
[rplus(W,0,W)],
[rplus(X, s(Y), s(Z)), not(rplus(X,Y,Z))]
],
Goal = [rplus(s(s(s(0))), s(s(0)), Result)],%s(s(s(s(s(0))))))],
hresolution(Goal, A, Solution).
