Artificial intelligence is a field that combines different methods and approaches to imitate human thought processes, which a computerized system can replicate. The rapid progress we have observed in recent years in this field is driven by the growing computing power, the abundance of extensive datasets, and the ongoing research and development of advanced algorithms.

With advancements in AI, it has become possible to address various challenges and transform multiple sectors, including finance, industrial production, healthcare, and autonomous driving. This ongoing process will undoubtedly lead to a significant change in our society, reshaping our work patterns, social interactions, and overall engagement with the world.

Let’s delve into the world of AI and understand how machines think. This exploration takes us to the intersection mathematics, computer science, and cognitive psychology. To find answers, we need to understand the basic principles that govern human reasoning. These principles include symbolic processing (where machines understand symbols and their relationships), knowledge representation (how machines store and use information), and logical inference (how machines draw conclusions from available information). By understanding these concepts, we can develop new and innovative approaches to help machines analyze, understand, and solve increasingly complex problems.


The Role of Logic

The subject we are about to explore is quite intricate and multi-layered. As a result, I want to present a simple example that breaks down how a machine thinks and deduces based on logical principles. These principles have been crucial in advancing artificial intelligence, especially knowledge representation and automated reasoning in expert systems.

Logic is the study of reasoning forms that systematically investigates the connection between premises and valid conclusions. The basic principle of reasoning is that if the premises are true, then the conclusions must necessarily follow. This principle is known as the principle of truth, underlining the logical coherence that characterizes a valid argument. Here’s an example of correct reasoning:

If it rains, then I take the umbrella. It’s raining, so I take the umbrella.

In formal terms, this reasoning can be generalized as follows:

\[ \frac{A \rightarrow B, \quad A}{B} \tag{1}\]

If \(A\), Then \(B\). It happens \(A\), so \(B\) occurs.

This statement is false only when the premise \(A\) is false. If we represent the truth table of logical implication, we have:

\begin{array}{|c|c|c|} \hline A & B & A \rightarrow B \\ \hline T & T & T \\ T & F & F \\ F & T & T \\ F & F & T \\ \hline \tag{2} \end{array}

Propositional logic examines the meaning of logical words used to connect propositions, such as not \( \neg \), and \( \land \), or \( \lor \), if…then \( \rightarrow \), and if and only if \( \leftrightarrow \), to determine the validity of inferences. For those with even a basic understanding of programming fundamentals, these notions will undoubtedly be familiar, making it clear how a formal representation of this kind allows for the automation of simple reasoning processes through algorithms.

Propositional logic has its own syntax and semantics.

  • The syntax describes what a propositional language is: \[\text{Prop}[P], \quad P = \lbrace p, q, r, \ldots \rbrace \tag{3} \] Where \(p,q,r\) are called propositional variables, or atomic statements (for example, “it’s raining”).

  • The semantics allows to give meaning to expressions formed through the propositional language, which in propositional logic can be true or false. In formal terms, the interpretation domain of propositional logic is: \[ Bool = \lbrace T,F \rbrace \tag{4}\] where interpretation refers to a function such that for every interpretation \(M\) of \(P\), we have \[ M:P\rightarrow Bool \tag{5}\]

A proposition is considered to be a logical consequence of a set of premises only if it is true in every interpretation where all the premises are true. Without delving too much into theory, let’s see how it is possible to define automatic deduction algorithms that demonstrate the logical consequence of a set of premises, thus inferring new knowledge about the facts.


Method of Analytic Tableaux

There are various ways to show that a certain formula \(\varphi\) is a logical consequence of a knowledge base \(K\). One of these methods is the Tableaux method, which uses refutation to prove the same. Essentially, a tableau can be thought of as a tree that is developed through specific formulas called \(\alpha\) and \(\beta\), starting from the root. This allows the tree to be expanded at depth, and the method can be mechanically constructed.

The goal of the algorithm is to demonstrate that \(K \cup \lbrace \neg \varphi \rbrace\) is unsatisfiable.

Imagine having a simple proposition like “If the sky is cloudy, then it will rain, or we won’t have rain.” In formal terms, to make it understandable for a computer, it can be expressed as:

\[(\varphi \rightarrow \psi) \lor \neg \psi \tag{6}\]

We use the Tableau method to mechanically verify the validity of this formula by constructing the corresponding tree.


  • As the first step of the proof, we negate the formula to check if \(K \cup \lbrace \neg \varphi \rbrace\) is unsatisfiable. In this case, we only have the formula \(\varphi\), so we proceed to its negation: \[\neg((\varphi \rightarrow \psi) \lor \neg \psi )\]

  • The expression \(\neg(A \lor B )\) can be rewritten using the expansion rules \(\alpha\) as: \[\neg(\varphi \rightarrow \psi), \neg \neg \psi )\]

  • The expression \(\neg(A \rightarrow B )\) can be rewritten using the expansion rules \(\alpha\) as \(A, \neg B\). Thus, the formula becomes: \[\varphi, \neg \psi, \neg \neg \psi\]

  • By eliminating double negation for \(\psi\), we obtain the branch: \[\varphi, \neg \psi, \psi\]


A tableau branch closes when a contradiction like \(\psi, \neg \psi\) is reached. In our case, the branch can be considered closed. If all branches of a tableau are closed, then we have demonstrated the validity of our formula, as in this specific case.

We have demonstrated that the formula \(\neg ((\varphi \rightarrow \psi) \lor \neg \psi) \tag{6}\) is unsatisfiable, and therefore our initial formula can never be false and thus is valid.

Conclusions

Tableau algorithms have been an integral part of artificial intelligence since the 1960s, and have undergone significant advancements and improvements over time, expanding their scope and applicability. The example provided is a very simplistic model and only demonstrates how logical-mathematical formalism is a necessary prerequisite for understanding certain constructs by automated systems. If we narrow the focus to logic, there are different formal logics, much more potent in expressive power than propositional logic, that allow inference to be performed on much more complex knowledge bases and will be the subject of the next issue.

  • To delve deeper into the tableaux method, I recommend referring to the corresponding entry on WikiPedia.

  • For propositional logic, I suggest the article Propositional Logic on the Internet Encyclopedia of Philosophy.