Telecom Paris Dep. Informatique & Réseaux Nils Holzenberger ← Home page February 2024

Neuro-Symbolic Artificial Intelligence

with

Simon Coumes

and

Zacchary Sadeddine

➜            other AI courses

Avec le mot "si", on peut faire
tout ce qu’on ne peut pas faire.
    (Pierre Dac) In the foreword of the LPAR-16 Conference, one can read:

Logic is a fundamental organizing principle in nearly all areas in Computer Science. (...) At one extreme, it underlies computability and complexity theory and the formal semantics of programming languages. At the other, it drives billions of gates every day in the digital circuits of processors of all kinds. Logic is in itself a powerful programming paradigm but it is also the quintessential specification language for anything ranging from real-time critical systems to networked infrastructures. Logical techniques link implementation and specification through formal methods such as automated theorem proving and model checking. Logic is also the stuff of knowledge representation and artificial intelligence. Because of its ubiquity, logic has acquired a central role in Computer Science education.

ARISTOTLE founded logic as the art of reasoning and of arguing. His aim was to find all the ways in which propositions could be linked together so that any particular reasoning could be formalized. His favorite tool was the syllogism (any a is a b, a₀ is a a, so a₀ is a b) by which it explained deduction, induction and abduction.^[Note1] This tradition has seen developments with the Stoics, then in the Middle Ages by the time of William of OCKHAM (fourteenth century). It reaches one of its peaks with the Logic of Port Royal (seventeenth century). Logic, in this context, is seen as a rigorous description of the art of reasoning and of convincing: what is logical provokes acceptance. Any sensible person (endowed with the Cartesian Good Sense) who accepts that a and b are two incompatible facts, that is, are mutually exclusive, must accept that if a occurs, then b is not the case. If the same person finds that it is b that occurred after all, she will have to conclude that a must be false.

This art of persuasion finds a natural extension in the idea that logic describes the processes of rational thought. Indeed, its mechanisms seem obvious to anyone, whatever the contents on which they operate. This idea has been developed by Emmanuel KANT, who distinguishes between transcendental logic, that is, the thought processes that are characteristic of the human mind, and logic as a system of laws as it is used by different domains of science. Transcendental logic is no longer a mere tool, an ‘Organon’ in the sense of ARISTOTLE. Studying it amounts to studying an essential aspect of human cognition.

Readings:

• KING, P. & SHAPIRO, S. (1995). The history of logic. In T. Honderich (Ed.), The Oxford companion to philosophy, 496-500. Oxford, UK: Oxford University Press.
• and a comic strips:
  DOXIADIS, A., PAPADIMITRIOU, C. & PAPADATOS, A. (2010). Logicomix. Paris : Vuibert.

As an answer to KANT’s "psychological" way of considering logic, founders of mathematical logic, such as George BOOLE (The mathematical Analysis of Logic, 1847; An Investigation of the Laws of Thought, 1854), Gottlob FREGE (Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens, 1879), Bertrand RUSSELL et Alfred WHITEHEAD (Principia Mathematica, 1910-1913) and Ludwig WITTGENSTEIN (Tractatus logico-philosophicus, 1921), made a radical distinction between formal aspects of reasoning and meaning. Their rejection of psychologism led them to distinguish between syntax and semantics. They succeeded in ‘syntactizing’ logic, and beyond logic, they tried to ‘syntactize’ mathematics, and even the world itself, considered as a set of absolute entities, according to a Platonic conception and in radical opposition to the Kantian view.

This idea of describing the world in an unambiguous and error-free manner was already present in Gottfried LEIBNIZ’ work (Vom Nutzen der Vernunftkunst oder Logik, 1696). He saw in logic a universal lingua rationalis. The inclination for syntactic formalism also has its roots in the development of axiomatic theories in mathematics. During the nineteenth century, EUCLID’s axiomatics was brought into question. The subsequent advent of non-Euclidean geometries was a serious blow to the primacy of what KANT called pure intuition. On the technical level, early developments in mathematical logic were made possible by the advent of set theory and modern algebra, following the work of Richard DEDEKIND, Georg CANTOR, George BOOLE and Augustus DE MORGAN. On the conceptual level, the work of the American philosopher Charles PEIRCE clarified the relationship between logic and reasoning. But a decisive step was taken when Gottlob FREGE and Bertrand RUSSELL introduced the notion of quantification, thanks to which individual entities and their properties can be formally distinguished.

Nowadays, automated theorem proving is based on the syntax/semantics distinction. The point is to convert semantic reasoning into purely syntactic processing that is parallel to semantics, but independent from it. The additional requirement of automated theorem proving is that proofs should be found in reasonable time.

Semantics corresponds to the meaning of symbols (and, eventually, to their evaluation). The development of non-Euclidian geometries at the end of the nineteenth century, and then Kurt GÖDEL’s incompleteness theorems in the nineteen thirtees, led to semantic relativism. Symbols are no longer considered to have a fixed reference. Their meaning may vary depending on the context. This change of perspective culminated with Model Theory. It makes the distinction between (local) truth (if a means "I am swimming" and b means "I am in water", (a ⊃ b) is true) on the one hand, and (universal) validity on the other hand ((a ⊃ a) is valid: it is always true, whatever the meaning of a). With Model Theory, studying Logic consists in formalizing properties and relations involved in reasoning, before applying them to concrete situations. The syntax of Logic is separated from its semantics. The latter consists in considering a specific domain in which all symbols get interpreted. Conversely, one may consider the ‘truth conditions’ of a logic formula, i.e. the set of domains (or worlds) in with the formula, once interpreted, is true.

Yet the same logic, with all its formal properties, can be used in a totally different way, which reconnects with Immanuel KANT’s ‘psychologizing’ tradition. Within the framework of the Cognitive Sciences, one can see in Logic not a means to evaluate the truth of utterances, but a tool to test their consistency. By showing that a speaker, through a complex arrangement of utterances, ends up saying one thing and its opposite, in other words that she asserts a along with other facts from which ¬ a can be deduced, this speaker can be regarded as being wrong, without needing to decide which of a or ¬ a is true (¬ designates negation). It should be remembered that Logic was born from argumentation: for ARISTOTLE (The Analytics, ~ -330), Logic was not separated from the art of convincing. Similarly, a scientist who shows that the facts she observes logically lead to a hypothesis (e.g., the photoelectric effect would force her to consider the existence of photons), merely establishes a logical link between propositions, without being able to establish any truth (Karl POPPER, Logik der Forschung, 1935).^[Note2]

To emphasize the difference between the traditional, truth-conditionalist approach (which is concerned with knowing the truth conditions of statements) and the argumentative approach, note that the former ceases to function in the presence of an inconsistency: from a & (¬ A), we can deduce that all things are true! Ironically, theoretical scientific inquiry, like argumentation, proceeds from a starting point which is an inconsistency. Though logicians pursue objectives that differ from what they are in science, in epistemology or in cognitive science, Logic is used almost in the same way in all these contexts.

Notes:

• The way adopted here to present propositional Logic follows the classical textbook of Melvin FITTING:
  FITTING, M. (1996). First-Order Logic and Automated Theorem Proving. New York: Springer Verlag.
• An history of logical proof automation can be found in:
  LOVELAND, D. W. (1983). "Automated theorem proving: A quarter century review". Proceeding of the special session on Automated Theorem Proving, 89th annual meeting of the American Mathematical Society, 1-15.
• Introducions to logic are available from various sources, e.g. the Stanford Encyclopedia of Philosophy.

The syntax of propositional language result from the following construction.

    - propositional symbols: p1, p2, ...    

    - connectives

• unary connective: ¬ (negation)
• binary connectives: ∧, ∨, ⊃, ⊂, ↑, ↓, ⊅, ⊄, ≡, ≠ (and, or, implies, only-if, nand (incompatible), nor, not-implies, not-onlyif, equivalent, not-equivalent)

    - atomic formulas

• propositional symbols
• ⊤, ⊥ (top, bottom)

    - set P of propositional formulas

• P contains atomic formulas
• If F is in P, then ¬F is in P
• If F and G are in P, then (F o G) is in P, where o is a binary connective.

    - P is the smallest set that has these properties.

Any element of P is said to be a "well-formed" expression. The objective of propositional calculus is, as we will see, to give a truth value to any well-formed propositional expression, starting from the truth value of their constituents. In particular, we seek out tautological propositional formulas, which are true whatever the truth values of their constituents.

Using the Prolog predicate op, one can define the unary operator - and nine binary operators and, or, imp, impinv, nand, nor, nonimp, nonimpinv, equiv.

% The first argument of 'op' gives precedence (converse of priority).
:-op(140, fy, -).        % 'fy' means right-associative: '- -X' means '-(-X)'
:-op(160,xfy, [and, or, equiv, imp, impinv, nand, nor, nonimp, equiv, nonimpinv]).    
    % 'xfy' means that: X and Y and Z = X and (Y and Z)
    % Note that '-' has priority over 'and', due to its lower precedence.

This is for the sake of convenience. From Prolog, consult the file containing these lines. Prolog now understands -p as -(p), and a and b as and(a,b). You may try X = and(a,b).
Verify that Prolog now accepts an expression lile:
    
    X = ((a and b) or (c and d)).

According to the logical tradition, "semantics" is about deciding on the truth of a proposition. This habit distorts the usual meaning of the word semantics, which is related to meaning and not to epistemic attitudes. Semantics stricto sensu is concerned with what utterances refer to in the (or a) world. It establishes a link between the propositional symbols and statements about a given world. The semantics of p could be the statement "John is angry" in the world of everyday psychology. Semantics must lead to statements whose truth value can then be determined without ambiguity. On the other hand, assigning a truth value corresponds to a propositional attitude, not to a reference. Unfortunately, logicians tend to conflate these two steps by calling "propositional semantics" the operation which consists in directly assigning a truth value to the propositional symbols themselves.

The "semantics" of propositional language is well known, as it is given by Truth Tables. We need to define a unary semantic operator and 16 binary semantic operators. Note that only 10 of them depend on their two arguments. The others, except for the tautology (always true) and the contradiction (always false) are said to be "degenerate".

	not
T	F
F	T

		and	or	imp	impinv	nand	nor	nimp	nimpinv	equ	nequ
T	T	T	T	T	T	F	F	F	F	T	F
T	F	F	T	F	T	T	F	T	F	F	T
F	T	F	T	T	F	T	F	F	T	F	T
F	F	F	F	T	T	T	T	F	F	T	F

		T	F	"degenerate" connectives
T	T	T	F	T        T        F        F
T	F	T	F	T        F        F        T
F	T	T	F	F        T        T        F
F	F	T	F	F        F        T        T

Now, we can make the link with syntax by granting a truth value to any propositional formula. This is what valuations do.

- Space of truth values:    T = {T, F} (propositional attitudes)
- Boolean valuation:    v: P ➜ T

• v(⊤) = T ; v(⊥) = F
• v(¬X) = not v(X)
• v(X o Y) = v(X) • v(Y) where the binary (syntactic) o and (semantic) • connectives correspond to teach other (∧ corresponds to and, ⊃ corresponds to imp, ≡ corresponds to equ, and so on).

A propositional formula X is a tautology if v(X) = T for any Boolean valuation v.
One can see that X is a tautology iff (X ≡ T) is a tautology.

A set S of propositional formulas is satisfiable if some valuation v₀ maps every member of S to T: v₀(X) = T for any X of S. One can easily verify that X is a tautology if and only if {¬X} is not satisfiable.

To know whether a formula is a tautology, one has to test all valuations. A valuation can be assimilated to the set of propositional symbols that it evaluates as true. Let’s build a valuation generator (already present in the file). For three propositions a, b and c:

is_true(V, X) :-
    member(X,V).    % only true elements are explicitly mentioned in V

valuation(V) :-
    % we keep all elements that V sends to true.
    % all other elements are supposed to be false.
    sub_set(V, [a,b,c]).

sub_set([], []).
sub_set([X|XL], [X|YL]) :-
    sub_set(XL, YL).
sub_set(XL, [_|YL]) :-
    sub_set(XL, YL).

To test the program, one have to ask this type of question:

?- valuation(V), is_true(V, a and -b).
    V = [a, c];    % this means that if a and c are true and b false, the formula is true
    V = [a]        % this means that if a is true, and b and c are false, the formula is true

(remember to type ‘;’ to get all solutions). Verify that the preceding formulas (Morgan’s et Frege’s) are tautologies.

Logic can be understood as the art of finding out formulas that are always true, i.e. tautologies (like X ⊃ X), their negation (contradictions) that are always false, and finally formulas which may be either true or false depending on the valuation chosen. From this point of view, truth tables are a quite simple way of deciding about the truth of any formula. One could stop there! In practice, however, we cannot be satisfied with truth tables: if n propositions are involved in a formula, we must systematically go through a table of size 2ⁿ, which requires a calculation time or a memory space that is prohibitive when dealing with a knowledge base^[Note3] of even modest size. Moreover, truth tables cannot be used for predicate logic, as we will see. To evaluate the truth value of a formula (i.e. determining whether it is a tautology, a truth, a falsehood or a contradiction), it is preferable to use transformations that modify the formula while preserving its truth value, until we obtain a simple formula whose truth status is known. The rest of this chapter consists of a presentation of these transformations that preserve truth values. The technical study of these transformations takes us away from the semantic aspect of logic (applying valuations and reading truth tables) and brings us closer to the syntactic perspective (the art of modifying the form of formulas independently of their truth status which remains unchanged).

The basic principle consists in using the replacement theorem.

If F(P) is a propositional formula with zero, one or several occurrences of symbol P, then:

Replacement Theorem

if (X ≡ Y) is a tautology, then (F(X) ≡ F(Y)) is a tautology as well.

This theorem may sound obvious. It serves however as basis for the syntactic processing of formulas in Logic, mathematics and automated theorem proving. If (X ≡ Y) is a tautology, then v(X) = v(Y) for any valuation v. In other words, nothing can distinguish X and Y from the point of view of their truth value. The replacement theorem then shows its interest: F(X) and F(Y) have the same truth value as well. One can then replace X by Y in F without changing the truth conditions. The formula has changed, but not its truth value. Thanks to this replacement, we can identify which transformations will preserve truth values when acting on propositional formulas.

Let’s note S ⊨ X the propositional consequence: if a valuation assigns the value T to all element of S, then it will assign T to X (note that what is to the left of the consequence sign ⊨ is a set, and what is to the right is a proposition).
⊨ X denotes the fact that X is a tautology.

The deduction theorem constitutes a further means to "syntactize" logical proofs (i.e. replace truth tables by formal operations).

The basic tool to perform truth-preserving formal transformations is a set of equivalences between basic formulas. For instance, (X ⊃ Y)) and (¬X ∨ Y) are equivalent (i.e. their equivalence is a tautology, i.e. they have the same truth value). To put some order before considering proof automation, one can use a set of basic equivalences to convert any formula into an equivalent formula which is in standard form.

The conjunctive normal form (CNF) rewrites any propositional formula as a conjunction of clauses.
A clause is noted [a, b, c].
A clause represents the disjunction of its terms, which are propositional symbols possibly with negation.

This is the system used by Prolog. Note that clauses are not part of the logic language. They are just rewriting tools used within a proof.

A conjunction of clauses is noted < C1, C2, C3 >. So, formula : (a ⊃ ¬(b ⊃ c)) will be rewritten as: < [¬a, b], [¬a, ¬c] >. A propositional formula is in conjunctive normal form if it is written as a conjunction of clauses : < C1, C2, ... Cn > where each C_i is a clause. Note that a CNF is not a formula of the propositional language. This is not a problem, as it is done for the purpose of proof processing. What is important is that truth values be preserved. To allow this, the power of valuations v is extended in the following way:

v([X₁, X₂, ... X_n ]) = F iff v(X_i) = F for all i

v(< C₁, C₂, ... C_m >) = T iff v(C_i) = T for all i

These definitions naturally extend to the empty clause: v([ ]) = F, and to the empty conjunction: v(< >) = T.

The following tables show how to transform the binary connectives of propositional Logic. Conjunctive formulas, called here α-Formulas, are such that α anf < α₁, α₂ > have the same truth value. Disjunctive formulas, called here β-Formulas, are such that β and [β₁, β₂] have the same truth value. These tables are useful: they are used to replace all connectives by rewriting them as conjunctions and disjunctions.

α	α1	α2
(X ∧ Y)	X	Y
¬(X ∨ Y)	¬X	¬Y
¬(X ⊃ Y)	X	¬Y
¬(X ⊂ Y)	¬X	Y
¬(X ↑ Y)	X	Y
(X ↓ Y)	¬X	¬Y
(X ⊅ Y)	X	¬Y
(X ⊄ Y)	¬X	Y

                                                [ only the greyed lines are to be remembered ]

β	β1	β2
(X ∨ Y)	X	Y
¬(X ∧ Y)	¬X	¬Y
(X ⊃ Y)	¬X	Y
(X ⊂ Y)	X	¬Y
(X ↑ Y)	¬X	¬Y
¬(X ↓ Y)	X	Y
¬(X ⊅ Y)	¬X	Y
¬(X ⊄ Y)	X	¬Y

The algorithm that converts a propositional formula into CNF proceeds step by step. Basic transitions are:

• replace < ... [ ... β ...] ... >    by    < ... [ ... β₁, β₂ ...] ... >
• replace < ... [ ... α ...] ... >    by    < ... [ ... α₁ ...], [ ... α₂ ...] ... >
• replace < ... [ ... ¬¬α ...] ... >    by    < ... [ ... α ...] ... >

For instance, the steps for converting (a ⊃ ¬ (b ⊃ c)) into CNF are the following ones:

<[(a ⊃ ¬(b ⊃ c))]>        Starting from a "conjunction" with only one clause which has only one term.
<[¬a, ¬(b ⊃ c)]>        third β-rule
<[¬a, b], [¬a, ¬c]]>    third α-rule and second transition.

• Propositional logic at CMU
• Resolution Theorem Proving: Propositional Logic (MIT)
• Univ. of Edinburgh (Tutorial 1    Tutorial 2    Tutorial 3    Tutorial 4)

            

Back to the main page