Logic : Page 1Representations for KBS: Logic: When Sound Deduction is Required Spring 2005 6.871 Knowledge Based Systems Howard Shrobe and Kimberle Koile Syntax Proofs Semantics Sound Inference and Complete Inference What Properties hold? The Language as a Representation Comprehensiveness Ambiguity Lack of Commitment Compromises between generality and tractability Some Applications in the logic spirit Wrap-up, What pair of glasses is this? Logic : Page 1Logic : Page 2What is Logic? A “Universal" Language” A formal Inference system that “preserves truth” Not a guarantee of correct answers. General spirit is to “pour in the axioms” and grind out the theorems. E.g. to do inference, start with axioms and grind out consequences.To plan, put in the planning axioms and grind out the plans. To do diagnosis, put in the description of the device and grind out the diagnosis. A means for formally relating syntax to semantics (or denotation) or, put another way: The study of the relationship between inference and entailment. Logic : Page 2Logic : Page 3Why A Universal Language? • What can you say in Mycin-like rule languages? – There are “Contexts” meaning, roughly, objects – Rules refer to one of them – You can talk about the Values of Attributes of Objects – You can compare Object Attributes Values to Numeric Quantities • What can’t you express? – Relationships between the values of attributes of one object and the values of attributes of another object. • The location of the infectious agent is within the bloodstream of the host. • Infectious agent-1 infected host-1 is 2 days earlier than infectious agent-2 infected host-2. – Quantified things: • Every infections agent in host-1 is a coccus • There is an infectious agent in host-1 that is a coccus Logic : Page 3Logic : Page 4Predicate Logic Syntax Solves These Problems • The unit of representation is the Statement which is the application of a predicate to a set of arguments: John Loves Mary • Building blocks: Constant Symbols, Variable Symbols, Function Symbols, Predicate Symbols • A Term is: A Constant symbol: John A variable symbol: ?x The Application of a function symbol to set of terms: (Brother (Cousin John))) • A basic Statement is: The application of a predicate symbol to a set of terms. • Compound statements are formed by connecting Basic Statements using: Boolean Connectives: And, Or, Not, Implies Quantifiers: Forall, Thereis Logic : Page 4Logic : Page 5Syntax Examples (Loves Bob Mary) Bob Loves Mary (Loves (Father Bob) (Mother Judy)) The Father of Bob Loves the mother of Judy (Implies (exercises Bob) (Healthy Bob)) If Bob exercises Bob is Healthy (Forall (?y) (Thereis (?x) (Loves ?x ?y))) Everybody has somebody who loves them (Thereis (?y) (Forall (?x) (Loves ?x ?y)) There is somebody whom everybody loves (Forall (?block ?robot ?t-1) (implies (and (cleartop ?block ?t-1) (handempty ?robot ?t-1)) (and (possible-successor ?t-2 ?t-1) (results-from ?t-2 (pickup ?robot ?block ?t-1)) (holding ?robot ?block ?t-2)))) at any time that the robot’s hand is empty and there is nothing on top of the block, the robot can pick up the block and it will be holding the block in the resulting situation. Logic : Page 5Logic : Page 6An Inference System • A precise notion of “Follows From” • Deduction Rules – 2 for each connective: An introduction rule and an elimination rule – And Elimination: From (And A B) you can deduce A – Modus Ponens: •From (IMPLIES P Q) and P you can deduce Q – Universal Instantiation: • (FORALL (X) (P X)) you can deduce (P A) for any A • Axioms: Statements that are given as a priori true • A Proof is: A Sequence of statements, such that each element is either: An Axiom An Assumption warranted by a proof rule Or the results of applying a deduction rule to previous statements • Theorem: Any conclusion of a proof. – Theorems are statements we’re forced to believe if we believe the axioms Logic : Page 6Logic : Page 7Natural Deduction Rules Propositional Rules And Introduction i A j B k (And A B) (AI i j) And Elimination i (And A B) j A (AE i) Conditional Proof i (Show (Implies P Q)) i+1 | P (assumption i) j | Q k (Implies P Q) (CP (j) (i+1)) Modus Ponens i (Implies A B) j A k B (MP i j) A statement can be copied from outside a box to inside the box, but not from the inside to the outside. Exactly like the lexical scoping rules of a programming language. Logic : Page 7Logic : Page 8i Natural Deduction Rules (2) Or Introduction Or Elimination iA i(Or A B) j (Or A B) (OI i) j (Show C) k | A (assumption j) l | C m | B (assumption j) n | C o C (OE (i l n) (k m)) Double Negation Elimination Negation Introduction (not (not A)) i Show (Not A) j A (DNE i) i+1 | A (assumption) k | B l | (not B) m (not A) (NI (k l) (i+1)) Logic : Page 8Logic : Page 9Quantifier Rules A Substitution of a for x in the statement (P x) is written [a/x](P x). It means that every free occurrence of x is replaced by a in the statement (P x). The substitution is only valid if no occurrence of a is “captured” (i.e. whenever a replaces a free occurrence of x, a should also be free in that context). For Example: [a/x](Forall (y)(P x y)) = (Forall (y) (P a y)) but [y/x](Forall (y)(P x y)) is not a valid substitution Because this would give (Forall (y) (P y y)) “capturing” the substituted in y Universal Instantiation i (Forall (x) (P ... )) j [a/x](P ... ) (UI i) Universal Generalization i (P ... x ... ) j (Forall (x) (P ... x ...)) (UG i) where a is any term at all as long as [a/x] is a valid substitution. variable where the sentence in line i contains no free variables introduced by existential instantiation and the x does not occur free in assumption within whose scope line i lies. Logic : Page 9Logic : Page 10Quantifier Rules (2) Existential Instantiation Existential Generalization i (Thereis (x) (P ... )) i (P ... ) j [z/x](P ... ) (EI i) j (Thereis (x)[x/a](P ... )) (EG i) where z is a brand new variable where a is any term at all Alphabetic Variance i (Q (x)(P ... )) j (Q (z)[z/x](P ... )) (AV i) where Q is either quantifier and [z/x] is a valid substitution. Logic : Page 10Logic : Page 11Derived Rules Indirect Proof GIGO i (Show A) i (not A) i+1 | (not A) j A J | B k C (GIGO i j) k | (not B) l A (IP (j k) (i+1)) Cut i (Or A B) j