Guiding Program Development Systems by a Connection Based Proof Strategy.
Christoph Kreitz, Jens Otten, Stephan Schmitt.
In M. Proietti, ed., 5th International Workshop on Logic Program Synthesis and Transformation (LoPSTr'95), LNCS 1048, pp. 137-151, Springer Verlag, 1996.
Abstract
	We present an automated proof method for constructive logic based on Wallen's matrix characterization for intuitionistic validity. The proof search strategy extends Bibel's connection method for classical predicate logic. It generates a matrix proof which will then be transformed into a proof within a standard sequent calculus. Thus we can use an efficient proof method to guide the development of constructive proofs in interactive proof/program development systems.
Also presented at Max-Plack Institut für Informatik (MPI), Saarbrücken, Germany, June 1995.

		Paper is available in postscript and pdf format		Slides of the conference presentation are available in compressed postscript and pdf format
Bibtex Entry					Back to overview of papers
	@InProceedings{inp:KreitzOttenSchmitt96a, author = "Christoph Kreitz and Jens Otten and Stephan Schmitt", title = "Guiding Program Development Systems by a Connection Based Proof Strategy", booktitle = "Fifth International Workshop on Logic Program Synthesis and Transformation", year = 1996, editor = "M. Proietti", volume = 1048, series = "Lecture Notes in Computer Science", pages = "137--151", publisher = "Springer Verlag" }