@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 = jan,
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",
note = "8th International Conference on Automated Deduction, 1986 ; Conference date: 27-07-1986 Through 01-08-1986",
}