Automatic inductive theorem proving using Prolog (Q1103415)

From MaRDI portal





scientific article
Language Label Description Also known as
English
Automatic inductive theorem proving using Prolog
scientific article

    Statements

    Automatic inductive theorem proving using Prolog (English)
    0 references
    0 references
    0 references
    1987
    0 references
    The paper describes a theorem-proving method based on Prolog. The method is used for proving universally quantified propositions in first order theory. The proposition must be in the form of a Horn clause in which the consequence is an equality predicate. The authors give a detailed description of three new mechanisms: Skolemization by need, suspended evaluation, limited forward chaining. The power of the method is illustrated by proving inductive properties of Prolog programs. Functional and algorithmic descriptions of the prover are included. The present inductive theorem proving method is compared with the term rewriting method and the Boyer-Moore method. Finally, the authors shortly describe how the method can be used for program development and verification.
    0 references
    inductive theory
    0 references
    theorem-proving
    0 references
    Prolog
    0 references
    first order theory
    0 references
    Horn clause
    0 references
    Skolemization
    0 references
    evaluation
    0 references
    term rewriting
    0 references
    program development
    0 references
    verification
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references

    Identifiers