Introduction: Introduction Computational Logic Lecture 1 Michael Genesereth Spring 2005
Human Logic: Human Logic
Fragments of Information: Fragments of Information The 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.
Conclusions: Conclusions The 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.
Proof: Proof The 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.
Reasoning by Pattern: Reasoning by Pattern All 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.
Questions: Questions Which patterns are correct?
How many patterns are enough?
Unsound Patterns: Unsound Patterns Pattern
All x are y.
Some y are z.
Therefore, some x are z.
Good Instance
All Toyotas are Japanese cars.
Some Japanese cars are made in America.
Therefore, some Toyotas are made in America.
Not-So-Good Instance
All Toyotas are cars.
Some cars are Porsches.
Therefore, some Toyotas are Porsches.
Induction - Unsound: Induction - Unsound I have seen 1000 black ravens.
I have never seen a raven that is not black.
Therefore, every raven is black.
Now try red Hondas.
Abduction - Unsound: Abduction - Unsound If 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?
Deduction - Sound: Deduction - Sound Logical Entailment/Deduction:
Does not say that conclusion is true in general
Conclusion true whenever premises are true
Leibnitz: 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.
Formal Logic: Formal Logic
Formal Mathematics: Formal Mathematics Algebra
1. Formal language for encoding information
2. Legal transformations
Logic
1. Formal language for encoding information
2. Legal transformations
Algebra Problem: Algebra Problem Xavier is three times as old as Yolanda. Xavier's age and Yolanda's age add up to twelve. How old are Xavier and Yolanda?
Logic Problem: Logic Problem If 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?
Formalization: Formalization Simple 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?
Rule of Inference: Rule of Inference Propositional Resolution
NB: 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.
Examples: Examples
Logic Problem Revisited: Logic Problem Revisited If 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?
Logic Problem Concluded: Logic Problem Concluded Mary loves only one person at a time. If it is Monday, does Mary love Pat?
Computational Logic: Computational Logic
Automated Reasoning: Automated Reasoning
Comparison With Formal Logic: Comparison With Formal Logic Formal Logic
Syntax, semantics, correctness and completeness
Emphasis on minimal sets of rules to simplify analysis
These rules are not always easy to implement or efficient
Computational Logic
Syntax, semantics, correctness, completeness
Also concerned with efficiency
Emphasis of different languages and different sets of rules
Attention to those that better suited to automation
Applications: Applications
Mathematics: Mathematics Group Axioms
and#x8;
Theorem
Tasks:
Proof Checking
Proof Generation
Program Verification: Program Verification Program
Specification:
Tasks:
Partial Evaluation
Verification
Proof of Termination
Complexity Analysis
Hardware Engineering: Hardware Engineering Circuit: Behavior: x y z s c Applications:
Simulation
Configuration
Diagnosis
Test Generation o a b
Database Systems: Database Systems Database in Tabular Form Database in Sentential Form Constraints
Definitions
Information Integration: Information Integration Consumers
Access and Update
Own Schema Suppliers
Distributed Mgmt
Own Schema Exchanges
Master Schema
Mapping Rules
Integration Data
Regulations and Business Rules: Regulations and Business Rules
Logic Technology: Logic Technology Components
Editors
Automated Reasoning Systems
Knowledge Bases
and#x8;
Some Popular Automated Reasoning Systems
Boyer-Moore
Otter
PTTP
Epilog
Knowledge Bases
Definitions (e.g. A bachelor is an unmarried adult male.)
Constraints (e.g. PV=nRT)
Laws (e.g. 1040 necessary if earnings andgt; $10,000.)
Study Guide: Study Guide
Multiple Logics: Multiple Logics Propositional Logic
If it is raining, the ground is wet.
Relational Logic
If x is a parent of y, then y is a child of x.
Metalevel Logic
John believes everything that Mary tells him.
Common Topics: Common Topics Common Topics
Syntax - expressions in the language
Semantics - meaning of expressions
Logical Entailment - premises and conclusions
Proof Methods
Contrasts
Expressiveness - operators, variables, expressions, ...
Computational Hierarchy - linear, polynomial, decidable,...
Tradeoffs - expressiveness versus computability
Meta: Meta We will frequently write sentences about sentences.
Sentence: When it rains, it pours.
Metasentence: That sentence contains a relative clause.
We will frequently prove things about proofs.
Proofs: formal
Metaproofs: informal
Mike took it twice!: Mike took it twice!
http://logic.stanford.edu/classes/cs157/: http://logic.stanford.edu/classes/cs157/