6. Logic-Based Reasoning

Of course, we mean programs which are correct syntactically.

As we have mentioned in Sect.  2.​2, we do not specify how a program should be executed in the declarative paradigm.

A rule of inference in FOL should not be mistaken for the notion of a rule in rule-based systems, which are a subclass of expert systems. In the first case rules of inference are formulas of reasoning schemes (e.g., the modus ponendo ponens rule), which are used in order to process axioms, which are stored in a knowledge base. These axioms are either facts, which concern the domain of an application of the AI system, or principles (rules), which are valid in this domain. In the second case (rule-based systems) rules are equivalents of such axioms-principles, which are valid in the domain.

We do not discuss here all definitions related to the FOL semantics. They are included in Appendix C.1.

See Definition C.12 in Appendix C.1.

Formal notions, which concern reasoning in logic are contained in Appendix F.2.

In the general case the resolution rule is defined for disjunctions consisting of any (finite) number of elements in the following way: \({\displaystyle \frac{\ \lnot \alpha \vee \beta _{1} \vee \cdots \vee \beta _{k}, \alpha \vee \gamma _{1} \vee \cdots \vee \gamma _{n}}{\beta _{1} \vee \cdots \vee \beta _{k} \vee \gamma _{1} \vee \cdots \vee \gamma _{n}}}\).

If an implication formula is of the form: “If Condition-1 and Condition-2 and ... and Condition-n, then Result”, formally speaking \(C_{1} \wedge C_{2} \wedge \cdots \wedge C_{n} \Rightarrow R\), then we generate a clause \(\lnot C_{1} \vee \lnot C_{2} \vee \cdots \vee \lnot C_{n} \vee R\). This clause contains at most one positive literal.

Alfred Horn—a professor of mathematics at the University of California, Berkeley. He introduced this form in 1951. His research results in the areas of universal algebra and lattice theory are very important in logic programming.

Of course, not all substitutions are allowable. For example, the replacement of a variable with a term which contains this variable is not allowed.

In the previous section, we have made use of the fact that the starting formula ( 6.19) was already in conjunctive normal form.

The rules of formula normalization are discussed in detail in monographs on the mathematical foundations of computer science, which are listed at the end of this chapter in a bibliographical note.

We can just keep in mind that they are at the front of the formula.

After moving quantifiers to the front we do not see which quantifier concerns which part of a conjunction.

Thoralf Albert Skolem—a professor of mathematics at the University of Oslo. His work, which concerns mathematical logic, algebra, and set theory (Löwenheim-Skolem theorem) is of great importance in the mathematical foundations of computer science.

After such a replacement the variable y “disappears”, so the quantifier \(\exists y\) does not quantify any variable. As a result, we can eliminate it.

We make use of a FOL rule of distribution of disjunction over conjunction:

\([ \ \alpha \ \ \vee ( \beta \wedge \gamma ) ] \Leftrightarrow [ \ ( \alpha \vee \beta ) \wedge ( \alpha \vee \gamma ) ]\).

As we have mentioned above, a Horn clause contains at most one positive literal. The clauses in ( 6.39) are Horn clauses, because each one contains only one positive literal student( x).

If we combine clauses belonging to various formulas, we should, once more, rename variables so that symbols of variables which belong to different formulas are also different.

String Rewriting Systems and Graph Rewriting Systems are formal models for AI systems based on generative grammars. They are introduced in Chap.  8.

In the formal definition of a term, a constant does not occur explicitly, because a zero-argument function is treated as a constant.

Applying the rules of inference in logic introduced in the previous sections is a good analogy to applying term rewriting rules.

Giuseppe Peano defined arithmetic operations for natural numbers with the help of one constant— zero—and one operation— successor.

Such a situation is analogous to the “Chinese room” thought experiment discussed in Chap.  1.

If we perform an addition \(m+n\), then always we have to apply n times the rule \(r_2\) and at the end we have to apply once the rule \(r_1\). This is the only possible sequence of operations.

John Barkley Rosser, Sr.—a professor of mathematics, logic, and computer science at the University of Wisconsin-Madison, a Ph.D. student of Alonzo Church. An author of excellent publications in logic, number theory, and ballistics.

For example, a “system of cooking” does not have the Church-Rosser property, which is known to the author of this monograph from personal experience. Any time I replace a model sequence of culinary operations (by mistake, of course) by another one, I obtain an unacceptable result.

We consider here the untyped lambda calculus.

The second such popular system, namely combinatory logic, was introduced by Moses Schönfinkel in 1920. The ideas of Schönfinkel were further developed by Haskell Brooks Curry in 1927.

Independently, A.M. Turing showed the same with the help of his abstract machine (now called a Turing machine) in 1937 [306].

We define notions in a simplified way, since we introduce lambda calculus in this section in an informal way. Therefore, we omit the subtle difference between lambda expression and lambda term (which is the equivalence class of lambda expressions), etc. Formal definitions which concern lambda calculus are contained in Appendix C.3.

Let us notice that we have already met such a situation, when we considered term rewriting systems. For example, an expression S( S( S(0))) can be interpreted either as the process of computing the third successor of the constant 0 or as a result of this computation, i.e., 3—-see formula ( 6.47).

This technique is called currying (as a reference to H.B. Curry) or Schönfinkelisation (referring to M. Schönfinkel).

We have met an analogous problem when we discussed methods based on FOL in a previous section—cf. formulas ( 6.34) and ( 6.35).

Both the variable which is replaced and the expression which replaces it are underlined.

The (universal) Turing machine and recursively definable functions are models which are equivalent to the lambda calculus, according to this thesis.

Haskell Brooks Curry—a mathematician and logician, a professor at the Pennsylvania State University. David Hilbert and Paul Bernays were his doctoral advisors. The functional programming languages Haskell and Curry are named after him.

William Alvin Howard—a mathematician and logician, a professor at the University of Illinois at Chicago. Author of well-known papers in proof theory.

Prolog, introduced in Sect.  6.4, is the second classic language in AI.