Computational Logic in Plain English
Computational logic concerns automated techniques for solving problems in logic. A Sudoku is a simple and familiar logic puzzle. Its rules are precise: we can check whether a claimed solution is correct with no room for argument. A Sudoku can be encoded as a huge logical formula, and standard computational logic software can easily find the solution.
A another example of a logic problem is to present a chess position, asking whether White has a winning move: precisely, that no matter how Black replies, White has a further winning move and Black cannot put off defeat forever. A chess problem is much more complicated than a Sudoku, because the number of possibilities could be astronomical. Such problems are generally infeasible unless White can force checkmate in a few moves. It isn't enough to say “this wins Black's Queen” because there are plenty of situations where somebody can lose their Queen and still win the game. Computers are certainly better than people at solving chess problems, though this is done using specialised chess software.
Solving puzzles is a mere pastime, but plenty of real-life problems can be expressed using logic. A classic one is timetabling, where you have teachers, classrooms, subjects and students. At any time during the school day, a teacher should be in a classroom, students need to be in classrooms, students need to attend classes in each of their subjects, but you can't ask somebody to be in two places at one time, and you can't have two different teachers in the same classroom. This sort of situation resembles a Sudoku.
Where computational logic especially pays off is in the design of computer systems themselves. Computers and their software are extremely complicated, and it is impossible to eliminate all the errors in their designs by testing. As a result, computers crash and can be hacked into, and people regularly have to download updates to fix bugs. Computer software is the one consumer product for which there are no warranties.
Computer system designs can be coded in logic, and many properties of software can also be deduced logically. The desired behaviour of these designs can be expressed mathematically, which also brings it within the scope of logic. A great variety of tools are available to validate different aspects of computer designs, including processor chips and device drivers. They are already yielding benefits in improved reliability, though we have a long way to go.
My own speciality includes interactive theorem proving, where a user interacts with a tool in order to set up mathematical models, and then to prove desired properties. A precise language of mathematical formulas is used, with strict rules to ensure that only logically valid formulas (“theorems”) can be produced. I also work on automatic theorem proving, where a formula is simply given to a piece of software, and if you are lucky, a proof emerges in a couple of seconds.
You may also want to look at my recent survey of the subject, published as Computational Logic: Its Origins and Applications. Proceedings of the Royal Society Series A (2018) also availble from the Royal Society's website.
This article take a fairly broad view of logic and then focusses specifically on some of my work.
Lawrence C. Paulson • Computer Laboratory • University of Cambridge