For those new to automated reasoning. The primary objective of automated reasoning (which includes automated deduction and automated theorem proving) is to develop computer programs that use logical reasoning for the solution of a wide variety of problems, including open questions. The book Automated Reasoning and Its Applications was written in honor of Larry Wos, one of the founders of the field. Wos played a central role in forming the "culture" of automated reasoning at Argonne National Laboratory. He and his colleagues consis¬tently seek to build systems that search huge spaces for solutions to difficult problems and proofs of significant theorems. They have had numerous notable successes. The contributors are among the world’s leading researchers in automated reasoning. Their essays cover the theory, software system design, and use of these systems to solve real problems.
What do the following three puzzles have in common?
There are twelve billiard balls, eleven of which are identical in weight. The remaining ballthe odd onehas a different weight. You are not told whether it is heavier or lighter. You have a balance scale for weighing the balls. Can you find which ball is the odd ball in three weighings, and can you also find out whether it is lighter or heavier than the others?
There are three missionaries and three cannibals on the west bank of a river. There is a boat on the west bank that can hold no more than two people. The missionaries wish to cross to the east bank. But they have a problem: If on either bank the cannibals ever outnumber the missionaries, those missionaries will be eaten. Is there a way for the missionaries to get their wishto get to the east bank without losing anyone?
There is a checkerboard whose upper left and lower right squares have been removed. There is a box of dominoes that are one square by two squares in size. Can you exactly cover the checkerboard with the dominoes?
Again, what is common to the three problems? The answer is: They can each be solved with reasoninglogical reasoning. And the answer also is: They have all been solved with the same computer program.
