Unformatted text preview:

Consequence-FindingCS 157 Computational LogicLecture 18November 19, 2009Autumn 2009Eric KaoProof-finding vs. Consequence-findingProof-finding: Given premises and a goal, determine whether the premises entail the goal.Consequence-finding: Given premises, find the sentences which the premises entail.Uses of Consequence-findingFinding novel theoremsKnowledge CompilationPredicting program behavior (specification generation)Abduction - Residues - Diagnostics - Requirements generation - ......Abduction - Generating hypothesesGiven a set of premises Σ and a goal φ, for which sentences δ is it the case that Σ U {δ} |= φ ?Equivalently, for which sentences δ is it the case that Σ U {~φ} |= ~δ and We saw this in generating residuesConsequence-findingGiven a set of sentence:{ p | q, ~q } find all consequences.How many consequences are there?Ans: Infinitely manyHow many non-tautological consequences are there?Ans: Infinitely manyConsequence-finding: definitionGiven a set of sentences Σ, normalized in clausal form, find a set of sentences Π such that: Σ |= Π for any clause c such that Σ |= c and c is not a tautology, there exists a clause d in Π such that d subsumes c.We denote such a set Π as Con[Σ]Example: For Σ = { p | q, ~q }, which sets qualify as Con[Σ]?{ p | q, ~q } { p | q, ~q, p } { p | q, ~q, p, p | ~q}{ p | q, ~q, p, q}{ p, ~q }Example: For Σ = { p(X) | q(X), ~q(a) }, which sets qualify as Con[Σ]?{ p(X) | q(X), ~q(a) }{ p(X) | q(X), p(a), ~q(a) }{ p(a), ~q(a) } { p(X) | q(X), p(X), ~q(a) }FinitenessGiven a finite set of clauses Σ, does there always a finite Con[Σ]?In propositional logic?yesFinitenessIn first-order logic?not always.Σ = { ~p(X1,X2) | ~p(X2,X3) | p(X1,X3) }(rule form: p(X1,X2) & p(X2,X3) => p(X1,X3) )Con[Σ] = {~p(X1,X2) | ~p(X2,X3) | p(X1,X3)~p(X1,X2) | ~p(X2,X3) | ~p(X3,X4) | p(X1,X4)~p(X1,X2) | ~p(X2,X3) | ~p(X3,X4) | ~p(X4,X5) | p(X1,X5)... ... }FinitenessGiven an input Σ, if there is a finite set Con[Σ], we expect to find that finite set as output.If Con[Σ] cannot be finite, we may want to enumerate it.Method for consequence findingTruth table?Generate and test "min terms"Karnaugh mapsDoes not work for FOL in generalMethod for consequence findingFormal proofs?Hard to mechanizetermination on finite Con[Σ]?Method for consequence findingResolutions method?Generate and testHow to systematically generate FOL clauses?Consequence-finding using resolutionΣ = { p | q, ~q }1. { p, q }2. { ~q }3. { p } Res 1,2We write Σ |-*Res φ to denote that φ can be derived from Σ in a finite number of resolution steps.And we write Res[Σ] to denote { φ : Σ |-*Res φ }. Resolution closureConsequence-finding using resolutionSo what if we take Res[Σ] as Con[Σ]?The resolution rule of inference is sound. So all derived clauses are sound consequencesBut is it complete?Generative IncompletenessResolution is refutation complete: If a set of sentences Γ is unsatisfiable, Γ |-*Res { }Resolution principle is not generatively complete: If Γ |= φ, it is not necessarily the case that Γ |-*Res φCompleteness of Resolution for CF [Lee 1967]unrestricted resolution is complete for consequence-finding: That is, Res[Σ] includes every formulate needed for Con[Σ].Given any set of clauses Σ, Res[Σ] satisfies all the requirements to be Con[Σ].Notice that the resolution principle itself, used for proof finding by refutation, was introduced earlier [Robinson, 1965]Resolution Strategies?In proof-finding, unrestricted resolution involves many redundant steps which may be optimized away using various resolution strategies.Do the same strategies work for consequence-finding?Completeness of elimination strategiesIdentical clause eliminationOKTautology eliminationOKSubsumed clause eliminationOKPure literal eliminationNO{p,~q}{q,r}Completeness of restriction strategiesSet of SupportNOEmpty set of support:1. {p,q} Background2. {~p} BackgroundMissing {q}Completeness of restriction strategiesLinear resolution (unordered)OK [Minicozzi and Reiter, 1972]semi-ordered resolutionNO [Minicozzi and Reiter, 1972]S = {<p,q><p,~q>}Missing: {p}SkippingModel elimination is not complete for consequence-finding =(But variations based on skipping have been shown to be complete for consequence-finding:1. <*p, q > top clause2. <p, *q > skip p3. <p,*p> resolve against <p,~q> on ~qSOL-resolution [Inoue 1991]SFK-resolution [del Val 1999]Conclusions for consequence-findingMany applications require consequence-finding rather than simply proof-finding.Some resolution strategies are sound and complete for consequence-finding.Unfortunately, semi-ordered resolution is not complete for CF.Some variations complete for CF at the cost of increased search space.Research questionsTargeted consequences: Given a class of consequences Q, and set of clauses Σ, find Con[Σ] ∩ Q. Incremental computation: Given Con[Σ] and a new clause c, find Con[ Σ U {c} ]. Given Con[Σ] and a clause d, find Con[ Σ - {d} ].References[Inoue 1991] K. Inoue. Consequence-finding based on ordered linear resolution. IJCAI 1991. http://dli.iiit.ac.in/ijcai/IJCAI-91-VOL1/PDF/026.pdf[del Val 1999] A. del Val. A new method for consequence finding and compilation in restricted languages. AAAI 1999.http://www.aaai.org/Papers/AAAI/1999/AAAI99-038.pdf[Lee 1967] Lee, C. 1967 A Completeness Theorem and a Computer Program for Finding Theorems Derivable from Given Axioms . Doctoral Thesis. UMI Order Number: AAI6810359., University of California, Berkeley.[Minicozzi and Reiter, 1972] Eliana Minicozzi and Raymond Reiter. A note on linear resolution strategies in consequence-finding. Artificial Intelligence , 3: 175-180, 1972.


View Full Document

Stanford CS 157 - Consequence Finding

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 Consequence Finding
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 Consequence Finding 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 Consequence Finding 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?