DOC PREVIEW
Stanford CS 157 - Computational Logic

This preview shows page 1-2-17-18-19-36-37 out of 37 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 37 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 37 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 37 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 37 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 37 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 37 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 37 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 37 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

IntroductionHuman LogicFragments of InformationConclusionsProofReasoning by PatternQuestionsUnsound PatternsInduction - UnsoundAbduction - UnsoundDeduction - SoundFormal LogicFormal MathematicsAlgebra ProblemLogic ProblemFormalizationRule of InferenceExamplesLogic Problem RevisitedLogic Problem ConcludedComputational LogicAutomated ReasoningComparison With Formal LogicApplicationsMathematicsProgram VerificationHardware EngineeringDatabase SystemsInformation IntegrationRegulations and Business RulesLogic TechnologyStudy GuideMultiple LogicsCommon TopicsMetaMike took it twice!http://logic.stanford.edu/classes/cs157/IntroductionComputational Logic Lecture 1Michael Genesereth Spring 20052Human Logic3Fragments of InformationThe red block is on the green block.The green block is somewhere above the blue block.The green block is not on the blue block.The yellow block is on the green block or the blue block.There is some block on the black block.A block can be on only one other block or the table (not both).A block can have at most one block on top.There are exactly 5 blocks.4ConclusionsThe red block is on the green block.The green block is on the yellow block.The yellow block is on the blue block.The blue block is on the black block.The black block is directly on the table.5ProofThe yellow block is on the green block or the blue block. The red block is on the green block.A block can have at most one block on top.Therefore, the yellow block is not on the green block. Therefore, the yellow block must be on the blue block.6Reasoning by PatternAll Accords are Hondas.All Hondas are Japanese.Therefore, all Accords are Japanese.All borogoves are slithy toves.All slithy toves are mimsy.Therefore, all borogoves are mimsy.All x are y.All y are z.Therefore, all x are z.7QuestionsWhich patterns are correct?How many patterns are enough?8Unsound PatternsPatternAll x are y.Some y are z.Therefore, some x are z.Good InstanceAll Toyotas are Japanese cars.Some Japanese cars are made in America.Therefore, some Toyotas are made in America.Not-So-Good InstanceAll Toyotas are cars.Some cars are Porsches.Therefore, some Toyotas are Porsches.9Induction - UnsoundI have seen 1000 black ravens.I have never seen a raven that is not black.Therefore, every raven is black.Now try red Hondas.10Abduction - UnsoundIf there is no fuel, the car will not start.If there is no spark, the car will not start.There is spark.The car will not start.Therefore, there is no fuel.What if the car is in a vacuum chamber?11Deduction - SoundLogical Entailment/Deduction:Does not say that conclusion is true in generalConclusion true whenever premises are trueLeibnitz: The intellect is freed of all conception of the objects involved, and yet the computation yields the correct result. Russell: Math may be defined as the subject in which we never know what we are talking about nor whether what we are saying is true.12Formal Logic13Formal MathematicsAlgebra1. Formal language for encoding information2. Legal transformationsLogic1. Formal language for encoding information2. Legal transformations14Algebra 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?x−3y=0x+y =12−4y =−12y=3x =915Logic 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?16FormalizationSimple 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⇒ qpqm17Rule of InferencePropositional ResolutionNB: If pi on the left hand side of one sentence is the same as qj in the right hand side of the other sentence, 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 same side of a single sentence, all but one of the occurrences can be deleted.p1∧...∧ pk⇒ q1∨...∨qlr1∧...∧rm⇒ s1∨...∨snp1∧...∧ pk∧r1∧...∧rm⇒ q1∨...∨ql∨s1∨...∨sn18Examplesp ⇒ q⇒ p⇒ qp ⇒ qq ⇒p ⇒p ⇒ qq ⇒ rp ⇒ r19Logic 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?20Logic Problem Concludedm ⇒ qp∧q ⇒m∧ p ⇒Mary loves only one person at a time. If it is Monday, does Mary love Pat?21Computational Logic22Automated Reasoningproof <- kbgoal in proof?r <- choose(rules)p <- choose(proof)q <- choose(proof)c <- apply(r,p,q)proof <- proof|cSuccessgoalkbrules23Comparison With Formal LogicFormal LogicSyntax, semantics, correctness and completenessEmphasis on minimal sets of rules to simplify analysisThese rules are not always easy to implement or efficientComputational LogicSyntax, semantics, correctness, completeness Also concerned with efficiencyEmphasis of different languages and different sets of rulesAttention to those that better suited to automation24Applications25MathematicsGroup AxiomsTheoremTasks:Proof CheckingProof Generation(x×y)×z =x×(y×z)x×e=xe ×x =xx×x−1=ex−1×x=e26Program VerificationProgramSpecification:Tasks:Partial EvaluationVerificationProof of TerminationComplexity Analysissorter Lsort(L)∀i.∀j.(i <j ⇒ sort(L)i<so r t(L)j)27Hardware EngineeringCircuit: Behavior:xyzscApplications:SimulationConfigurationDiagnosisTest Generationo⇔ (x∧¬y)∨(¬x∧ y)a⇔ z∧ob⇔ x∧ys⇔ (o∧¬z)∨(¬o∧z)c⇔ a∨boab28Database SystemsDatabase in Tabular Form Database in Sentential Formparentart bobart beabea coeConstraintsDefinitionsparent(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)29Information IntegrationSchemaSchemaSchema SchemaSchema Master SchemaSchemaSchemaRulesRulesRulesRulesRules Rules RulesConsumersConsumersAccess and UpdateOwn SchemaSuppliersSuppliersDistributed MgmtOwn SchemaExchangesExchangesMaster SchemaMapping RulesIntegration Data30Regulations and Business Rules31Logic TechnologyComponents Editors Automated Reasoning Systems Knowledge BasesSome Popular Automated


View Full Document

Stanford CS 157 - Computational Logic

Documents in this Course
Lecture 1

Lecture 1

15 pages

Equality

Equality

32 pages

Lecture 19

Lecture 19

100 pages

Epilog

Epilog

29 pages

Equality

Equality

34 pages

Load more
Download Computational Logic
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Computational Logic and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Computational Logic 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?