Abstract
We develop methods for proving the fairness and correctness properties of rule based completion strategies by means of process logic. The concepts of these properties are formulated generally within process logic and then concretized to rewrite system theory based on transition rules. We develop in parallel the notions of success and failure of a completion strategy, necessary to support the proves of the cited properties. Finally we show the necessity of another property, called justice, in the analysis of completion strategies.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
L. Bachmair. Proof methods for equational theories. PhD thesis, University of Illinois, Urbana Champaign, Illinois, 1987.
L. Bachmair, N. Dershowitz, and J. Hsiang. Orderings for equational proofs. In Proceedings 1st IEEE Symposium on Logic in Computer Science, Cambridge, MA, pages 346–357, June 1986.
N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science B: Formal Methods and Semantics, chapter 6. North-Holland, Amsterdam, 1990.
M.J. Fischer and R.E. Ladner. Propositional dynamic logic of regular programs. Journal of Computer and System Science, 18:194–211, 1979.
N. Francez. Fairness. Springer Verlag, 1986.
D. Gabbay, A. Pnueli, S. Shelah, and J. Stavi. On the temporal analysis of fairness. In Proceedings of the 7th ACM Symposium on POPL, Las Vegas, pages 163–173, January 1980.
M. Hermann. On proving properties of completion strategies. Research report 90-R-149, Centre de Recherche en Informatique de Nancy, 1990.
D. Harel, D. Kozen, and R. Parikh. Process logic: Expressiveness, decidability, completeness. Journal of Computer and System Science, 25:144–170, 1982.
J.Y. Halpern and J.H. Reif. The propositional dynamic logic of deterministic, well-structured programs. Theoretical Computer Science, 27:127–165, 1983.
G. Huet. A complete proof of correctness of the Knuth-Bendix completion algorithm. Journal of Computer and System Science, 23(1):11–21, August 1981.
D.E. Knuth and P.B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263–297. Pergamon Press, Oxford, 1970.
F. Kröger. Temporal logic of programs, volume 8 of EATCS Monographs on Theoretical Computer Science. Springer Verlag, 1987.
Z. Manna and A. Pnueli. How to cook a temporal proof system for your pet language. In Proceedings of the 10th ACM POPL Symposium, Austin, TX, pages 141–154, 1983.
J.P. Queille and J. Sifakis. Fairness and related properties in transition systems — A temporal logic to deal with fairness. Acta Informatica, 19:195–220, 1983.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hermann, M. (1991). On proving properties of completion strategies. In: Book, R.V. (eds) Rewriting Techniques and Applications. RTA 1991. Lecture Notes in Computer Science, vol 488. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-53904-2_113
Download citation
DOI: https://doi.org/10.1007/3-540-53904-2_113
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-53904-9
Online ISBN: 978-3-540-46383-2
eBook Packages: Springer Book Archive