CS 561, Session 191Logical reasoning systems• Theorem provers and logic programming languages• Production systems• Frame systems and semantic networks• Description logic systemsCS 561, Session 192Logical reasoning systems• Theorem provers and logic programming languages – Provers: use resolution to prove sentences in full FOL. Languages: use backwardchaining on restricted set of FOL constructs.• Production systems – based on implications, with consequentsinterpreted as action (e.g., insertion & deletion in KB). Based onforward chaining + conflict resolution if several possible actions.• Frame systems and semantic networks – objects as nodes in agraph, nodes organized as taxonomy, links represent binaryrelations.• Description logic systems – evolved from semantic nets. Reasonwith object classes & relations among them.CS 561, Session 193Basic tasks• Add a new fact to KB – TELL• Given KB and new fact, derive facts implied by conjunction of KBand new fact. In forward chaining: part of TELL• Decide if query entailed by KB – ASK• Decide if query explicitly stored in KB – restricted ASK• Remove sentence from KB: distinguish between correcting false sentence, forgetting useless sentence, or updating KB re. change in the world.CS 561, Session 194Indexing, retrieval & unification• Implementing sentences & terms: define syntax and map sentences onto machine representation.Compound: has operator & arguments.e.g., c = P(x) ∧ Q(x) Op[c] = ∧; Args[c] = [P(x), Q(x)]• FETCH: find sentences in KB that have same structure as query.ASK makes multiple calls to FETCH.• STORE: add each conjunct of sentence to KB. Used by TELL.e.g., implement KB as list of conjunctsTELL(KB, A ∧¬B)TELL(KB, ¬C ∧ D)then KB contains: [A, ¬B, ¬C, D]CS 561, Session 195Complexity• With previous approach, FETCH takes O(n) time on n-element KBSTORE takes O(n) time on n-element KB (if check for duplicates)Faster solution?CS 561, Session 196Table-based indexing•Use hash table to avoid looping over entire KB for each TELL or FETCHe.g., if only allowed literals are single letters, use a 26-element array to store their values.• More generally: - convert to Horn form- index table by predicate symbol- for each symbol, store:list of positive literalslist of negative literalslist of sentences in which predicate is in conclusionlist of sentences in which predicate is in premiseCS 561, Session 197Tree-based indexing• Hash table impractical if many clauses for a given predicate symbol• Tree-based indexing (or more generally combined indexing):compute indexing key from predicate and argument symbolsPredicate?First arg?CS 561, Session 198Unification algorithm• Using clever indexing, can reduce number of calls to unification• Still, unification called very often (at basis of modus ponens) => need efficient implementation.• See AIMA p. 303 for example of algorithm with O(n^2) complexity(n being size of expressions being unified).CS 561, Session 199Logic programmingRemember: knowledge engineering vs. programming…CS 561, Session 1910Logic programming systemse.g., Prolog:• Program = sequence of sentences (implicitly conjoined)• All variables implicitly universally quantified• Variables in different sentences considered distinct• Horn clause sentences only (= atomic sentences or sentences withno negated antecedent and atomic consequent)• Terms = constant symbols, variables or functional terms• Queries = conjunctions, disjunctions, variables, functional terms• Instead of negated antecedents, use negation as failure operator: goal NOT P considered proved if system fails to prove P• Syntactically distinct objects refer to distinct objects• Many built-in predicates (arithmetic, I/O, etc)CS 561, Session 1911Prolog systemsCS 561, Session 1912Prolog exampleCS 561, Session 1913Expanding Prolog• Parallelization:OR-parallelism: goal may unify with many different literals andimplications in KBAND-parallelism: solve each conjunct in body of an implicationin parallel• Compilation: generate built-in theorem prover for different predicates in KB• Optimization: for example through re-orderinge.g., “what is the income of the spouse of the president?”Income(s, i) ∧ Married(s, p) ∧ Occupation(p, President)faster if re-ordered as:Occupation(p, President) ∧ Married(s, p) ∧ Income(s, i)CS 561, Session 1914Theorem provers• Differ from logic programming languages in that:- accept full FOL- results independent of form in which KB enteredCS 561, Session 1915OTTER• Organized Techniques for Theorem Proving and Effective Research (McCune, 1992)• Set of support (sos): set of clauses defining facts about problem• Each resolution step: resolves member of sos against other axiom• Usable axioms (outside sos): provide background knowledge about domain• Rewrites (or demodulators): define canonical forms into which terms can be simplified. E.g., x+0=x• Control strategy: defined by set of parameters and clauses. E.g., heuristic function to control search, filtering function to eliminate uninteresting subgoals.CS 561, Session 1916OTTER• Operation: resolve elements of sos against usable axioms• Use best-first search: heuristic function measures “weight” of each clause (lighter weight preferred; thus in general weight correlated with size/difficulty)• At each step: move lightest close in sos to usable list, and add to usable list consequences of resolving that close against usable list• Halt: when refutation found or sos emptyCS 561, Session 1917ExampleCS 561, Session 1918CS 561, Session 1919CS 561, Session 1920Forward-chaining production systems• Prolog & other programming languages: rely on backward-chaining(I.e., given a query, find substitutions that satisfy it)• Forward-chaining systems: infer everything that can be inferred from KB each time new sentence is TELL’ed• Appropriate for agent design: as new percepts come in, forward-chaining returns best actionCS 561, Session 1921Implementation• One possible approach: use a theorem prover, using resolution to forward-chain over KB• More restricted systems can be more efficient.• Typical components:- KB called “working memory” (positive literals, no variables)- rule memory (set of inference rules in formp1 ∧ p2 ∧ … Þ act1 ∧ act2 ∧ …- at each cycle: find rules whose premises satisfiedby working memory (match phase)- decide which should be executed
View Full Document