Copyright 1999Paul F. Reynolds, Jr.Foundations of LogicProgrammingCopyright 1999Paul 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 ofaxioms) are necessarily either:•incomplete (there are statements that can't be proven)•or inconsistent (S such that S and ¬S can be proventrue)•Interesting systems include Presberger Arithmetic(0,1,*,+) and Peano Arithmetic (0,1,+)•Recall: all inconsistent systems are completeCopyright 1999Paul 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 fromthe initial formula by the proof method."BUT•FOPL is undecidable–An attempt to prove a formula may go on forever, but there will be noindication when to stop without sacrificing formulae that can be proven.  completeness of FOPL is of theoretical interest, but of limitedpracticality. (completeness is predicated on there being a search strategythat knows when to stop a particular unproductive line of deduction.)•Higher order predicate logics (and calculi) - ones which allowpredicates of predicates - are not complete.Copyright 1999Paul F. Reynolds, Jr.Foundations of Logic Programming•Logic programming is based on Horn Clauses–In the propositional calculus all formulae can be put in conjunctivenormal form (disjuncts connected by  )–Each disjunct can be expressed as:A1 A2 ... Am ¬B1 ¬B2 ... ¬Bn  A1  A2  ...  Am  ¬ (B1  B2  ...  Bn)  A1  A2  ...  Am  (B1  B2  ...  Bn)•interpretations: m > 1Conclusions are indefinite, one or more are true. m = 1Horn clauses. m = 1, n > 0(A  B1  B2  ...  Bn ) -- definite clause, 1 conclusion m = 1, n = 0(A  ) unconditional definite clause (fact) m = 0, n > 0negation of (B1  B2  ...  Bn) m = 0, n = 0 the empty clause (contradiction)•In logic, all clauses can be represented as Horn Clauses...Copyright 1999Paul F. Reynolds, Jr.Proof by Refutation•An important proof method: P: set of axioms Q:clause to be proven–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 canbe performed: A1  (B1  B2  ...  Bn)  A1  A2  ...  Am ________________________________  (B1  B2  ...  Bn)  A2  ...  Am  Keep applying this until  is achieved.Copyright 1999Paul F. Reynolds, Jr.More PHC Resolution•e.g.to prove A2(1)A1 (2)A2  A1, A3(3)A3 (4) A2 -- negated goal•proof leading to contradiction:(5) A1, A3-- apply 2 & 4(6) A3 -- apply 1 & 5(7)-- apply 3 & 6•Note: Prolog and other logic-based languages are based on thisresolution proof strategy.Copyright 1999Paul F. Reynolds, Jr.First Order Predicate Logic•Predicates can have arguments: constants, variables, otherfunctional terms.e.g.(1) a(X)  m(X)(2) m(X)  e(X)(3) e(c) (4) a(X)  s(X)(5) s(b) (6)  a(X)•When we start dealing with variables, we need:Axiom of General Specification: A clause with logical variablesis true for every set of values of the variables.–Supports generalizing PHC resolution into Horn Clause Resolution (HCR)•by systematically instantiating variables.  "Unification”Copyright 1999Paul F. Reynolds, Jr.FOPL (cont)•e.g.1) p(t)2) q(X)  p(X)3)  q(t)4) q(t)  p(t) (X = t) -- from (2), (3) and substitution5)  p(t) -- from (3) & (4)6)  -- from (1) and (5) resolution is combination of unification andelimination in one operation.Copyright 1999Paul F. Reynolds, Jr.More Proofs•Using:(1) a(X)  m(X)(2) m(X)  e(X)(3) e(c) (4) a(X)  s(X)(5) s(b) (6)  a(X)•with goal  a(X) (step (6)), we can derive:(7)  m(X)-- applying (1) & (6)(8)  e(X)-- applying (2) & (7)(9)  X = c-- applying (3) & (8) also:(10)  s(X)-- applying (4) & (6)(11)  X = b-- applying (5) & (10)Copyright 1999Paul F. Reynolds, Jr.Alternative Proof Strategies•Top Down: what we've just seen - collecting variablebindings.– Start with goal and reduce into subgoals until there isonly the empty subgoal.•Bottom up: Combining facts with rules or rules with otherrules.Copyright 1999Paul F. Reynolds, Jr.Bottom Up•Using: (1) a(X)  m(X)(2) m(X)  e(X)(3) e(c) (4) a(X)  s(X)(5) s(b) (6)  a(X)•Combine rule (2) m(X)  e(X) -- combining with fact (3) e(c) -- rule with yielding: m(c)  -- a fact yields combined with rule (1)a(X)  m(X) -- a new yields:a(c) -- fact•or Combine rule (1)a(X)  m(X)-- combining rules with rule (2) m(X)  e(X)-- to make a new yields:a(X)  e(X)-- rule• -- allows us to make discoveries from known facts and rules.Copyright 1999Paul F. Reynolds, Jr.Closed World Assumption•Inabilty to demonstrate that something is true means that itis false.–assumes user made no typos and specified all things that need to bespecified 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 specifiedas such or can be derived.Copyright 1999Paul 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; searchnegative; report unknown; (4) work in constrained environment where everything is known (5) work in statistical environment where answers are expressed interms of likelihoods.Copyright 1999Paul F. Reynolds, Jr.About Prolog•Prolog lends itself nicely to concurrency form: p0 :- p1, p2, p3, p4 ^---^---^---^---- can be executedconcurrently(with communications about bindings) -- "AND parallelism" or: HG :- ................{ HG :-