Next: eval: Interpreting a Up: The Logic/Functional Style Previous: serialise: Inplace Updates

wang: On-the-Fly Construction of Proof Trees

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 workhorse 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 ``!-&'').


wang(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).
The alternative member definition (using both parenthesized clauses) is the LISP-like version mentioned in the introduction. (Using the first parenthesized clause and the second unparenthesized clause gives a definition returning [X|R] instead of true only for an X occurring as the first element of the original list.) Our functional wang algorithm could again be degenerated to a non-tree-building relational algorithm by just omitting all ``&''-separators; the resulting hornish clauses could then be simplified, mainly by bringing the work recursions to the top-level.



Next: eval: Interpreting a Up: The Logic/Functional Style Previous: serialise: Inplace Updates


Harold Boley & Michael Sintek (sintek@dfki.uni-kl.de)