Logic Programming
             FrankPfenning
             CarnegieMellonUniversity
                     Draft of January 2, 2007
             Notes for a course given at Carnegie Mellon University, Fall 2006. Mate-
             rials available at http://www.cs.cmu.edu/~fp/courses/lp. Please send
             commentstofp@cs.cmu.edu.
                  c
             Copyright
FrankPfenning2006–2007
              LECTURE NOTES               JANUARY2, 2007
                                                   15-819K: Logic Programming
                                                              Lecture 1
                                                   Logic Programming
                                                           FrankPfenning
                                                          August29,2006
                             In this first lecture we give a brief introduction to logic programming. We
                             also discuss administrative details of the course, although these are not
                             included here, but can be found on the course web page.1
                             1.1   Computationvs.Deduction
                             Logic programming is a particular way to approach programming. Other
                             paradigms we might compare it to are imperative programming or func-
                             tional programming. The divisions are not always clear-cut—a functional
                             language may have imperative aspects, for example—but the mindset of
                             various paradigms is quite different and determines how we design and
                             reason about programs.
                                To understand logic programming, we first examine the difference be-
                             tween computation and deduction. To compute we start from a given ex-
                             pression and, according to a fixed set of rules (the program) generatee a
                             result. For example, 15 + 26 → (1 + 2 + 1)1 → (3 + 1)1 → 41. To deduce
                             westartfromaconjectureand,accordingtoafixedsetofrules(theaxioms
                             andinferencerules), tryto constructa proofofthe conjecture. So computa-
                             tion is mechanical and requires no ingenuity, while deduction is a creative
                                                     n     n    n
                             process. For example, a +b 6= c for n > 2, ::: 357 years of hard work :::,
                             QED.
                                Philosophers, mathematicians, and computer scientists have tried to
                             unify the two, or at least to understand the relationship between them for
                             centuries. Forexample,GeorgeBoole2succeededinreducingacertainclass
                               1http://www.cs.cmu.edu/~fp/courses/lp/
                               21815–1864
                             LECTURE NOTES                                               AUGUST29,2006
                      L1.2                                        LogicProgramming
                      oflogical reasoningtocomputationinso-calledBooleanalgebras. Sincethe
                      fundamental undecidability results of the 20th centuries we know that not
                      everythingwecanreasonaboutisinfactmechanicallycomputable,evenif
                      wefollowawell-definedsetofformalrules.
                         In this course we are interested in a connection of a different kind. A
                      first observation is that computation can be seen as a limited form of de-
                      duction because it establishes theorems. For example, 15 + 26 = 41 is both
                      the result of a computation, and a theorem of arithmetic. Conversely, de-
                      duction can be considered a form of computation if we fix a strategy for
                      proof search, removing the guesswork (and the possibility of employing
                      ingenuity)from thedeductive process.
                         Thislatter idea is the foundation of logic programming. Logic program
                      computation proceeds by proof search according to a fixed strategy. By
                      knowingwhatthis strategy is, we can implement particular algorithms in
                      logic, and execute the algorithms by proof search.
                      1.2  JudgmentsandProofs
                      Since logic programming computation is proof search, to study logic pro-
                      grammingmeanstostudyproofs. WeadoptheretheapproachbyMartin-
                      Lo¨f [3]. Although he studied logic as a basis for functional programming
                      rather than logic programming, his ideas are more fundamental and there-
                      fore equally applicable in both paradigms.
                         Themostbasicnotionisthatofajudgment,whichisanobjectofknowl-
                      edge. We know a judgment because we have evidence for it. The kind of
                      evidence we are most interested in is a proof, which we display as a deduc-
                      tion using inference rules in the form
                                                J :::J
                                                 1    n
                                                        R
                                                   J
                      where R is the name of the rule (often omitted), J is the judgment estab-
                      lished by the inference (the conclusion), and J ;:::;J are the premisses of
                                                            1     n
                      the rule. We can read it as
                           If J and ··· and J then we can conclude J by virtue of rule R.
                              1          n
                         ByfarthemostcommonjudgmentisthetruthofapropositionA,which
                      wewrite as A true. Because we will be occupied almost exclusively with
                      the thruth of propositions for quite some time in this course we generally
                      omit the trailing “true”. Other examples of judgments on propositions are
                      LECTURE NOTES                                  AUGUST29,2006