2023: The Year of The Artificial Intelligence
February 1, 2023
1982 – 1988
February 1, 2023Automated Reasoning
Introduction
Since the beginning of artificial intelligence, scientists have concurred that learning and reasoning about problems and solving them are fundamental pillars of intelligent behavior. Like many subfields of artificial intelligence, automated reasoning and machine learning have grown into highly specialized research areas.
Both have experienced the dichotomy between the ideal of imitating human intelligence, whereby the threshold of success would be the indistinguishability of human and machine and the idea that machines can and should learn and reason in their own way. According to the latter, the measure of success is independent of similarity to human behavior.(1)
Automated reasoning typically combines results and techniques of mathematical logic, theoretical computer science, algorithmics, and artificial intelligence. Some subareas of automated reasoning are automated theorem proving, interactive (or formal) theorem proving, and automated proof checking. Automated reasoning has applications in software and hardware verification, circuit design, logic programming, program synthesis, deductive databases, ontology reasoning, mathematical software, educational software, robotics, and planning, among others.
The modern history of automated reasoning is several decades old, but its roots go centuries or even millennia. For instance, Aristotle and ancient Greek philosophers tried to define forms of reasoning by syllogisms, aiming at formal deductive reasoning; on the other hand, Leibniz worked on reducing human reasoning to calculations within symbolic logic that could resolve differences of opinion. Leibniz’s dream motivated much of modern mathematical logic as well as automated reasoning. The modern history of automated reasoning started in the early 1950s, along with the first programmable computers, and with motivations and key challenges explained by Martin Davis: deductive reasoning, especially as embodied in mathematics, presented an ideal target for those interested in experimenting with computer programs that purported to implement the “higher” human faculties. (2)
Automated Reasoning in Propositional Logic
Propositional logic is the simplest part of mathematical logic, dealing with propositional variables, propositional constants (⊥, ⊤), and connectives (¬, ∧, ∨, ⇒, ⇔). Propositional logic has been studied (in some form) even in ancient Greece, while the major developments came with the work of Augustus DeMorgan and George Boole in the mid- 19th century. The first computer program — Logic Theorist — able to prove the theorem of propositional logic was created in 1956 by Allen Newell, Herbert Simon, and Clifford Shaw. The program was one of the very first to perform a task for which humans are credited with intelligence. (2)
Automated Reasoning in First-Order Logic
First-order logic (FOL) is more expressive than propositional logic — it allows the use of predicate and function symbols and quantification over variables. This expressiveness leads to undecidability — no procedure can decide whether an arbitrary first-order formula is valid. However, FOL is semi-decidable — some procedures can confirm (in a finite number of steps) if an arbitrary first-order formula is valid (if the formula is invalid, then these procedures only in some cases can detect that the formula is invalid, and otherwise they loop). (2)
Automated Reasoning in Higher-Order Logic and Interactive Theorem Proving
Skolem and Herbrand derived the first such semi-decision procedures in the 1920s and early 1930s, much before the first computers. Higher-order logic is more expressible than first-order logic as it admits several types of quantification. For instance, it is not only quantification over individual variables that are allowed, but also quantification over predicate and function symbols.
Conclusion
Over the years, automated reasoning transformed from a research field based on mathematical logic into a field that is a driving force for mathematical logic. Nowadays, automated reasoning tools are used in everyday practice in mathematics, computer science, and engineering. Based on the development of its properties, its role in education (both as a supporting tool and a subject matter) continues to increase. (2)