Automatic inductive theorem proving using Prolog
type: Item
instance of: scholarly article
title: Automatic inductive theorem proving using Prolog
zbMATH Open document ID: 0645.68095
DOI: 10.1016/0304-3975(87)90016-8
author: Jieh Hsiang
author: Mandayam Srivas
published in: Theoretical Computer Science
publication date: 1987-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 4053060
zbMATH Keywords: inductive theory
zbMATH Keywords: theorem-proving
zbMATH Keywords: Prolog
zbMATH Keywords: first order theory
zbMATH Keywords: Horn clause
zbMATH Keywords: Skolemization
zbMATH Keywords: evaluation
zbMATH Keywords: term rewriting
zbMATH Keywords: program development
zbMATH Keywords: verification
MaRDI profile type: Publication
full work available at URL: 0304-3975(87)90016-8
OpenAlex ID: W2053332596
cites work: Q3894958
cites work: Q3919057
cites work: Q3725518
cites work: Q3880309
cites work: Refutational theorem proving using term-rewriting systems
cites work: Q3783512
cites work: Q3725520
cites work: Q3709891
cites work: Q5581665
cites work: Q3690200
cites work: New decision algorithms for finitely presented commutative semigroups
cites work: Making prolog more expressive
cites work: The occur-check problem in Prolog
Recommended article: Q3732983
Recommended article: Automating Inductive Proofs Using Theory Exploration
Recommended article: Q3781734
Recommended article: Q3345810
Recommended article: Q4269904
Recommended article: Automated verification of Prolog programs
Recommended article: Automated theorem proving and logic programming: a natural symbiosis
Recommended article: Q3977980
Recommended article: Q4934147
Recommended article: Automated theorem proving by test set induction
description: scientific article; zbMATH DE number 4053060