Automatic inductive theorem proving using Prolog

DOI10.1016/0304-3975(87)90016-8zbMath0645.68095OpenAlexW2053332596MaRDI QIDQ1103415

Mandayam Srivas, Jieh Hsiang

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

verificationevaluationterm rewritingPrologHorn clauseprogram developmentfirst order theoryinductive theorySkolemizationtheorem-proving

Mathematics Subject Classification ID

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

Cites Work

• Refutational theorem proving using term-rewriting systems
• The occur-check problem in Prolog
• New decision algorithms for finitely presented commutative semigroups
• Making prolog more expressive
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item