1IntroductionComputational Logic Lecture 1Michael Genesereth Autumn 20082Computational 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)23MathematicsGroup Axioms!TheoremTasks: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)35Hardware EngineeringCircuit: Behavior:Applications:SimulationConfigurationDiagnosisTest Generationo ⇔ (x ∧ ¬y) ∨ (¬x ∧ y)a ⇔ z ∧ ob ⇔ x ∧ ys ⇔ (o ∧ ¬z) ∨ (¬o ∧ z)c ⇔ a ∨ bxyzscoab6Constraint Satisfaction Systems47 Database TablesQueriesquery(X,Z) :- parent(X,Y) & parent(Y,Z)Constraintsillegal :- parent(X,X)illegal :- parent(X,Y) & parent(Y,X)Deductive Database Systemsparentart bobart beabea coeparent(art, bob)parent(art, bea)parent(bob,coe)8Data IntegrationSide-by-sideComparisonInfomasterManufacturer 1Manufacturer 2General DataIntegratedSearchProduct analysisSatisfactionRatingsSupplier 1Supplier 2Supplier 3Supplier 459Data 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 725677710Logical Spreadsheets611Examples of Non-Functional ConstraintsScheduling–Start times must be before end times–Room 104 may not be scheduled after 5:00 pm–Only senior managers can reserve the third floorconference roomTravel Reservations–The number of lap infants in a group on a flightmust not exceed the number of adults.Academic Programs–Students must take at least 2 math courses12Regulations and Business RulesUsing the language of logic, it is possible to definenew relations.Office mates are people who share an office.officemate(X,Y) :- office(X,Z) ∧ office(Y,Z)This includes the property of legality / illegality.Managers and subordinates may not be office mates.illegal :- manages(X,Y) ∧ officemate(X,Y)713Michigan Lease Termination ClauseThe University may terminate this lease when the Lessee, havingmade application and executed this lease in advance ofenrollment, is not eligible to enroll or fails to enroll in theUniversity or leaves the University at any time prior to theexpiration of this lease, or for violation of any provisions of thislease, or for violation of any University regulation relative toresident Halls, or for health reasons, by providing the studentwith written notice of this termination 30 days prior to theeffective data of termination; unless life, limb, or property wouldbe jeopardized, the Lessee engages in the sales of purchase ofcontrolled substances in violation of federal, state or local law, orthe Lessee is no longer enrolled as a student, or the Lesseeengages in the use or possession of firearms, explosives,inflammable liquids, fireworks, or other dangerous weaponswithin the building, or turns in a false alarm, in which cases amaximum of 24 hours notice would be sufficient.14Logical VersionA ⇐ A1 ∧ A2 ∧¬BA ⇐ A4 ∧¬BA ⇐ A5 ∧¬BA ⇐ A6 ∧¬BA ⇐ A7 ∧¬BB ⇐ B1B ⇐ B2B ⇐ B3B ⇐ B4B ⇐ B5815Elements16Formal MathematicsAlgebra1. Formal language for encoding information2. Legal transformations3. AutomationLogic1. Formal language for encoding information2. Legal transformations3. Automation917Algebra ProblemXavier is three times as old as Yolanda. Xavier's ageand Yolanda's age add up to twelve. How old areXavier and Yolanda?18Algebra SolutionXavier is three times as old as Yolanda. Xavier's ageand Yolanda's age add up to twelve. How old areXavier and Yolanda?Automation: Saint, Sin, Reduce, Macsyma,Mathematicax − 3y = 0x + y = 12−4y = −12y = 3x = 91019Logic ProblemIf Mary loves Pat, then Mary loves Quincy. If it isMonday, then Mary loves Pat or Quincy. If it isMonday, does Mary love Quincy?If it is Monday, does Mary love Pat?Mary loves only one person at a time. If it isMonday, does Mary love Pat?20FormalizationSimple 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⇒ qpqm1121Rule of InferencePropositional ResolutionNB: If pi is the same as sj, it is okay to drop the twosymbols, with the proviso that only one such pairmay 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∨ ... ∨ sn22Examplesp ⇒ q⇒ p⇒ qp ⇒ qq ⇒p ⇒p ⇒ qq ⇒ rp ⇒ r1223Logic Problem Revisitedp ⇒ qm ⇒ p ∨ qm ⇒ q ∨ qm ⇒ qIf Mary loves Pat, then Mary loves Quincy. If it isMonday, then Mary loves Pat or Quincy. If it isMonday, does Mary love Quincy?24Logic Problem Concludedm ⇒ qp ∧ q ⇒m ∧ p ⇒Mary loves only one person at a time. If it isMonday, does Mary love Pat?1325Automated Reasoning26Logic 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.)1427Study Guide28Multiple LogicsPropositional LogicIf it is raining, the ground is wet.Relational LogicIf x is a parent of y, then y is a child of x.1529Common TopicsCommon TopicsSyntax - expressions in the languageSemantics - meaning of expressionsComputational MattersContrasts Expressiveness - operators, variables, terms, ... Computational Hierarchy - polynomial? decidable? Tradeoffs - expressiveness versus computability30MetaWe 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: informal1631Mike took it twice!32http://cs157.stanford.edu1733Web Service
View Full Document
Unlocking...