Automatic inductive theorem proving using Prolog

DOI10.1016/0304-3975(87)90016-8MaRDI QIDQ1103415zbMATH OpenOpenAlexFDO

Authors Jieh Hsiang, Mandayam Srivas

Publication date 1987

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(87)90016-8

zbMATH Keywords

evaluationfirst order theoryHorn clauseinductive theoryprogram developmentPrologSkolemizationterm rewritingtheorem-provingverification

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Specification and verification (program logics, model checking, etc.) (68Q60)

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.

Recommendations

• scientific article; zbMATH DE number 3965464
• Automating Inductive Proofs Using Theory Exploration
• scientific article; zbMATH DE number 4043814
• scientific article; zbMATH DE number 3880144
• scientific article; zbMATH DE number 1360950
• Automated verification of Prolog programs
• Automated theorem proving and logic programming: a natural symbiosis
• scientific article; zbMATH DE number 13446
• scientific article; zbMATH DE number 1389654
• Automated theorem proving by test set induction

Cites work

• scientific article; zbMATH DE number 3913659 (Why is no real title available?)
• scientific article; zbMATH DE number 3938563 (Why is no real title available?)
• scientific article; zbMATH DE number 3956406 (Why is no real title available?)
• scientific article; zbMATH DE number 3956408 (Why is no real title available?)
• scientific article; zbMATH DE number 4047053 (Why is no real title available?)
• scientific article; zbMATH DE number 3684925 (Why is no real title available?)
• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• scientific article; zbMATH DE number 3731310 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• Making prolog more expressive
• New decision algorithms for finitely presented commutative semigroups
• Refutational theorem proving using term-rewriting systems
• The occur-check problem in Prolog

Cited in

(13)

• A Prolog technology theorem prover: A new exposition and implementation in Prolog
• Inductive theorem proving based on tree grammars
• scientific article; zbMATH DE number 3935002 (Why is no real title available?)
• scientific article; zbMATH DE number 3965463 (Why is no real title available?)
• scientific article; zbMATH DE number 3965464 (Why is no real title available?)
• scientific article; zbMATH DE number 3986670 (Why is no real title available?)
• Automatic Learning of Proof Methods in Proof Planning
• Logic Programming with Graph Automorphism: Integratingnautywith Prolog (Tool Description)
• Some observations on the logical foundations of inductive theorem proving
• scientific article; zbMATH DE number 3995084 (Why is no real title available?)
• Automating Inductive Proofs Using Theory Exploration
• The applicability of logic program analysis and transformation to theorem proving
• Logic Based Program Synthesis and Transformation

This page was built for publication: Automatic inductive theorem proving using Prolog

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1103415)