Issues for automated deduction

The following basic observations provide the background to the comments:

• The satisfiability of a propositional formula is equivalent to the non-validity of its negation: this establishes a direct semantic link between satisfiability and validity.
• The fact that the satisfiability and validity can be determined by inspecting the truth table means that this determination is decidable i.e. it can be solved by an algorithm.
• If a propositional formula is in a particular form, deciding satisfiability or validity may be computationally efficient. For instance, you can check the validity of a formula in conjunctive normal form easily - it is sufficient that every disjunction clause contains a literal and its negation, so that the disjunction evaluates to true. In a dual fashion, you can check the satisfiability of a propositional formula in disjunctive normal form quite efficiently: you need only check that there is at least one conjunctive clause that doesn't contain a literal and its negation.
• From a computational perspective, the challenging situations concern determining the satisfiability of a propositional formula in conjunctive normal form or the validity of a formula in disjunctive normal form. Any given propositional formula can be transformed into all kinds of different CNF - examples include Horn clause CNF, 2-CNF and 3-CNF. Certain special variants of CNF enable satisfiablity to be decided efficiently, but in general deciding whether a propositional formula in CNF is satisfiable is NP-complete (hence most probably not soluble in polynomial time).

Because even the problem of deciding satisfiability of a formula in propositional logic is computationally complex, all approaches to automated deduction suffer from some limitations. Example issues - closely interconnected - include:

• Formulae may have to be transformed into a normal form. Checking the satisfiability in the normal form may be relatively simple, but the process of transformation will then be costly. For instance, every propositional formula is semantically equivalent to a Horn formula, but the transformation is computationally expensive.
• The satisfiability techniques may work efficiently for formulae of a particular form (e.g. expressed as a Horn formula, 2-CNF formula), but there are cases in which they fail. See the discussion of SAT solvers in Huth and Ryan section 1.6.
• The algorithms that have to be applied cease to be conceptually simple, as a mathematician or logician would ideally like them to be; pragmatic and ad hoc techniques have to be introduced to avoid problems such as infinite loops. This has been a significant issue for logic programming languages such as Prolog, where it proves necessary to introduce notions such as cuts to ensure that searches terminate, and this detracts from the logical integrity of the deductive process.
• The link between the informal semantics in the problem domain and the logical formulation of a problem for automated reasoning can be obscure, and the results of automated reasoning are difficult to interpret in terms that a human observer can understand. For instance, advanced computer chess programs can beat human chess players, but the techniques they use do not necessarily translate into human-uasable chess knowledge.