IntroductionComputational LogicMathematicsSoftware EngineeringConstraint Satisfaction SystemsLogical SpreadsheetsDeductive Database SystemsData IntegrationWeb Service IntegrationRegulations and Business RulesMichigan Lease Termination ClauseLogical VersionPowerPoint PresentationFormal MathematicsAlgebra ProblemAlgebra SolutionLogic ProblemFormalizationRule of InferenceExamplesLogic Problem RevisitedLogic Problem ConcludedAutomated ReasoningLogic TechnologySlide 25Multiple LogicsCommon TopicsMetaMike took it twice!http://cs157.stanford.eduIntroductionComputational Logic Lecture 1Michael Genesereth Autumn 20072Computational Logicabove(yellow,blue)on(red,yellow)x.y.(on(x,y) above(x,y))y.on(blue,y)on(yellow,blue)on(green,yellow) on(green,blue)3MathematicsGroup AxiomsTheoremTasks:Proof CheckingProof Generation(x×y)×z =x×(y×z)x×e=xe ×x =xx×x−1=ex−1×x =e4Software EngineeringProgramSpecification:Tasks:Partial EvaluationProgram VerificationProof of TerminationComplexity Analysissorter Lsort(L)∀i.∀j.(i <j ⇒ sort(L)i<sort(L)j)5Constraint Satisfaction Systems6Logical Spreadsheets7Deductive Database SystemsDatabase Tables Database Sentencesparentart bobart beabea coeConstraintsView Definitionsparent(art,bob)parent(art,bea)parent(bob,coe)parent(x,y)∧ parent(y,z)⇒ grandparent(x,z)¬parent(x,x)parent(x,y)⇒ ¬parent(y,x)8Data Integrationemployee(x,y) manager(y,x)name manager office phone John Jill MJH222 38086Jane Jerry Cedar12 57493Jill MJH222 Jerry 420-032 56777name employee location telephone John MJH222 7238086Jane Cedar12 7257493Jill John MJH222 Jerry Jane 420-032 72567779Web Service IntegrationResultFacilitatorRequestQBF (Query by Form) - User queries Internet in his own schemaABF (Application by Form) - User requests services using own schemaInsurer 1Insurer 2AppraiserTitle CompanyBank 1Bank 2Bank 310Regulations and Business Rules11Michigan Lease Termination ClauseThe University may terminate this lease when the Lessee, having made application and executed this lease in advance of enrollment, is not eligible to enroll or fails to enroll in the University or leaves the University at any time prior to the expiration of this lease, or for violation of any provisions of this lease, or for violation of any University regulation relative to resident Halls, or for health reasons, by providing the student with written notice of this termination 30 days prior to the effective data of termination; unless life, limb, or property would be jeopardized, the Lessee engages in the sales of purchase of controlled substances in violation of federal, state or local law, or the Lessee is no longer enrolled as a student, or the Lessee engages in the use or possession of firearms, explosives, inflammable liquids, fireworks, or other dangerous weapons within the building, or turns in a false alarm, in which cases a maximum of 24 hours notice would be sufficient.12Logical VersionA A1 A2 BA A4 B A A5 B A A6 B A A7 B B B1B B2B B3B B4B B513Elements14Formal MathematicsAlgebra1. Formal language for encoding information2. Legal transformations3. AutomationLogic1. Formal language for encoding information2. Legal transformations3. Automation15Algebra ProblemXavier is three times as old as Yolanda. Xavier's age and Yolanda's age add up to twelve. How old are Xavier and Yolanda?16Algebra SolutionXavier is three times as old as Yolanda. Xavier's age and Yolanda's age add up to twelve. How old are Xavier and Yolanda?Automation: Saint, Sin, Reduce, Macsyma, Mathematicax−3y=0x+y=12−4y =−12y=3x =917Logic ProblemIf Mary loves Pat, then Mary loves Quincy. If it is Monday, then Mary loves Pat or Quincy. If it is Monday, does Mary love Quincy?If it is Monday, does Mary love Pat?Mary loves only one person at a time. If it is Monday, does Mary love Pat?18FormalizationSimple Sentences: Mary loves Pat. Mary loves Quincy. It is Monday.Premises: If Mary loves pat, Mary loves Quincy. If it Monday, Mary loves Pat or Quincy. Mary loves one person at a time.Questions: Does Mary love Pat? Does Mary love Qunicy?p⇒ qm⇒ p∨qp∧q⇒⇒ p⇒ qpqm19Rule of InferencePropositional ResolutionNB: If pi is the same as sj, it is okay to drop the two symbols, with the proviso that only one such pair may be dropped.NB: If a constant is repeated on the left or the right, all but one of the occurrences can be deleted.p1∧...∧ pk⇒ q1∨...∨qlr1∧...∧rm⇒ s1∨...∨snp1∧...∧ pk∧r1∧...∧rm⇒ q1∨...∨ql∨s1∨...∨sn20Examplesp ⇒ q⇒ p⇒ qp ⇒ qq ⇒p ⇒p ⇒ qq ⇒ rp ⇒ r21Logic Problem Revisitedp ⇒ qm ⇒ p∨qm ⇒ q∨qm ⇒ qIf Mary loves Pat, then Mary loves Quincy. If it is Monday, then Mary loves Pat or Quincy. If it is Monday, does Mary love Quincy?22Logic Problem Concludedm ⇒ qp∧q ⇒m∧ p ⇒Mary loves only one person at a time. If it is Monday, does Mary love Pat?23Automated Reasoningproof <- kbgoal in proof?r <- choose(rules)p <- choose(proof)q <- choose(proof)c <- apply(r,p,q)proof <- proof|cSuccessgoalkbrules24Logic TechnologyLanguages Knowledge Interchange Format (KIF) - ANSI Common Logic - W3CSome Popular Automated Reasoning SystemsOtterPTTP / EpilogSnark / Vampire / …Knowledge Bases Definitions (Bachelor is an unmarried adult male.) Constraints (e.g. PV=nRT) Laws (e.g. 1040 necessary if earnings > $10,000.)25Study Guide26Multiple LogicsPropositional LogicIf it is raining, the ground is wet.Relational LogicIf x is a parent of y, then y is a child of x.27Common TopicsCommon TopicsSyntax - expressions in the languageSemantics - meaning of expressionsComputational MattersContrasts Expressiveness - operators, variables, terms, ... Computational Hierarchy - polynomial? decidable? Tradeoffs - expressiveness versus computability28MetaWe will frequently write sentences about sentences.Sentence: When it rains, it pours.Metasentence: That sentence contains two verbs.We will frequently prove things about proofs.Proofs: formalMetaproofs: informal29Mike took it
View Full Document
Unlocking...