Statistical Relational Artificial Intelligence. Luc De Raedt

Чтение книги онлайн.

      Figure 2.5: A logic program defining nat.

2.2 FIRST-ORDER LOGIC AND LOGIC PROGRAMMING

      The probabilistic models introduced in the previous section have a fixed finite number of random variables. Boolean random variables correspond to propositions in logic, and propositions can also represent more complex random variables. First-order logic allows for an unbounded number of propositions by including logical variables, constants, and functions. The same ideas can be used for random variables. In order to understand this we now introduce first-order logic, and the directed variant, which are logic programs.

      To introduce logic and logic programs, consider Figs. 2.4 and 2.5, which contain two programs, grandparent and nat. In these programs grandparent/2, parent/2, and nat/1 are predicates (with their arity, the number of arguments, listed explicitly). The strings jef, paul, ann, and 0 are constants, whereas X, Y, and Z are logical variables, which we will just call variables when there is no confusion with random variables. All constants and variables are also terms. In addition, there exist structured terms such as s(X), which contains the functor s/1 of arity 1 and the term X. Constants are often considered as functors of arity 0. A first-order alphabet ∑ is a set of predicate symbols, constant symbols and functor symbols.

      Atoms are predicate symbols followed by the necessary number of terms, e.g., parent(jef, paul), nat(s(X)), parent(X, Z), etc. A literal is an atom, e.g., nat(s(X)), (called a positive literal) or the negation of an atom, e.g., ¬nat(s(X)) (called a negative literal).

      First-order logical formulas are recursively constructed from atoms using logical connectives (¬, ⋁ and ⋀) and quantifiers (∀ and ∃). If f₁ and f₂ are formulas then the following are formulas, too:

      • ¬f₁ (negation), which is true iff f₁ is not true;

      • f₁ ⋀ f₂ (conjunction), which is true iff both f₁ and f₂ are true;

      • f₁ ⋁ f₂ (disjunction), which is true iff either f₁ or f₂ is true;

      • f₁ → f₂, or f₂ ← f₁ (implication), which is true if f₁ is false or f₂ is true;

      • f₁ ↔ f₂ (equivalence), which is shorthand for (f₁ → f₂) ∧ (f₂ → f₁);

      • ∀Xf₁ (universal quantification), which is true if f₁ is true for every individual that X could refer to; and

      • ∃Xf₁ (existential quantification), which is true if f₁ is true for at least one individual.

      An important subset of first-order logic is that of clausal logic. A clausal theory consists of a set of clauses. A clause is a formula of the form

      where the Aj and the Bi are atoms. All variables in clauses are understood to be universally quantified. Clause (2.3) is logically equivalent to

      Example 2.2 Two example clauses are:

      The first clause states that for all X if X is human, X is either male or female. The second clause states that for all X, X cannot be both male and female, that is, no-one is both male and female. Here, false is an atom that is always false or is the empty disjunction n = 0.

      A practical subset of clausal logic is that of logic programs, which are a subset that contains no uncertainty; what is given up is the ability to state that a ∨ b is true, without saying which one of a or b is true. Logic programs are of interest because they have an intuitive declarative and procedural interpretation [Kowalski, 2014].

      A definite clause is a clause with exactly one atom in the conclusion part of the clauses (that is, n = 1). Following the Prolog tradition, definite clauses are usually written with the conjunction represented by a comma, and “if” represented by “: -”

      A is the head of the clause, and B₁, …, Bm is the body of the clause. If m = 0 the implication “: -” can be omitted and the clause is called a fact. A logic program is a set of definite clauses.

      Example 2.3 The definite clause

      can be read as: for all X, for all Y and for all Z: X is a grandparent of Y if X is a parent of Z and Z is a parent of Y. grandparent(X, Y) in the head of the clause, and parent(X, Z), parent(Z, Y) is the body of the clause.

      Example 2.4 Figure 2.4 shows a logic program defining grandparent/2 with two parent/2 facts and Fig. 2.5 a program defining nat/1.

      Reasoning with logic involves manipulating the formula as data structures. An expression is a term, atom, conjunction, or clause. The set of logical variables in expression E is denoted as Var(E). For example, in the СКАЧАТЬ