Transformational reasoning with incomplete information

Transformational reasoning with incomplete information,O. Celiku,J. von Wright

Transformational reasoning with incomplete information  
BibTex | RIS | RefWorks Download
Starting a proof without having complete information about the proof term can be beneflcial. While the proof is carried out newly introduced constraints can make the information more precise. Window inference, a proof paradigm based on hierarchical term rewriting, is very well suited for general transformational reasoning and especially for rea- soning about programs. The HOL implementation of window inference does not support proofs with uninstantiated terms since the HOL system does not have a formalized metalogic. We show how, without having to redo proofs, higher order variables (metavariables) can be used to per- form proofs with uninstantiated terms in HOL window inference. We illustrate the uses of metavariables with a few examples related to pro- gram reasoning.
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.