Foundations of Logic Programming Copyright 1999 Paul F Reynolds Jr Deductive Logic e g of use Gypsy specifications and proofs About deductive logic G del 1931 Interesting systems with a finite number of axioms are necessarily either incomplete there are statements that can t be proven or inconsistent S such that S and S can be proven true Interesting systems include Presberger Arithmetic 0 1 and Peano Arithmetic 0 1 Recall all inconsistent systems are complete Copyright 1999 Paul F Reynolds Jr First Order Predicate Logic Logic programming is based on FOPL FOPL is complete J A Robinson resolution theorem proving All clauses logically implied by an initial formula may be derived from the initial formula by the proof method BUT FOPL is undecidable An attempt to prove a formula may go on forever but there will be no indication when to stop without sacrificing formulae that can be proven completeness of FOPL is of theoretical interest but of limited practicality completeness is predicated on there being a search strategy that knows when to stop a particular unproductive line of deduction Higher order predicate logics and calculi ones which allow predicates of predicates are not complete Copyright 1999 Paul F Reynolds Jr Foundations of Logic Programming Logic programming is based on Horn Clauses In the propositional calculus all formulae can be put in conjunctive normal form disjuncts connected by Each disjunct can be expressed as A1 A1 A1 A2 A2 A2 Am Am Am B1 B2 B1 B2 B1 B2 Bn Bn Bn interpretations m 1 m 1 m 1 n 0 m 1 n 0 m 0 n 0 m 0 n 0 Conclusions are indefinite one or more are true Horn clauses A B1 B2 Bn definite clause 1 conclusion A unconditional definite clause fact negation of B1 B2 Bn the empty clause contradiction In logic all clauses can be represented as Horn Clauses Copyright 1999 Paul F Reynolds Jr Proof by Refutation An important proof method set of axioms P clause to be proven Q show P Q is false by deriving a contradiction i e assert Q and try to derive empty clause which represents false In this context Q is called a goal Propositional Horn Clause Resolution PHC Resolution In doing a refutation proof the following general PHC resolution step can be performed A1 B1 B2 Bn A1 A2 Am B1 B2 Keep applying this until Bn A2 Am is achieved Copyright 1999 Paul F Reynolds Jr More PHC Resolution e g to prove A2 1 2 3 4 A1 A2 A3 A1 A3 A2 negated goal proof leading to contradiction 5 6 7 A1 A3 A3 apply 2 4 apply 1 5 apply 3 6 Note Prolog and other logic based languages are based on this resolution proof strategy Copyright 1999 Paul F Reynolds Jr First Order Predicate Logic Predicates can have arguments constants variables other functional terms e g 1 2 3 4 5 6 a X m X e c a X s b m X e X s X a X When we start dealing with variables we need Axiom of General Specification A clause with logical variables is true for every set of values of the variables Supports generalizing PHC resolution into Horn Clause Resolution HCR by systematically instantiating variables Unification Copyright 1999 Paul F Reynolds Jr FOPL cont e g 1 p t 2 q X 3 4 q t 5 6 p X q t p t X t p t from 2 3 and substitution from 3 4 from 1 and 5 resolution is combination of unification and elimination in one operation Copyright 1999 Paul F Reynolds Jr More Proofs Using 1 2 3 4 5 6 with goal a X m X e c a X s b m X e X s X a X a X step 6 we can derive 7 8 9 10 11 Copyright 1999 applying 1 6 e X applying 2 7 X c applying 3 8 also s X applying 4 6 X b applying 5 10 m X Paul F Reynolds Jr Alternative Proof Strategies Top Down what we ve just seen collecting variable bindings Start with goal and reduce into subgoals until there is only the empty subgoal Bottom up Combining facts with rules or rules with other rules Copyright 1999 Paul F Reynolds Jr Bottom Up Using 1 2 3 4 5 6 Combine rule 2 with fact 3 yielding combined with rule 1 yields or Combine rule 1 with rule 2 yields a X m X e c a X s b m X e X s X a X m X e c m c a X a c a X m X a X e X combining rule with a fact yields m X a new fact m X e X e X combining rules to make a new rule allows us to make discoveries from known facts and rules Copyright 1999 Paul F Reynolds Jr Closed World Assumption Inabilty to demonstrate that something is true means that it is false assumes user made no typos and specified all things that need to be specified to properly identify true queries as true leads to joining unknown and not provably true into one class failing to prove something true leads to conclusion that it is false CWA says that all things that are true have been specified as such or can be derived Copyright 1999 Paul F Reynolds Jr Closed World Assumption 2 Possible alternatives 1 leave system alone accept CWA 2 allow negation in clauses but not in conclusion of Horn Clauses 3 allow statement of negative conclusions search positive search negative report unknown 4 work in constrained environment where everything is known 5 work in statistical environment where answers are expressed in terms of likelihoods Copyright 1999 Paul F Reynolds Jr About Prolog Prolog lends itself nicely to concurrency form p0 p1 p2 p3 p4 can be executed concurrently with communications about bindings AND parallelism or HG HG HG Copyright 1999 OR parallelism Paul F Reynolds Jr About Prolog 2 Prolog and principles Orthogonal separates logic and control assert retract and cut violate this regular regular rules security meaning of a program is determined by what a user writes simplicity simple rules violates localized cost execution cost is determined by rule order defense in depth misspellings alter meaning of program Copyright 1999 Paul F Reynolds Jr