Each production, a rule

The grammar uses ->, |, &, ~ and parentheses. Each BNF production becomes a rule:

impl ::= disj
       | disj "->" impl
disj ::= conj
       | disj "|" conj
conj ::= lit
       | conj "&" lit
lit  ::= atom
       | "~" lit
atom ::= var
       | "(" impl ")"

impl(F, T) :- disj(F, T).
impl(F, T) :- disj(F, M), char(M, "-"), char(M + 1, ">"), impl(M + 2, T).
disj(F, T) :- conj(F, T).
disj(F, T) :- disj(F, M), char(M, "|"), conj(M + 1, T).
conj(F, T) :- lit(F, T).
conj(F, T) :- conj(F, M), char(M, "&"), lit(M + 1, T).
lit(F, T)  :- atom(F, T).
lit(F, T)  :- char(F, "~"), lit(F + 1, T).
atom(F, T) :- char(F, C), prop_var(C), T = F + 1.
atom(F, T) :- char(F, "("), impl(F + 1, M), char(M, ")"), T = M + 1.

disj and conj recurse on the left: p | q | r is effectively (p | q) | r (left associative).

impl recurses on the right: p -> q -> r is effectively p -> (q -> r) (right associative).