Limited Belief for Reasoning with Disjunctive Information

Limited Belief for Reasoning with Disjunctive Information Shuo Mao Lingxiang Xiang Why are we doing this? Problem: Classical reasoning service is still intractable in propositional case and undecidable in FOL.

Semantically coherent yet computationally wellbehaved reasoning service Two Extremes: logical entailment VS retrieval (augmented by some syntactic normalization) Controversy in between: semantically problematic VS structure failure Idea of Logic of Belief Instead of considering what the service must draw in terms of inference

Considering the beliefs of the system overall, and what properties the set of beliefs must satisfy. Theoretical framework for analyzing these properties: B Well defined semantics When a sentence is true; What follows Disjunctions Reconsidered

Two major applications: Rules as in Horn clauses; Incomplete knowledge(computational problem) How to deal with it in a controlled way? Subjective logic(SL) Bk Belief operators Belief level: how much case splitting is tolerated in

deriving implicit beliefs. How much resources are required to determine what is an implicit belief at that level Each belief operator will be closed under various forms of obvious reasoning like unit propagation, case splitting, subsumption Bk => Bk ( or ) or )) Syntax

The language SL is a first-order logic with equality whose atomic formulas are belief atoms of the form Bk Say L is the standard first order logic, SL is the least set of expressions such that: In short, the formulas of SL are such that all predicates other than equality must occur within a modal operator. Semantics

Sentences of SL are interpreted via a setup, which is a set of non-empty ground clauses and specifies which sentences of L are believed and which sentences of SL are true. UP(s) : closure of s under unit propagation VP(s): the set {c| c is a ground clause and there exists c from UP(s) such that c is a subset of c}

s|= Ex.a iff for some constant d, s|=axd S|= Bk iff one of the following holds: Subsume: k=0, is a clause c and c UP(s) Reduce: is not a clause and s|=(Bk ) Split: k>0 and there is some c s such that for all q c, s U {q} |= Bk-1 Example S= (a,~c,e) &(d,e)&(c)&(~d,a)&(b,~e)

(a,e) (b,d) (a,b) Query Evaluation Problem on SL Foundation for limited but decidable reasoning service Given a knowledge base KB and formula , decide whether the SL formula ( or )B0KB =>Bk )

Example Approximate Inference Lingxiang Xiang Problems in Knowledge Representation System commonsense reasoning V.S. logicist approach

logicist approach: flexible, but slow (exp) special-purpose inference algorithms: computationally attractive limited for practical application what to do with info that cannot be represented? trade-off? Knowledge Compilation compute approximations to the knowledge base speed up inference without giving up correctness or

completeness Approximating General Propositional Theories by Horn Theories Clause: a disjunction of literals A clause is Horn iff it contains at most one positive literal. Horn theory: a set of Horn clauses formulas are given in conjunctive normal form

e.g., p q r, (~p r) (~q r) q q r, (~p r) (~q r) r, (~p r) (~q r) r) q r, (~p r) (~q r) (~q r) (~q r) r) compiling propositional theories by Horn theories solve a problem in linear time if knowledge base contains only Horn clauses Approximating General Propositional Theories by Horn Theories (cont.) transfer an arbitrary set of clauses into a

logically equivalent set of Horn clause? an exact translation -> often not possible use two sets of Horn clauses to approximate the original theory upper bound bound the set of models model of original theory lower bound

Horn lower-bound and upper-bound Horn Approximation Example: non-Horn theory = (~p r) (~q r) r) q r, (~p r) (~q r) (~q r) (~q r) r) q r, (~p r) (~q r) (p r) (~q r) q). (p q r, (~p r) (~q r) q q r, (~p r) (~q r) r) (p q) (p q r, (~p r) (~q r) q) (p q)

Horn lower-bound: (p q r, (~p r) (~q r) q q r, (~p r) (~q r) r) GLBs: p q r, (~p r) (~q r) r, q q r, (~p r) (~q r) r (p q) r (p q) ((~p r) (~q r) r) q r, (~p r) (~q r) (~q r) (~q r) r)) Horn upper-bound: (~p r) (~q r) r) q r, (~p r) (~q r) (~q r) (~q r) r) LUB: r Using Bounds for Fast Inference How to improve the efficiency of a knowledge

representation system? E.g., suppose KB contains , (p q) ?? generate the Horn approximations glb , lub if lub ? => yes, logically follows glb lub if not glb ? =>no, does not logically follows answer certain queries in linear time what if no answer is obtained?

General Knowledge Compilation Framework A knowledge compilation system: L: a formal language (propositional logic in Horn) (p q) : a consequence relation over sets of sentences in L (logical entailment, subsumption, etc.) LS: source sublanguage (a general KB) LT: target sublanguage (approximations to KB) LQ: query sublanguage

fL: map a theory to a sequence of lower-bound (the last element is GLB) fU: map a theory to a sequence of upper-bound General Knowledge Compilation Framework a query ? L LQ after performing i compilation steps on the source theory . lb : i-th element of fL() ub: i-th element of fU()

if not lb (p q) ?=> no, if ub (p q) ?=> yes, otherwise, unknown Other Instances of Knowledge Compilation

generalizations of Horn clauses first-order theories logic programs terminological logics Refer the paper for details.