Proofs by Program Transformations

Abhik Roychoudhury, K. Narayan Kumar, C. R. Ramakrishnan, I. V. Ramakrishnan

Abstract:
Logic program transformation systems are often described as a collection of unfolding, folding and goal replacement transformation rules. Unfold/fold logic program transformation systems have been extensively used for program synthesis and program optimization. However, relatively little work has been done on using such systems for constructing proofs. In this paper, we examine how unfolding, folding and goal replacement transformations can be used towards automating the construction of such induction proofs.

Bibtex Entry:

@inproceedings{RKRR:LOPSTR99,
author = {Abhik Roychoudhury and  K. Narayan Kumar and  C. R. Ramakrishnan and  I. V. Ramakrishnan},
title = {Proofs by Program Transformations},
booktitle = {Ninth International Workshop on Logic-based Program Synthesis and
	Transformations ({LOPSTR})},
address = {Venice, Italy},
year = {1999}
}

Full Paper: [pdf]

Home | Papers

C. R. Ramakrishnan
(cram@cs.sunysb.edu)