Chapter 16Chapter 16 TopicsIntroductionPropositionSymbolic LogicObject RepresentationCompound TermsParts of a Compound TermForms of a PropositionLogical OperatorsQuantifiersClausal FormPredicate Calculus and Proving TheoremsResolutionProof by ContradictionTheorem ProvingOverview of Logic ProgrammingExample: Sorting a ListThe Origins of PrologTermsTerms: Variables and StructuresFact StatementsRule StatementsExample RulesGoal StatementsInferencing Process of PrologApproachesSubgoal StrategiesBacktrackingSimple ArithmeticExampleTraceSlide 33List StructuresAppend ExampleMore ExamplesDeficiencies of PrologApplications of Logic ProgrammingSummaryChapter 16Logic Programming LanguagesCopyright © 2012 Addison-Wesley. All rights reserved. 1-2Chapter 16 Topics•Introduction•A Brief Introduction to Predicate Calculus•Predicate Calculus and Proving Theorems•An Overview of Logic Programming•The Origins of Prolog•The Basic Elements of Prolog•Deficiencies of Prolog•Applications of Logic ProgrammingCopyright © 2012 Addison-Wesley. All rights reserved. 1-3Introduction•Programs in logic languages are expressed in a form of symbolic logic•Use a logical inferencing process to produce results•Declarative rather that procedural:–Only specification of results are stated (not detailed procedures for producing them)Copyright © 2012 Addison-Wesley. All rights reserved. 1-4Proposition•A logical statement that may or may not be true–Consists of objects and relationships of objects to each otherCopyright © 2012 Addison-Wesley. All rights reserved. 1-5Symbolic Logic•Logic which can be used for the basic needs of formal logic:–Express propositions–Express relationships between propositions–Describe how new propositions can be inferred from other propositions•Particular form of symbolic logic used for logic programming called predicate calculusCopyright © 2012 Addison-Wesley. All rights reserved. 1-6Object Representation•Objects in propositions are represented by simple terms: either constants or variables•Constant: a symbol that represents an object•Variable: a symbol that can represent different objects at different times–Different from variables in imperative languagesCopyright © 2012 Addison-Wesley. All rights reserved. 1-7Compound Terms•Atomic propositions consist of compound terms•Compound term: one element of a mathematical relation, written like a mathematical function–Mathematical function is a mapping–Can be written as a tableCopyright © 2012 Addison-Wesley. All rights reserved. 1-8Parts of a Compound Term•Compound term composed of two parts–Functor: function symbol that names the relationship–Ordered list of parameters (tuple)•Examples:student(jon)like(seth, OSX)like(nick, windows)like(jim, linux)Copyright © 2012 Addison-Wesley. All rights reserved. 1-9Forms of a Proposition•Propositions can be stated in two forms:–Fact: proposition is assumed to be true–Query: truth of proposition is to be determined•Compound proposition:–Have two or more atomic propositions–Propositions are connected by operatorsCopyright © 2012 Addison-Wesley. All rights reserved. 1-10Logical OperatorsName Symbol Example Meaningnegation a not aconjunctiona  b a and bdisjunctiona  b a or bequivalencea  b a is equivalent to bimplicationa  ba  ba implies bb implies aCopyright © 2012 Addison-Wesley. All rights reserved. 1-11QuantifiersName Example Meaninguniversal X.P For all X, P is trueexistential X.P There exists a value of X such that P is trueCopyright © 2012 Addison-Wesley. All rights reserved. 1-12Clausal Form•Too many ways to state the same thing•Use a standard form for propositions•Clausal form:–B1  B2  …  Bn  A1  A2  …  Am–means if all the As are true, then at least one B is true•Antecedent: right side•Consequent: left sideCopyright © 2012 Addison-Wesley. All rights reserved. 1-13Predicate Calculus and Proving Theorems•A use of propositions is to discover new theorems that can be inferred from known axioms and theorems•Resolution: an inference principle that allows inferred propositions to be computed from given propositionsCopyright © 2012 Addison-Wesley. All rights reserved. 1-14Resolution•Unification: finding values for variables in propositions that allows matching process to succeed•Instantiation: assigning temporary values to variables to allow unification to succeed•After instantiating a variable with a value, if matching fails, may need to backtrack and instantiate with a different valueCopyright © 2012 Addison-Wesley. All rights reserved. 1-15Proof by Contradiction•Hypotheses: a set of pertinent propositions•Goal: negation of theorem stated as a proposition•Theorem is proved by finding an inconsistencyCopyright © 2012 Addison-Wesley. All rights reserved. 1-16Theorem Proving•Basis for logic programming•When propositions used for resolution, only restricted form can be used•Horn clause - can have only two forms–Headed: single atomic proposition on left side–Headless: empty left side (used to state facts)•Most propositions can be stated as Horn clausesCopyright © 2012 Addison-Wesley. All rights reserved. 1-17Overview of Logic Programming•Declarative semantics–There is a simple way to determine the meaning of each statement–Simpler than the semantics of imperative languages•Programming is nonprocedural–Programs do not state now a result is to be computed, but rather the form of the resultCopyright © 2012 Addison-Wesley. All rights reserved. 1-18Example: Sorting a List•Describe the characteristics of a sorted list, not the process of rearranging a listsort(old_list, new_list)  permute (old_list, new_list)  sorted (new_list)sorted (list)  j such that 1 j < n, list(j)  list (j+1)Copyright © 2012 Addison-Wesley. All rights reserved. 1-19The Origins of Prolog•University of Aix-Marseille (Calmerauer & Roussel)–Natural language processing•University of Edinburgh (Kowalski)–Automated theorem provingCopyright © 2012 Addison-Wesley. All rights reserved. 1-20Terms•This book uses the Edinburgh syntax of Prolog•Term: a constant, variable, or structure•Constant: an atom or an integer•Atom: symbolic value of Prolog•Atom consists of either:–a string of letters, digits, and underscores beginning with a lowercase letter–a string of printable ASCII characters delimited by