Automatic inductive theorem proving using Prolog (Q1103415)
From MaRDI portal
![]() | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: Automatic inductive theorem proving using Prolog |
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
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