×

Constraint contextual rewriting. (English) Zbl 1039.68059

Summary: The effective integration of decision procedures in formula simplification is a fundamental problem in mechanical verification. In this paper we address the problem by proposing a general pattern of interaction between rewriting and decision procedures and by providing an account of such a pattern of interaction which is precise and concise at the same time. The first step amounts to a generalization of contextual rewriting which allows the available decision procedure to access and manipulate the rewriting context. We call this generalized form of contextual rewriting Constraint Contextual Rewriting (CCR for short). The second step amounts to providing a rule-based presentation of CCR which is modular, declarative, and formal at the same time. This allows us to give a rigorous account of CCR and to formally state and prove its soundness and termination.

MSC:

68Q42 Grammars and rewriting systems

Software:

OMRS; NQTHM; Tecton; STeP; RDL
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Armando, A.; Ballarin, C., Maple’s evaluation process as constraint contextual rewriting, (Mourrain, B., ISSAC-01, Proceedings of the 2001 International Symposium on Symbolic and Algebraic Computation. ISSAC-01, Proceedings of the 2001 International Symposium on Symbolic and Algebraic Computation, New York, July 22-25, 2001 (2001), ACM Press), 32-37 · Zbl 1356.68268
[2] Armando, A., Compagna, L., Ranise, S., 2001. RDL; Armando, A., Compagna, L., Ranise, S., 2001. RDL · Zbl 0988.68557
[3] Armando, A., Ranise, S., 1998. Constraint contextual rewriting. In: Caferra, R., Salzer, G. (Eds.), FTP’98, Proceedings of the 2nd International Workshop on First Order Theorem Proving, Vienna, Austria, November 23-25, pp. 65-75; Armando, A., Ranise, S., 1998. Constraint contextual rewriting. In: Caferra, R., Salzer, G. (Eds.), FTP’98, Proceedings of the 2nd International Workshop on First Order Theorem Proving, Vienna, Austria, November 23-25, pp. 65-75 · Zbl 1039.68059
[4] Armando, A.; Ranise, S., A practical extension mechanism for decision procedures: the case study of universal Presburger arithmetic, Journal of Universal Computer Science (Special Issue: Formal Methods and Tools), 7, 2, 124-140 (2001) · Zbl 0970.68110
[5] Baumgartner, P., Furbach, U., Petermann, U., 1992. A Unified Approach to Theory Reasoning. Technical Report, Inst. für Informatik (Koblenz); Baumgartner, P., Furbach, U., Petermann, U., 1992. A Unified Approach to Theory Reasoning. Technical Report, Inst. für Informatik (Koblenz)
[6] Bjørner, N.S., 1998. Integrating Decision Procedures for Temporal Verification. Ph.D. Thesis, Computer Science Department, Stanford University; Bjørner, N.S., 1998. Integrating Decision Procedures for Temporal Verification. Ph.D. Thesis, Computer Science Department, Stanford University
[7] Bjørner, N. S.; Stickel, M. E.; Uribe, T. E., A practical integration of first-order reasoning and decision procedures, (McCune, W., Proc. of the 14th International Conference on Automated Deduction. Proc. of the 14th International Conference on Automated Deduction, Townsville, Australia, July 13-17, 1997. Proc. of the 14th International Conference on Automated Deduction. Proc. of the 14th International Conference on Automated Deduction, Townsville, Australia, July 13-17, 1997, Lecture Notes Artificial Intelligence, vol. 1249 (1997), Springer-Verlag), 101-115 · Zbl 1430.03037
[8] Boyer, R. S.; Moore, J. S., Integrating decision procedures into Heuristic theorem provers: a case study of linear arithmetic, Machine Intelligence, 11, 83-124 (1988) · Zbl 0678.68091
[9] Coglio, A., Giunchiglia, F., Pecchiari, P., Talcott, C.L., 1997. A Logic Level Specification of the NQTHM Simplification Process. Technical Report, IRST; Coglio, A., Giunchiglia, F., Pecchiari, P., Talcott, C.L., 1997. A Logic Level Specification of the NQTHM Simplification Process. Technical Report, IRST
[10] Cyrluk, D.; Lincoln, P.; Shankar, N., On Shostak’s decision procedure for combinations of theories, (McRobbie, M. A.; Slaney, J. K., Proceedings of the 13th International Conference on Automated Deduction. Proceedings of the 13th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, vol. 1104 (1996), Springer-Verlag), 463-477 · Zbl 1415.03019
[11] Dershowitz, N.; Jouannaud, J. P., Rewriting systems, (Handbook of Theoretical Computer Science (1990), Elsevier Publishers: Elsevier Publishers Amsterdam), 243-320 · Zbl 0900.68283
[12] Detlefs, D., Nelson, G., Saxe, J., 1996. Simplify: the ESC Prover. COMPAQ. Available from: http://www.research.digital.com/SRC/esc/Esc.html; Detlefs, D., Nelson, G., Saxe, J., 1996. Simplify: the ESC Prover. COMPAQ. Available from: http://www.research.digital.com/SRC/esc/Esc.html
[13] Giunchiglia, F., Pecchiari, P., Talcott, C.L., 1994. Reasoning Theories: Towards an Architecture for Open Mechanized Reasoning Systems. Technical Report TR-9409-15, IRST; Giunchiglia, F., Pecchiari, P., Talcott, C.L., 1994. Reasoning Theories: Towards an Architecture for Open Mechanized Reasoning Systems. Technical Report TR-9409-15, IRST · Zbl 0899.03022
[14] Jaffar, J., Lassez, J.-L., 1987. Constraint logic programming. In: Proceedings 14th ACM Symposium on Principles of Programming Languages, pp. 111-119; Jaffar, J., Lassez, J.-L., 1987. Constraint logic programming. In: Proceedings 14th ACM Symposium on Principles of Programming Languages, pp. 111-119
[15] Janičić, P.; Bundy, A.; Green, I., A framework for the flexible integration of a class of decision procedures into theorem provers, (Ganzinger, H., CADE-16, Proceedings of the 16th International Conference on Automated Deduction. CADE-16, Proceedings of the 16th International Conference on Automated Deduction, Trento, July 7-10, 1999. CADE-16, Proceedings of the 16th International Conference on Automated Deduction. CADE-16, Proceedings of the 16th International Conference on Automated Deduction, Trento, July 7-10, 1999, Lecture Notes in Artificial Intelligence, vol. 1632 (1999), Springer-Verlag), 127-141 · Zbl 0941.68122
[16] Kapur, D., Musser, D.R., Nie, X., 1994. An overview of the tecton proof system. In: Theoretical Computer Science, vol. 133; Kapur, D., Musser, D.R., Nie, X., 1994. An overview of the tecton proof system. In: Theoretical Computer Science, vol. 133 · Zbl 0938.68823
[17] Kapur, D., Nie, X., 1994. Reasoning about Numbers in Tecton. Technical Report, Department of Computer Science, State University of New York, Albany, NY 12222; Kapur, D., Nie, X., 1994. Reasoning about Numbers in Tecton. Technical Report, Department of Computer Science, State University of New York, Albany, NY 12222
[18] Kaufmann, M.; Moore, J. S., Industrial strength theorem prover for a logic based on Common Lisp, IEEE Transactions on Software Engineering, 23, 4, 203-213 (1997)
[19] Klop, J. W., Term rewriting systems, (Abramsky, S.; Gabbay, D. M.; Maibaum, T. S.E., Handbook of Logic in Computer Science, vol. 2 (1992), Oxford University Press: Oxford University Press Oxford), 1-117, (Chapter 1)
[20] Lassez, J.-L.; Maher, M. J., On Fourier’s algorithm’s for linear arithmetic constraints, Journal of Automated Reasoning, 9, 373-379 (1992) · Zbl 0781.90064
[21] Manna, Z., 1994. STeP; Manna, Z., 1994. STeP
[22] Monfroy, E., Ringeissen, C., 1998. SoleX: a domain-independent scheme for constraint solver extension. In: AISC’98, 4th International Conference on Artificial Intelligence and Symbolic Computation, Plattsburgh, New York, September. pp. 222-233; Monfroy, E., Ringeissen, C., 1998. SoleX: a domain-independent scheme for constraint solver extension. In: AISC’98, 4th International Conference on Artificial Intelligence and Symbolic Computation, Plattsburgh, New York, September. pp. 222-233
[23] Nelson, G., Oppen, D.C., 1978. Simplification by Cooperating Decision Procedures. Technical Report STAN-CS-78-652, Stanford Computer Science Department; Nelson, G., Oppen, D.C., 1978. Simplification by Cooperating Decision Procedures. Technical Report STAN-CS-78-652, Stanford Computer Science Department · Zbl 0452.68013
[24] Nelson, G.; Oppen, D. C., Fast decision procedures based on congruence closure, Journal of the ACM, 27, 2, 356-364 (1980) · Zbl 0441.68111
[25] Shostak, R. E., Deciding combination of theories, Journal of the ACM, 31, 1, 1-12 (1984) · Zbl 0629.68089
[26] Steinbach, J., 1994. Termination of Rewriting. Ph.D. Thesis, Universitaat Kaiserslautern; Steinbach, J., 1994. Termination of Rewriting. Ph.D. Thesis, Universitaat Kaiserslautern
[27] Zhang, H., Contextual rewriting in automated reasoning, Fundamenta Informaticae, 24, 1/2, 107-123 (1995) · Zbl 0839.68051
[28] Zhang, H.; Remy, J. L., Contextual rewriting, (Jouannaud, J.-P., Proceedings of the 1st International Conference on Rewriting Techniques and Applications. Proceedings of the 1st International Conference on Rewriting Techniques and Applications, Dijon, France, May 1985. Proceedings of the 1st International Conference on Rewriting Techniques and Applications. Proceedings of the 1st International Conference on Rewriting Techniques and Applications, Dijon, France, May 1985, LNCS, vol. 202 (1985), Springer), 46-62
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.