Formulation of induction formulas in verification of prolog programs

Tadashi Kanamori, Hiroshi Fujita

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

12 Citations (Scopus)

Abstract

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
Pages281-299
Number of pages19
ISBN (Print)9783540167808
DOIs
Publication statusPublished - Jan 1 1986
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

Other

Other8th International Conference on Automated Deduction, 1986
CountryUnited Kingdom
CityOxford
Period7/27/868/1/86

Fingerprint

Prolog
Proof by induction
LISP (programming language)
Formulation
Semantics
Specifications
Program Transformation
Fixpoint
Equivalence
Specification
First-order

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Kanamori, T., & Fujita, H. (1986). Formulation of induction formulas in verification of prolog programs. In J. H. Siekmann (Ed.), 8th International Conference on Automated Deduction - Proceedings (pp. 281-299). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 230 LNCS). Springer Verlag. https://doi.org/10.1007/3-540-16780-3_97

Formulation of induction formulas in verification of prolog programs. / Kanamori, Tadashi; Fujita, Hiroshi.

8th International Conference on Automated Deduction - Proceedings. ed. / Jorg H. Siekmann. Springer Verlag, 1986. p. 281-299 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 230 LNCS).

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

Kanamori, T & Fujita, H 1986, Formulation of induction formulas in verification of prolog programs. in JH Siekmann (ed.), 8th International Conference on Automated Deduction - Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 230 LNCS, Springer Verlag, pp. 281-299, 8th International Conference on Automated Deduction, 1986, Oxford, United Kingdom, 7/27/86. https://doi.org/10.1007/3-540-16780-3_97
Kanamori T, Fujita H. Formulation of induction formulas in verification of prolog programs. In Siekmann JH, editor, 8th International Conference on Automated Deduction - Proceedings. Springer Verlag. 1986. p. 281-299. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/3-540-16780-3_97
Kanamori, Tadashi ; Fujita, Hiroshi. / Formulation of induction formulas in verification of prolog programs. 8th International Conference on Automated Deduction - Proceedings. editor / Jorg H. Siekmann. Springer Verlag, 1986. pp. 281-299 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{ab623d1555834798b0933430b79ddaa4,
title = "Formulation of induction formulas in verification of prolog programs",
abstract = "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.",
author = "Tadashi Kanamori and Hiroshi Fujita",
year = "1986",
month = "1",
day = "1",
doi = "10.1007/3-540-16780-3_97",
language = "English",
isbn = "9783540167808",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "281--299",
editor = "Siekmann, {Jorg H.}",
booktitle = "8th International Conference on Automated Deduction - Proceedings",
address = "Germany",

}

TY - GEN

T1 - Formulation of induction formulas in verification of prolog programs

AU - Kanamori, Tadashi

AU - Fujita, Hiroshi

PY - 1986/1/1

Y1 - 1986/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=0346547847&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0346547847&partnerID=8YFLogxK

U2 - 10.1007/3-540-16780-3_97

DO - 10.1007/3-540-16780-3_97

M3 - Conference contribution

AN - SCOPUS:0346547847

SN - 9783540167808

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 281

EP - 299

BT - 8th International Conference on Automated Deduction - Proceedings

A2 - Siekmann, Jorg H.

PB - Springer Verlag

ER -