• TUCS Publication Series
• How to Publish in TUCS Series
• Publication Search
• Publication Graph
• Publication Input
• Publication Input Guide
• JuFo Browser

Transformational Reasoning with Incomplete Information

Orieta Celiku, Joakim von Wright, Transformational Reasoning with Incomplete Information. In: TPHOLs 2001: Supplemental Proceedings, Informatics Report Series, University of Edinburgh, Division of Informatics, 2001.

Abstract:

Starting a proof without having complete information about the proof
term can be beneficial. 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 reasoning 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 perform proofs with
uninstantiated terms in HOL window inference. We illustrate the uses of
metavariables with a few examples related to program reasoning.

Files:

Abstract in PDF-format

BibTeX entry:

@INPROCEEDINGS{pCevo01a,
  title = {Transformational Reasoning with Incomplete Information},
  booktitle = {TPHOLs 2001: Supplemental Proceedings},
  author = {Celiku, Orieta and Wright, Joakim von},
  series = {Informatics Report Series},
  publisher = {University of Edinburgh, Division of Informatics},
  year = {2001},
  keywords = {Metavariables, Window Inference, HOL },
}

Edit publication