Predicate Logic PDF - INF4067 - S8 - MAJ - IADS 2024-2025

Introduction to "Symbolic" Artificial Intelligence (a.k.a Logic Intelligent Agents) INF4067 – S8 - MAJ - IADS 2024-2025 Section 3: Predicate Logic Jacques Robin and Camilo Correa © 2022-2025  Section outline 1. Full Classical First-Order Logic (FCFOL): a relational ex...

Introduction to "Symbolic" Artificial Intelligence (a.k.a Logic Intelligent Agents) INF4067 – S8 - MAJ - IADS 2024-2025 Section 3: Predicate Logic Jacques Robin and Camilo Correa © 2022-2025  Section outline 1. Full Classical First-Order Logic (FCFOL): a relational extension of FCPL 2. Horn Classical First-Order Horn Logic (HCFOL): a practical trade-off between expressivity, explainability and inference scalability  Section readings First-Order logic: AIMA4 chapters 8 and 9  KRL Properties: Procedural vs. Declarative Procedural Declarative  Knowledge is split into:  Application specific sentences in  Application-specific data structures a KRL that an IE can use to infer or objects representing the agent’s new sentences from declared environment state space and the sentences agent’s preferences over it  Application-independent fully  Application-specific functions in a reusable IE to perform such functional language, procedures in a procedural language or methods inference in an object-oriented language  Specify in the KB only what representing the agent’s percepts, relations hold between actions and its environment’s properties events and state changes  Let the IE (e.g., a SAT solver  For each application, manually using resolution, forward or program multiple code units backward chaining) not the implementing how to derive programmer, figure out how to environment state properties infer some properties from from percepts and agent actions others based on those relations history  KRL properties: compositionality, structure and relation A KRL is compositional if:  It has syntactic composition operators to build complex sentences from atomic sentences (e.g., for CPL, logical connectives)  The semantics of the complex sentences can be derived from the semantics of its atomic components (e.g., CPL connectives truth-tables) A KRL is structured if its atomics sentences specify properties over complex data structures, rather than just over symbols  One key limitation of CPL is its lack of structure A KRL is relational if it can express, intentionally and concisely, in a single sentence, a universal relation between all individuals from N given classes  Another key limitation of CPL is that it not relational  An SQL database schema (not the data itself) is declarative and relational  But a SQL query engine is not an IE as it can only retrieve what has been explicitly stored in it and not automatically derive new data from stored data to answer a query  SQL triggers can implement such derivation but only procedurally First-Order Logic extends CPL with relational and tree structured sentences Full Classical First-Order Logic (FCFOL) Examples: X,Y,T safe(X,Y,T)  pit(X,Y)  (wumpus(X,Y)  wumpusAlive(T)) X,Y,T bel(safe(X,Y,T), T)  bel(noPit(X,Y),T)  (bel(noWumpus(X,Y),T)  bel(wumpusDead(T),T))  FCFOL vs FCPL as WW agent KRL FCFOL FCPL  X,Y,T bel(ag@(X,Y),T)   (belAg11-0  (sense(breeze,T)  bel(breeze@(X,Y))) (senseBreeze-0  belBreeze11))   S,T,U,V,X,Y bel(ag@(U,V,T), T)  (belAg12-0  X = U+1  Y = V+1  T = S+1  (senseBreeze-0  belBreeze12))  (bel(ag@(U,V,S), T)  … (do(forward, S)  sense(bump,T))) (belAg44-1000   (bel(ag@(U,Y,S), T)  (senseBreeze-1000  bel(agDir(south, S), T)  belBreeze44)) do(forward, S))  (belAg11-1-1   (bel(ag@(X,V,S), T)  (belAg11-0-1  bel(agDir(west, S), T)  (doForward-0  senseBump-1)) do(forward, S))  (belAg12-0-1   FCFOL representation exponentially belAgDirSouth-0-1  more concise and thus much faster to doForward-0-1) manually specify and concisely explain  (belAg21-0-1   Note: slides follow lowercase-uppercase belAgDirWest-0-1  conventions of logic programming, doForward-0-1)) which, for some mysterious reason, are … inverted from those of mathematical (belAg44-1000-1000  logic used in AIMA4 (belAg44-999-1000   KR with FCFOL  Ground terms: can represent application domain individuals, a.k.a. concept instances, a.k.a. object, a.k.a. entities with their properties, e.g., pit(1,2,3,7), gold(4,4)  Constant terms: can represent values of unstructured, a.k.a. simple, a.k.a. primitive, a.k.a. atomic properties, e.g., 1,2,3,7 in pit(1,2,3,7)  Logical variables: can represent intentionally properties of concepts and individuals e.g., Id,X,Y and T in pit(Id,X,Y,T)  Non-ground terms: can represent application domain concepts, a.k.a. classes, with logical variable instantiation (a.k.a. binding) representing class instantiation e.g., pit(Id,X,Y,T) instantiated into pit(1,2,3,4) with substitution {Id=1, X=2, Y=3, T=4}  Unary predicates: can represent Boolean properties of individuals e.g., alive(wumpus), alive(Actor)  As there is no built-in construct for type in CFOL (but there is in Sorted FOL), a type can be represented either:  Inside an individual, by a sub-term inside the term t representing the individual i e.g., cell(X,Y,pit)  Outside an individual by a unary predicate taking t as sole argument, e.g., pit(cell(X,Y)) i  N-ary predicates, with N  2: can represent relations among concepts or individuals, including denotational equality of two individuals with different names, e.g., has(agent, arrow), has(agent, gold), john = johnny  Quantifiers: can represent subsets of logical variable values for which a formula holds X,Y,U,V adjacent(cell(X,Y), cell(U,V))  (U = X-1  V =Y)  (U = X+1  V =Y)  (U = X  V =Y-1)  (U = X  V =Y+1)  Logical connectives: can represent complex propositions by logically composing simpler ones, with the semantics of the complex one being composed from the semantics of the simpler ones  FCFOL semantic models An atomic FCPL formulas merely logically connects unstructured symbols The semantics, a.k.a. meaning, a.k.a. interpretations a.k.a. models of a FCPLF is thus solely derived from: The cognitive association between the symbols of these atomic formulas and the IA’s environment properties they denote in the mind of the knowledge engineer who authored the KB The logical connectives truth-table FCFOL makes the same epistemological commitment about the degrees of beliefs than FCPL The degrees of belief of an agent about a particular FCFOLF can be derived from its FOLAF (First-Order Logic Atomic Formula) using truth-tables with the addition of new rules to define quantifiers semantics  FCFOL semantic models FCFOL makes a much richer first-order a.k.a. relational ontological commitment than FCPL with four semantically distinct sorts of symbols, each one allowed to appear in a distinctive syntactic positions in the FOLAF: Constant symbols appearing at the leaves of FOLAF terms to denote unstructured objects in the IA’s environment or property values of structured objects Variable symbols also appearing at the leaves of the FOLAF terms to denote sets of unstructured objects or set of structured object property values in the IA’s environment  These variables are quantified by quantifiers appearing higher in the syntactic three of the FCFOL  and that determine whether the IA’s environment’s property, represented by the FOLAF syntactic tree path where the variable occurs,  holds for all or at least one possible values of the variables Function symbols allowing to denote objects as trees with arbitrarily deep sub-term structures Predicate symbols to denote relations among objects in the IA’s environment  FCFOL semantic example  Semantic relations between ,  and  : From AIMA4 person(richard)  king(john)  brother(richard, john)  (K king(K)  (person(K)  C (onHead(K, C)  crown(C))))  shorter(leftLeg(richard), leftLeg(john)) Function symbols: {richard/0, john/0, leftLeg/1} Predicate symbols: {person/1, king/1, brother/2, onHead/2, crown/1} Variable symbols: {K, C}  FCFOL denotational semantic models How to compute the (Herbrand) model of a FCFOL f? 1. Build the Herbrand Universe HU(f) of f, i.e., the set of all ground terms that can be built with the constant and function symbols appearing in it 2. Build the Herbrand Base HB(f) of f, the conjunction of all clauses of f with their variables instantiated, a.k.a. substituted, with all possible combinations from the terms in HU(f) 3. Substitute each universally quantified FOL clause by the conjunction of all its possible instantiations into ground clauses and create a proposition symbol from each ground terms in it to obtain semantically equivalent CPL clauses 4. Substitute each existentially quantified FOL clause by a ground clause in which each existentially quantified variable is substituted by a synonymous constant symbol, a.k.a., skolemize the clause into a CPL clauses 5. Now that the set of FOL clauses have been propositionalized by a semantically equivalent set of CPL clauses, truth-table based model checking can be applied to compute MH(f)  Example of Herband universe, base and model FCFOLF l: person(richard)  king(john)  brother(richard, john)  (K king(K)  person(K))  C (onHead(K, C)  crown(C)))) HU(l): {richard, john} HB(l): person(richard)  king(john)  brother(richard, john)  (king(richard)  person(richard)  onHead(richard, richard(c))  crown(richard(c))  (king(john)  person(john)  onHead(john, john(c))  crown(john(c)) Equivalent FCPL clause propositionalization of I: personRichard  kingJohn  brotherRichardJohn  (kingRichard  personRichard  onHeadRichardRichardC  crownRichardC )  (kingJohn  personJohn onHeadJohnJohnC  crownJohnC)  FCFOL inference by propositionalization Reduces FCFOL inference to FCPL inference To answer question: f |= g, where f, g are FCFOL: Propositionalize f into prop(f) and g into prop(g) Use any FCPL IE to answer question prop(f) |= prop(g) Straightforward for Datalog CFOL sub-language: Where all predicate arguments either logical variables or constant symbols Thus, excluding deep terms structured by function symbols e.g., excluding clauses such as shorter(leftLeg(richard), leftLeg(john)) Function symbols make the Herbrand universe and thus the Herbrand base and the propositionalized formula … infinite! Example: Adding to I the clause: shorter(leftLeg(richard), leftLeg(john)) Makes HU(l) = {richard, john, leftLeg(richard), leftLeg(john),leftLeg(leftLeg(richard)), leftLeg(leftLeg(richard), …} infinite!  Herbrand’s and Gödel’s theorems Herbrand’s Theorem (1930): if a set of clauses is unSAT, then there exists a finite subset of these clauses that is also unSAT Thus, the Herbrand universe, Herbrand base, FCFOLF propositionalization and its unSAT proof can be constructed by iteratively considering deeper and deeper ground terms However, this iteration may never terminate if the set of clauses to refute is in fact SAT FCFOL entailment is merely only semi-decidable There exist inference algorithms guaranteed to prove f |= g with f, g FCFOLF, whenever f does indeed entail g But an algorithm guaranteed to find a proof for all FCFOL entailments problems cannot be devised (Gödel’s incompleteness theorem 1931)  FOLAF unification Propositionalization generates many groundings that end-up unused by the CPL IE to prove prop(f) |= prop(g) unify(f,g) is an extended form of equality between two FOLAF modulo instantiations in both f and g of sub- terms that make (f) = (g) Example: unify(p(X,f(t(a,X),Y), p(b,f(Z,c))) = p(b,f(t(a,b),c)) with X/b, Y/c, Z/t(a,b) Unification allows lifting any CPL inference rule, such as modus ponens and resolution, into a FOL inference rule FOL IE based on such lifted inference rules are more efficient than FOL IE based on propositionalization because they only make instantiations relevant to a FOL proof  FOLAF unification algorithm A FOLAF is a tree:  Rooted by a predicate symbol  With either variable or constant symbols on its leaf  With function symbols on its intermediary nodes unify(f,g) proceeds recursively by traversing synchronically both trees top-down and depth-first If root(f)  root(g) then unify(f,g) fails Else, at each step down the tree, compare nodes n(f) and m(g)  If they are different function or constant symbols, then unify(f,g) fails  Else if n(f) = X variable then:  If X does not occur in subtree(g, m(g)), the subtree down m(g), then add X/subtree(g,m(g)) to the substitution  result of unify (this test is called the occur- check)  Else unify(f,g) fails to avoid entering into an infinite loop trying to build an infinite tree, e.g., unify(s(X), s(s(X))) fails to avoid building s(s(s(…….  Else, symmetrically, if m(g) = Y, then add Y = subtree(f, n(f)) to   Else if they are the same function symbol, recurse one level down  Else if they are the same constant symbols, unify succeeds returning both  and (f)  FOLAF unification example unify(p(X,f(t(a,X),Y), p(b,f(Z,c))) p p Root: p = p OK Left subtree: add X/b to  X f b f Right subtree: Root: f = f OK Right subtree: add Y/c to  t Y Z c Left subtree: add Z/t(a,X) to  Return: a  = {X/b, Y/c, Z/t(a,X)} (p(X,f(Y,t(a,X)))) = (p(b,f(Z,c))) = p(b,f(c,t(a,b)))  FCFOLF normal forms Any FCFOLF can be put in the same semantically equivalent, normal forms than any FCPLF In those normal forms, all quantifiers are factored out left Then, all existentially quantified variables can be skolemized, leaving only universally quantified ones allowing eliding  Note that for y expression with the scope of a y, y must be skolemized by a function of x rather than a constant e.g., X Y p(X,Y) skolemizes into p(X, x(X)) for there is a potentially a different Y for each X While Y X p(X,Y) skolemizes into p(X, y) for there is a unique Y for all X  FOL normal forms Many sorted full FOL (MSFFOL) extends FCFOL with a sort (a.k.a. type) associated to some FOL terms, i.e., to atomic formula predicate arguments to restrict the interpretation domain of these arguments  Horn CFOL (HCFOL) HCFOL is the Horn restriction of FCFOL: CFOLF in INF restricted to a single concluding FOLAF Unification lifts: HCLP clause forward chaining into HCFOL clause forward chaining HCLP clause backward chaining into HCFOL clause backward chaining Forward chaining the unification-lifted modus ponens inference rule is a sound and complete method for proving HCFOL theorems Horn FOL as a specialization of FOL  HCFOL forward chaining example Natural language specification: It is a crime for an American to sell weapons to hostile nations. The country Nono, an enemy of America has some missiles, all of them sold by Colonel West, who is American. Is Colonel West a criminal? HCFOL formalization: (american(P)  weapon(W)  sells(P,W,N)  hostile(N)  crimimal(P))  owns(nono,m1)  missile(m1)  (missile(W)  weapon(W))  (enemy(N, america)  hostile(N)  (missile(W)  owns(nono,W)  sells(west,W,nono))  american(west)  HCFOL forward chaining example (american(P)  weapon(W)  sells(P,W,N)  hostile(N)  crimimal(P))  (missile(W)  weapon(W))  missile(m1)  owns(nono,m1)  (missile(W)  owns(nono,W)  sells(west,W,nono))  enemy(nono,america)  (enemy(N, america)  hostile(N))  (american(west))  HCFOL backward chaining Backward chaining the unification-lifted resolution inference rule is sound It may be incomplete if searching the AND-OR proof tree depth-first (infinite loop) Loop example: does C1  C2 |= G ? where: C1 = path(X,Y)  link(Y,Z)  path(X,Z) C2 = link(X,Z)  path(X,Z) G = path(a,c) G unifies with C1’s head with X/a, Z/c and recurses with G1 = path(a,c), same a G, also unifying with C1’s head with X/a, Z/c triggering infinite recursion It is complete if searching it breadth-first or through iterative deepening  HCFOL backward chaining example (american(P)  weapon(W)  sells(P,W,N)  hostile(N)  criminal(P))  american(west)  (missile(W)  weapon(W))  missile(m1)  (missile(W)  owns(nono,W)  sells(west,W,nono))  owns(nono,m1)  (enemy(N, america)  hostile(N))  (enemy(nono,america)) ? criminal(west)  Non-Horn FCFOLF resolution example A1: animal(f(X))  G, D |R kills(jack,tuna) (H) loves(g(X),X) E, F |R animal(tuna) (I) A2: loves(Y,f(Y))  I, B |R {Z/tuna} loves(U,V)  kills(V,tuna) (J) loves(g(Y),Y) J, H |R {V/jack, Z/tuna} loves(U,jack) (K) B: loves(U,V)  animal(Z)  C, A2 |R {Y/jack, W/f(Y)} kills(V,Z) animal(f(jack))  loves(g(jack), C: animal(W)  jack) (L) loves(jack,W) L, A1 |R {X/jack} loves(g(jack), jack) (M) D: kills(jack,tuna)  M, K |R {U/g(jack)} false kills(curiosity,tuna) E: cat(tuna) F: cat(T)  animal(T) G: kills(curiosity,tuna)  Resolution strategies The resolution inference rule (lifted or not and paired with the factoring rule) reduces the KB |= Q task of a logical IE into a search problem Thus, the key design decision of a resolution-based IE is to choose a resolution strategy specifying which pair of clauses to try to resolve at each proof step Popular strategies:  Unit preference: priority to unit clauses, i.e., made of a single literal  Unit resolution: always pick at least one unit clause (incomplete in general but complete with Horn KB)  Set of support: always pick one of the two clauses from a restricted set of support, often the negated query, to which resolvents are added  Linear resolution: always pick one clause from the KB and the other among the ancestors of the last resolvent (complete)  Selective Linear Definite (SLD):  Initially push query clause Q on a goal stack  Then always pick goal stack top with one KB clause  If they can be resolved push resolvent on goal stack  Else pick an alternative KB clause to try to resolve with the goal stack top  Complete for Horn KB  Limitations of FCFOL No quantification over predicate names Thus, no high-order relations, i.e., relations holding over a set of relations e.g., transitive closure But this can be simulated through reification Represent an IA’s environment relations R, S, etc. that must be related by a high-order relation H, G, etc. as a term appearing inside the FOLAF representing H, G, etc. Only monotonic reasoning: No changing of truth value of a over formula over time as the IA’s environment changes state and the IA accumulates knowledge of it through sensing and acting This can be simulated through axiomatization: Represent the non-monotonic reasoning system inference rules, a.k.a. axioms, as HFOL rules Axiomatization and reification go hand in hand  Example of axiomatization and reification The Event Calculus (EC) to reuse a monotonic IE to implement non- monotonic reasoning about an IA’s environment state changes cf. AIMA4 10.3 Application-independent EC axioms defining special predicates to simulate non-monotonic reasoning (happens(E,T1,T3)  initiates(E,F,T2)   terminates(F,T2,T4)  T1  T2  T3  T4  holds(F,T2,T4))  (happens(E,T1,T3)  terminates(E,F,T2)   initiated(F,T2,T4)  T1  T2  T3  T4   holds(F,T2,T4))  (terminated(F,T1,T5)   E,T1,T3,T4 happens(E,T2,T4)  terminates(E,F,T3)  T1  T2  T3  T4  T5)  (initiated(F,T1,T5)   E,T1,T3,T4 happens(E,T2,T4)  initiates(E,F,T3)  T1  T2  T3  T4  T5) Monotonically deducing  holds(F,T3,T4) after having deduced holds(F,T1,T2) models fluent F truth value changing from true to false without introducing a contradiction as long as T1  T2 < T3  T4 Application-specific knowledge rules using the EC’s predicate E = fly(A, Here, There)  happens(E,T1,T2)  terminates(E, at(A,Here), T1)  initiates(E, at(A, There), T2) Relation at is reified into a term inside FOLAF with EC predicate symbols Four top-level classes of IA inferences Four main broad classes of inference methods: 1. Deduction:  From specific knowledge of c(a) and generic causal rule X c(X)  e(X)  Deduce specific knowledge e(a) effect of cause c(a)  IE: SAT solvers, Satisfiability Modulo Theory (SMT) solvers, FOL theorem provers 2. Abduction:  From specific observation o(a) and generic causal rule X c(X)  o(X)  Abduce that specific cause c(a) may have caused o(a)  Often stated as c(a) explains o(a)  Inherently uncertain reasoning  Unless X c(X) is known to be the sole possible cause of o(X) (only if)  but then the converse rule X o(X)  c(X) also holds  and hence we know X c(X)  o(X) rather than just X c(X)  o(X)  Databases and Prolog CWA can be considered, as a limited, purely negative form of abduction  Prolog with Negation as Failure (NaF) is abduction  IE: Prolog, Abductive (Constraint) Logic Programming engines Four top-level classes of IA inferences 3. Induction  From specific knowledge (dataset) of co-occurrence observations: (c(a1),e(a1)), … , (c(an),e(an))  Induce general causal rule: X c(X)  e(X)  Also inherently uncertain  Since it can be invalidated by new observation of c(an+1) without e(an+1)  Basis for decision tree Machine Learning (ML) engines and Prolog program ML ILP engines 4. Analogy:  From specific knowledge (dataset) of co-occurrence observations: (c(a1),e(a1)), … , (c(an),e(an))  And similarity metric simil over {c(a1), …, c(an)}  When observing new specific knowledge c(an+1)  Infer by analogy derived specific knowledge e(an+1) = e(ai) where simil(c(ai), c(an+1)) =  No inference of general knowledge: instance-based reasoning  Basis for KNN  Also inherently uncertain  All ML is uncertain reasoning  Deduction based on only machine learned logic rules is thus applying certain reasoning algorithms on knowledge acquired through uncertain reasoning :). Diversity of Logic KRLs and IEs IE diversity KRL diversity