Formulation of induction formulas in verification of prolog programs

Tadashi Kanamori, Hiroshi Fujita

Research output: Chapter in Book/Report/Conference proceedingConference contribution

14 Citations (Scopus)


How induction formulas are formulated in verification of Prolog programs is described. The same problem for well-founded induction was investigated by Boyer and Moore in their verification system for terminating LISP programs (BMTP). The least fixpoint semantics of Prolog provides us with the advantages that computational induction can be easily applied and can generate simpler induction schemes. We investigate how computational induction is applied to a class of first order formulas called S-formulas, in which specifications in our verification system are described. In addition, we show how equivalence preserving program transformation can be utilized to merge induction schemes into a simpler one when more than two induction schemes are suggested.

Original languageEnglish
Title of host publication8th International Conference on Automated Deduction - Proceedings
EditorsJorg H. Siekmann
PublisherSpringer Verlag
Number of pages19
ISBN (Print)9783540167808
Publication statusPublished - Jan 1 1986
Externally publishedYes
Event8th International Conference on Automated Deduction, 1986 - Oxford, United Kingdom
Duration: Jul 27 1986Aug 1 1986

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume230 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other8th International Conference on Automated Deduction, 1986
Country/TerritoryUnited Kingdom

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Formulation of induction formulas in verification of prolog programs'. Together they form a unique fingerprint.

Cite this