The semantics of answer literals (Q1357665)

From MaRDI portal
Revision as of 09:15, 30 July 2024 by Openalex240730090724 (talk | contribs) (Set OpenAlex properties.)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
scientific article
Language Label Description Also known as
English
The semantics of answer literals
scientific article

    Statements

    The semantics of answer literals (English)
    0 references
    0 references
    12 January 1998
    0 references
    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.
    0 references
    answer literals
    0 references
    soundness
    0 references
    completeness
    0 references
    resolution theorem-prover OTTER
    0 references
    algebraic theory
    0 references
    solution of an equation
    0 references
    inequation
    0 references
    0 references

    Identifiers