1. Introduction
In this tutorial, we’ll go through the subject of automated reasoning and understand which type of problems we can solve using it. In the process, we’ll discuss the use cases for automated reasoning and the tools and techniques it offers for problem-solving.
2. What Is Automated Reasoning?
Reasoning is an inherent ability of human beings that refers to thinking about something logically and sensibly. It involves applying logic consciously by concluding new or existing information to seek the truth. There are many types of reasoning, like inductive reasoning and deductive reasoning.
Deductive reasoning is what we apply commonly in our everyday life. Here, we seek the most likely explanation from a set of observations. For instance, “In Monsoon it rains, and because it’s Monsoon already it will probably rain”:
Now, reasoning is largely a manual process performed by humans. But, what if we can automate it? Automated reasoning is concerned with building computing systems that automate this process. Hence, the goal is to mechanize different forms of reasoning.
For instance, automated reasoning finds effective usage in mechanical theorem proving. Here, an automated reasoning program implements an algorithmic description of a formal calculus so that it can efficiently prove theorems of the calculus.
To develop such a program, we need to define the class of problem we intend to solve and the language to represent the provided as well as the inferred information. We also need to specify the mechanism for the program to conduct deductive inferences.
3. Techniques in Automated Reasoning
An important part of building an automated reasoning program is the selection of deduction calculus. This is what the program uses to perform its inferences. Now, since logic is one of the oldest fields of study, the options here are quite varied.
But, essentially the choice depends on the nature of the problem domain. For instance, first-order logic is used for general-purpose theorem proving and program verification, and higher-order logic is used for hardware verification and mathematics.
3.1. First-order Logic
First-order logic (FOL) or predicate calculus is a collection of formal systems. FOL extends from propositional logic and uses quantified variables. The foundations of FOL were developed independently by Gottlob Frege and Charles Sanders Peirce.
There are two key parts of FOL, syntax and semantics. The syntax determines which finite sequences of symbols are well-formed expressions. The semantics determine the meaning behind these expressions. The key components of FOL include predicates and quantification:
The language of FOL is completely formal and hence it can be mechanically determined whether the given expression is well formed. It comprises terms and formulas which are strings of symbols, where all the symbols together form the alphabet of the language.
FOL is the standard for the formalization of mathematics into axioms. There are many deductive systems for FOL which are both sound and complete. Hence, it finds much application in automated theorem proving with many tools available, like Vampire.
3.2. Higher-order Logic
Higher-order logic (HOL) is a form of logic that distinguishes from FOL by additional quantifiers, and sometimes, stronger semantics. HOL features higher-order predicates, which are predicates of predicates or operations.
While FOL quantifies only variables that range over individuals, second-order logic also quantifies over sets, and third-order logic also quantifies over sets of sets. Here, HOL is the union of first, second, third, and similarly to nth-order logic:
HOL provides two possible semantics, standard and Henkin semantics. In standard semantics, quantifiers over higher-type objects range over all possible objects of that type. In Henkin semantics, a separate domain is included in each interpretation of each higher-order type.
HOL is inherently more expressive than FOL and is closer in spirit to actual mathematical reasoning. Many tools are available that use HOL, for instance, Isabelle is a higher-order logic theorem prover that provides a framework for the rapid prototyping of deductive systems.
4. Use Cases for Automated Reasoning
The idea of automating different forms of reasoning is quite exciting, but what may be the use of such an endeavor? As it appears, automated reasoning has very diverse applications in various fields across different industries. Most notable applications have been in computer science.
Automated reasoning is still largely a research-oriented field. The research continues to provide the necessary theoretical framework. With that, automated reasoning programs are increasingly being used to address open questions in mathematics and solve problems in engineering.
4.1. Mathematical Modeling
Since its introduction, one of the primary goals of automated reasoning has been the automation of mathematics. Here, the application of automated reasoning has been to discover new mathematical proofs or check existing ones for errors.
Typically mathematicians solve problems and verify mathematical proofs by using mathematical models. These models can rely on several variables to deduce probable solutions to a problem. Hence, using automated theorem provers can make this process highly scalable and efficient.
One of the earliest computer systems used to check the correctness of proofs was Automath devised by Nicolaas Govert de Bruijn in 1967. This has been superseded by more capable systems like the Mizar system started by Andrzej Trybulec in 1973.
4.2. Hardware Verification
Today, the scale and complexity at which hardware systems are produced is unprecedented. Moreover, the cost of defects in such hardware can be staggering. So, increasingly hardware manufacturers are turning towards more formal methods of hardware verification.
The microprocessor industry is finding the traditional ways of testing chip design insufficient. The idea behind using automated reasoning is to rigorously prove with mathematical certainty that the hardware system functions as specified.
Some of the common applications include formally establishing that the system functions correctly on all inputs, or that two different circuits are functionally equivalent. There are many automated formal verification techniques like SAT Solvers, Symbolic Simulation, and Model Checking.
4.3. Software Validation
With the increasing dependency of our lives on software systems, we must safeguard against malfunctioning software that can have dire consequences. Hence, it’s necessary to supplement traditional testing and validation methods with formal verification techniques.
For instance, automated theorem proving is being used for formal verification of security protocols. Security protocols like the Advanced Encryption Standard (AES) ensure that transactions take place securely over public networks. However, verification of such protocols is non-trivial.
The KeY tool, an interactive theorem-proving environment has been used to prove the properties of imperative and object-oriented sequential programs. It allows for full functional verification of sequential Java (with some limitations) and Java Card 2.2.x programs.
5. Advantages and Limitations of Automated Reasoning
As we’ve seen, automating different forms of reasoning has tremendous impact and value for us. It has marked advantages over traditional manual methods. Automated reasoning programs can handle larger and more complex problems that are too costly to handle manually.
Hence, automated reasoning brings increased efficiency, accuracy, and scalability. This leads to faster decision-making and problem-solving. Moreover, it’s less prone to errors resulting in more reliable results. We’re still realizing different applications for automated reasoning in the industry.
But, since automated reasoning is still in the early stages of evolution for practical applications, there are known limitations. First of all, automated reasoning applications require high computational resources and extensive domain knowledge to function effectively.
Further, automated reasoning programs may not always give interpretable or actional output. For instance, some problems involve ambiguity and uncertainty which require human intuition and creativity. But the ongoing research in this area is striving to make this better every day!
6. How Does It Relate to Artificial Intelligence?
As we hear many technical jargon daily, it’s worthwhile to understand how they relate to each other. But, before we do so, let’s quickly understand how automated reasoning started in the first place. As with many other fields, it’s difficult to pin a single date as the origin of automated reasoning.
However, the development of formal logic has been the catalyst for automated reasoning. Many believe the start to be early works like the Logic Theorist program by Newell, Shaw & Simon from 1955 and Martin Davis’ implementation of Presburger’s Decision Problem from 1954.
The Cornell Summer Meeting of 1957 gave rise to Automated Theorem Proving (ATP), now a subfield of automated reasoning. This development had a significant impact as it gave impetus to the development of computer science and also led to the development of Artificial Intelligence (AI).
Today, automated reasoning is a specific discipline within the general umbrella of artificial intelligence. AI is a field of research in computer science that enables computer systems to exhibit intelligence. It has many sub-disciplines like machine learning and deep learning.
One of the widely discussed AI technologies is Natural Language Processing (NLP). NLP focuses on training computers to understand written or verbal speeches. On the contrary, automated reasoning uses logical models and proofs to reason about the possible behaviors of a system.
7. Conclusion
In this tutorial, we understood the basics of automated reasoning, a sub-field of artificial intelligence in computer science. Then we discussed some of the core use cases that we’ve for automated reasoning as of today and the available tools and techniques to address them.