The semantics of answer literals (Q1357665)

The technique of answer literals is well known in resolution and is usually presented as a trick for keeping track of the variable bindings. For Horn clause sets this technique produces the one-literal answer. Non-Horn examples may produce disjunctive answers. The answer literal technique can be used with other resolution-based methods, such as paramodulation. The author gives a simple semantic explanation of the answer literal method that is not tied to resolution at all. Thus, answer literals could just as well be used with any other proof procedure, such as tableau-based systems, which have been advocated as an alternative to resolution. The specifics of the deductive system come in only when we consider the issues of soundness and completeness. Completeness for a resolution procedure means only refutational completeness; this does not necessarily imply that every answer clause that follows from an axiom will be derived. The author discusses also the difference between soundness and refutational soundness. In the last sections, the author illustrates the previous discussion with two classes of examples obtained using the resolution theorem-prover OTTER (Mc Cune's system). The author shows how to use OTTER to produce all answers to a given equation; i.e., OTTER proves from an algebraic theory that a solution of an equation exists, and then uses the answer literal to retrieve the solution. In the second class, the author shows how to solve an inequation and tries to pin down which instances of a rule are needed to prove a given fact.