; -> is prolog's neck (we could reverse this to make N3 or any other form of logic

is_proved(Term, (Term : How)) <- is_given(Term,How).
is_proved(Term, (Term : How)) <- pv(Term,How).

pv(B,P1 ^ P2) <- is_proved(A,P1), is_proved(A=>B,P2).
pv(A,P1) <- is_proved(A & B,P1).
pv(B,P1) <- is_proved(A & B,P1).
pv(A & B,P1 ^ P2) <- is_proved(A,P1), is_proved(B,P2).
pv(C,P1 ^ P2 ^ P3) <- is_proved(A v B,P1), is_proved(A=>C,P2), is_proved(B=>C,P3).
pv(A v B,P1) <- is_proved(A,P1).
pv(A v B,P1) <- is_proved(B,P1).

; Database
is_given(a,1).
is_given(c,2).
is_given(a=>b,3).

; Query

?- is_proved(b,R).
R = b:(3:a=>b ^ a:1)