Since its pure LISP description in [MAE+62], Wang's proof
algorithm for the propositional calculus has often
been reformulated to demonstrate the use of declarative languages.
The algorithm applies reduction rules to a
sequent representation of propositional formulas until an atomic formula occurs in both
the antecedent and consequent of all derived sequents, reporting
`true`, or no more rule is applicable to a sequent, reporting
`false`.
[PS91] gives a version with an extra relation argument
for constructing a proof tree ``on-the-fly'',
whose size can be computed by an invertible function.

Here we give a RELFUN version that returns the trees of successful proofs, where subtrees are built and their roots labeled ``on-the-fly'' by
a constructor and two self-passivating functions:
the constructor indicates that an atomic formula occurs on
`both` sequent sides and the self-passivating functions exhibit
the reduction of a formula on the `right` (consequent) or on
the `left` (antecedent) side.

For example,
`wang([],[impl[and[p,and[q,r]],and[and[p,q],r]]])`
returns the `and`-associativity proof tree

right[ impl[and[p,and[q,r]],and[and[p,q],r]], right[ and[and[p,q],r], right[ and[p,q], left[ and[p,and[q,r]], left[and[q,r],both[p,wang[[r,q,p],[p]]]] ], left[ and[p,and[q,r]], left[and[q,r],both[q,wang[[r,q,p],[q]]]] ] ], left[and[p,and[q,r]],left[and[q,r],both[r,wang[[r,q,p],[r]]]]] ] ]

The main `wang` function's first clause initializes with `[]`
two auxiliary (atomic formula) arguments
of a `work`horse function that either returns a proof tree,
or yields `unknown`. In the former case, `wang` commits
to the tree value by employing a `sole' cut
(```! .`'' or ```!.`'', instead of only ```.`'', as the footed-clause terminator). In the latter case the
second `wang` clause returns `false`, thus implementing a
procedure-specific closed-world assumption for
the `wang` operator. The `work` function realizes the
usual reduction rules deterministically,
employing `ankle' cuts (```! &`'' or ```!&`'' instead of just
a ```&`'' separator) for committing to each
rule before its foot is reached. In most `work` clauses
no body premises are needed between the conclusion and the foot,
hence
their ankle cut coincides with a `neck' cut (```:- !`'' is joined
to ```!-`'', ```:- !&`'' to ```!-&`'').

The alternativewang(L,R) :-& work(L,R,[],[])!. (or wang(L,R) :-& if W is work(L,R,[],[]) wang(L,R) :-& false. then W else false.) work([],[],A,B) :- member(X,A), member(X,B) !& both[X,wang[A,B]]. work([X|L],R,A,B) :- atomic(X) !& work(L,R,[X|A],B). work(L,[X|R],A,B) :- atomic(X) !& work(L,R,A,[X|B]). work(L,[not[P]|R],A,B) !-& right(not[P],work([P|L],R,A,B)). work([not[P]|L],R,A,B) !-& left(not[P],work(L,[P|R],A,B)). work(L,[and[P,Q]|R],A,B) !-& right(and[P,Q],work(L,[P|R],A,B),work(L,[Q|R],A,B)). work([and[P,Q]|L],R,A,B) !-& left(and[P,Q],work([P,Q|L],R,A,B)). work(L,[or[P,Q]|R],A,B) !-& right(or[P,Q],work(L,[P,Q|R],A,B)). work([or[P,Q]|L],R,A,B) !-& left(or[P,Q],work([P|L],R,A,B),work([Q|L],R,A,B)). work(L,[impl[P,Q]|R],A,B) !-& right(impl[P,Q],work([P|L],[Q|R],A,B)). work([impl[P,Q]|L],R,A,B) !-& left(impl[P,Q],work([Q|L],R,A,B),work(L,[P|R],A,B)). work(L,[equiv[P,Q]|R],A,B) !-& right(equiv[P,Q],work([P|L],[Q|R],A,B),work([Q|L],[P|R],A,B)). work([equiv[P,Q]|L],R,A,B) !-& left(equiv[P,Q],work([P,Q|L],R,A,B),work(L,[P,Q|R],A,B)). left(|R) :-& left[|R]. right(|R) :-& right[|R]. member(X,[X|R]). (or member(X,[X|R]) :-& [X|R].) member(X,[Y|R]) :- member(X,R). (or member(X,[Y|R]) :-& member(X,R).) atomic(F[|R]) !- unknown. atomic(X).