Logic Programming Part 2

Return to List of Lectures

Previous Lecture

Questions?


Horn Clauses, Resolution, and Proof

    Horn Clause:

        A   if  B1 and B2 and ... and Bn


    Resolution: Consider 2 Horn clauses

        A   if  B1 and ... and Bn
        C   if  D1 and ... and A and ... Dm

        Clearly, these can be combined into

        C   if  D1 and ...
                    and (B1 and ... and Bn)
                    and ... Dm

        This is resolution.


    More interestingly, view Horn clauses through
    the logical equivalence
        A if B  ==      (not B) or A
    so
            A if B1 and B2 and ... and Bn
        =   A or not(B1 and B2 and ... and Bn)
        =   A or (not B1) or (not B2) or ... or (not Bn)
    i.e., a Horn clause is an "or" of terms, all but one
        of which are negations.

    This view demonstrates how a "fact" can be
    stated as a trivial sort of Horn clause (one with
    no negated terms):

        A

    (Note that Sebesta has this point wrong - a fact
    is not a headless Horn clause, it is a Horn clause
    that consists only of a head.)


    Multiple Horn clauses in a "program" are
    connected by "and's" (i.e., all are assumed to
    be true implications)

    Program =
            (A or not B1 or not B2 .... or not Bn)
    and (C or not D1 or ... or not Dm)
    and ....

    Resolution can now be seen as a way of simplifying
    such a system, with an eye to deciding whether it
    is satisfiable (i.e., whether all the clauses really
    can be true at once):

    A or (not B1) or ... or (not Bn)    and
    C or (not D1) or ... or (not A) or ... or (not Dm)

        becomes

    C or (not D1) or ...
        or (not B1) or ... or (not Bn)
        or ... or (not Dm)

    (Logically, since the "A" in one clause and the
    "not A" in the other can't both be true, but one
    must be, the overall conjunction is satisfiable if
    and only if at least one of the other terms is
    satisfiable)

    Note that this reduces the total number of clauses
    in the system by 1.

    This is the heart of resolution as a
    theorem-proving technique:

        If a series of resolutions simplifies a system
        of Horn clauses to nothing, it means that the
        system is inconsistent (i.e., to satisfy it,
        at least one term in an empty clause must be
        true).

        So to "prove" a statement, phrase it's negation
        as a Horn clause, add it to a Horn clause system
        of "axioms", and run resolution until either it
        can no longer simplify the system (the
        theorem isn't provable), or it produces an
        empty clause (the theorem is true).

        Typically the theorem to be proven is a single
        proposition, e.g., A, its negation is thus
        (not A), i.e., a headless Horn clause.

    This is basically both the semantics and execution
    model for pure Prolog programming.
    
    
Logic programming in reality - Prolog

    Sec.s 15.5 and 15.6.1 - 15.6.5
    
    Look at Prolog and simple uses of logic programming via a set of
    facts and rules about the history of programming languages. For
    example:
    
        invented( john_backus, fortran ).
        % John Backus invented FORTRAN.

        invented( john_backus, bnf ).
        invented( peter_naur, bnf ).
        % John Backus and Peter Naur co-invented BNF
    
    Now one can look up these facts via Prolog workspace with queries such as
        invented(Who,fortran).
        % Who invented FORTRAN?
    
        invented(Who,bnf).
        % Who invented BNF - has multiple solutions
    
    How about rules? As a context, consider describing how languages have
    influenced each other:

        based_on( pl1, fortran ).
        based_on( bcpl, pl1 ).
        based_on( c, bcpl ).
        % PL/1 was based on FORTRAN, BCPL was based on PL/1, etc.
        
    Mini-Assignment: These relations imply things like FORTRAN influenced BCPL,
    FORTRAN influenced C, etc. Come up with more-or-less Prolog rule for inferring
    this "one-language-influenced-another" relationship.

Next Lecture