Understanding Logic and Relational Proofs in Computer Science
Explore the concepts of logical entailment, determining logical entailment, analysis of object and relation constants, good news in proofs, Fitch system for relational logic, and logical entailment and provability completeness in this comprehensive study on logic and relational proofs in Computer Science.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Introduction to Logic Relational Proofs Michael Genesereth Computer Science Department Stanford University
Logical Entailment A set of premises logically entails a conclusion ( |= ) if and only if every interpretation that satisfies also satisfies .
Determining Logical Entailment {m p q, p q} m q? 3
Determining Logical Entailment {p(a) p(b), x.(p(x) q(x))} x.q(x)?
Analysis Object constants: n Binary relation constants: k Factoids in Herbrand Base: k*n2 Interpretations: 2k*n2 Object constants: 4 Binary relation constants: 4 Factoids in Herbrand Base: 64 Interpretations: 264 = 18,446,744,073,709,551,616 5
Good News Good News: If logically entails , then there is a finite proof of from . And vice versa. Good News: If logically entails , it is possible to find such a proof in finite time. More Good News: Such proofs are often much smaller than the corresponding truth tables.
Logical Entailment and Provability Completeness A set of premises logically entails a conclusion ( |= ) if and only if every interpretation that satisfies also satisfies . If there exists a proof of a sentence from a set of premises using the rules of inference in R, we say that is provable from using R (written R ).
Soundness and Completeness A proof system is sound if and only if every provable conclusion is logically entailed. If , then . A proof system is complete if and only if every logical conclusion is provable. If , then .
Fitch Theorem: Fitch is sound and complete for RelationalLogic. |= if and only if Fitch . Upshot: The truth table method and the proof method succeed in exactly the same cases!
Logical Rules of Inference Negation Introduction Negation Elimination And Introduction And Elimination Or Introduction Or Elimination Assumption Implication Elimination Implication Introduction Biconditional Introduction Biconditional Elimination
New Rules of Inference Universal Elimination Domain Closure Universal Introduction Universal Reasoning Existential Introduction Existential Elimination Existential Reasoning
Universal Elimination (UE) . where is ground NB: is an instance of with alloccurrences of replaced by .
UE Examples Premise: x.hates(jane,x) Conclusions: x jill x jane hates(jane,jill) hates(jane,jane) Non-Conclusions: hates(jane,y) Must be ground. x y Wrong!
UE Examples Premise: x.hates(x,x) Conclusions: x jane hates(jane,jane) hates(jill,jill) x jill Non-Conclusions: hates(jane,x) hates(x,jane) hates(x,x) Must be ground. x jane Wrong! x jane Wrong! x jane Wrong!
UE Examples Premise: x. y.hates(x,y) Conclusions: y.hates(jane,y) x jane
UE Examples Premise: x. y.hates(x,y) Conclusion: y.hates(jane,y) x jane Subsequent Conclusion: hates(jane,jill) hates(jane,jane) y jill y jane
Domain Closure [ 1] [ n] every object constant } . [ ]
DC Example likes(abby,cody) likes(bess,cody) likes(cody,cody) likes(dana,cody) x.likes(x,cody)
DC Example likes(abby,abby) likes(bess,bess) likes(cody,cody) likes(dana,dana) x.likes(x,x)
DC Example likes(abby,cody) likes(cody,abby) likes(bess,cody) likes(cody,bess) likes(cody,cody) likes(cody,cody) likes(dana,cody) likes(cody,dana) x.(likes(x,cody) likes(cody,x))
DC Example y.likes(abby,y) y.likes(bess,y) y.likes(cody,y) y.likes(dana,y) x. y.likes(x,y)
Proof y.(likes(cody,y) happy(y)) y.likes(cody,y) likes(cody,abby) happy(abby) likes(cody,abby) happy(abby) likes(cody,bess) happy(bess) likes(cody,bess) happy(bess) likes(cody,cody) happy(cody) 1. 2. 3. 4. 5. 6. 7. 8. 9. 10. likes(cody,cody) 11. happy(cody) 12. likes(cody,dana) happy(dana) 13. likes(cody,dana) 14. happy(dana) Premise Premise UE: 1 UE: 2 IE: 4, 3 UE: 1 UE: 2 IE: 6, 7 UE: 1 UE: 2 IE: 9, 10 UE: 1 UE: 2 IE: 12, 13
Example 1. y.(likes(cody,y) happy(y)) 2. y.likes(cody,y) 3. likes(cody,c) happy(c) 4. likes(cody,c) 5. happy(c) 6. y.happy(y) Premise Premise UE: 1 UE: 2 IE: 4, 3 UI: 5
Reasoning About Arbitrary Objects Examples If we can prove a property about an arbitrary object, then it must be true of all objects. Common type of mathematical reasoning: Let c be an arbitrary object. We can prove that a particular property is true of c. Therefore, the property is true of everything.
Examples Placeholders A placeholder is a new type of symbol that stands for an arbitrary object constant but is not itself an object constant. Spelled the same as object constants. Placeholders must be disjoint from object constants. Object Constants: abby, bess, cody, dana Placeholder: c Sometimes written in brackets: [c] Placeholders are used only within the Fitch procedure, never used outside of the procedure.
Universal Introduction (UI) where is a placeholder not used in any active assumption NB: is an instance of with alloccurrences of replaced by .
UI Example Object Constants: jane, ... Placehoders: c, ... Premise: hates(c,jane) Conclusion: x.hates(x,jane)
UI Example Object Constants: jane, ... Placehoders: c, ... Premise: hates(c,jane) hates(jane,c) Conclusion: x.(hates(x,jane) hates(jane,x)) c x
Example Premises: x.p(x) x.(p(x) q(x)) Goal: x.q(x)
Proof 1. x.(p(x) q(x)) 2. x.p(x) 3. p(c) q(c) 4. p(c) 5. q(c) 6. x.q(x) Premise Premise UE: 1 UE: 2 IE: 4, 3 UI: 5
Problem Premises: x.(q(x) r(x)) x.(p(x) q(x)) Goal: x.(p(x) r(x))
Proof x.(p(x) q(x)) x.(q(x) r(x)) p(c) q(c) q(c) r(c) | p(c) 1. 2. 3. 4. 5. Premise Premise UE: 1 UE: 2 Assumption n IE: 5, 3 IE: 6, 4 II: 5, 7 UI: 8 6. 7. 8. 9. | q(c) | r(c) p(c) r(c) x.(p(x) r(x))
General Lovers Lovers Everybody loves somebody. Everybody loves a lover. Show that everybody loves everybody. Premises: y. z.loves(y,z) x. y.( z.loves(y,z) loves(x,y)) Conclusion: x. y.loves(x,y)
Proof Everybody loves somebody. Everybody loves a lover. Show that everybody loves everybody. 1. y. z.loves(y,z) 2. x. y.( z.loves(y,z) loves(x,y)) Premise 3. z.loves(d,z) 4. y.( z.loves(y,z) loves(c,y)) 5. z.loves(d,z) loves(c,d) 6. loves(c,d) 7. y.loves(c,y) 8. x. y.loves(x,y) Premise UE: 1 UE: 2 UE: 4 IE: 5, 3 UI: 6 UI: 7
Universal Introduction (UI) where is a placeholder not used in any active assumption NB: is an instance of with alloccurrences of replaced by .
Bad, Bad, Bad "Proof" x.(p(x) q(x)) p(a) p(c) q(c) | p(c) | q(c) | y.q(y) p(c) y.q(y) x.(p(x) y.q(y)) p(a) y.q(y) y.q(y) 1. 2. 3. 4. 5. 6. 7. 8. 9. 10 . Premise Premise UE: 1 Assumption IE: 5, 3 UI: 5 NO!!! II: 4, 6 UI: 7 UE: 8 IE: 9, 2 Wrong.
Universal Introduction (UI) where is a placeholder not used in any active assumption NB: is an instance of with alloccurrences of replaced by .
Name Conflict Not Cool 1. y.(likes(cody,y) happy(y)) Premise 2. likes(cody,abby) Premise 3. likes(cody,abby) happy(abby) UE: 1 4. happy(abby) IE: 3, 2 5. y.happy(y) Wrong. UI: 4
Reasoning Tip for Universal Reasoning If you have some universal sentences and you want to prove a universal sentence, use placeholders to eliminate the universals, prove a specific conclusion, then generalize.
Proof x.(p(x) q(x)), x.(q(x) r(x)) x.(p(x) r(x)) x.(p(x) q(x)) x.(q(x) r(x)) p(c) q(c) q(c) r(c) | p(c) 1. 2. 3. 4. 5. Premise Premise UE: 1 UE: 2 Assumption n IE: 5, 3 IE: 6, 4 II: 5, 7 UI: 8 6. 7. 8. 9. | q(c) | r(c) p(c) r(c) x.(p(x) r(x))
Existential Introduction (EI) . where is a constant NB: is an instance of with 0 or moreoccurrences of replaced by .
Examples EI Examples Premise: hates(jill,jill) Conclusions: x.hates(x,x) x.hates(jill,x) x.hates(x,jill) Two Applications: x. y.hates(x,y)
Examples EI Examples Premise: x.hates(x,x) Non-Conclusion: y. x.hates(x,y) Wrong. Constants only!
EE Example Premises: x.(hates(jane,x) mean(jane)) x.hates(jane,x) Conclusion: mean(jane)
