Constraint contextual rewriting

Armando, 2001, Maple’s evaluation process as constraint contextual rewriting, 32 Armando, A., Compagna, L., Ranise, S., 2001. RDL—rewrite and decision procedure laboratory. In: IJCAR 2001, Proceedings of the International Joint Conference on Automated Reasoning, Siena, Italy, June, 2001 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, 2001, 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, 124 Baumgartner, P., Furbach, U., Petermann, U., 1992. A Unified Approach to Theory Reasoning. Technical Report, Inst. für Informatik (Koblenz) Bjørner, N.S., 1998. Integrating Decision Procedures for Temporal Verification. Ph.D. Thesis, Computer Science Department, Stanford University Bjørner, 1997, A practical integration of first-order reasoning and decision procedures, vol. 1249, 101 Boyer, 1988, Integrating decision procedures into Heuristic theorem provers: a case study of linear arithmetic, Machine Intelligence, 11, 83 Coglio, A., Giunchiglia, F., Pecchiari, P., Talcott, C.L., 1997. A Logic Level Specification of the NQTHM Simplification Process. Technical Report, IRST Cyrluk, 1996, On Shostak’s decision procedure for combinations of theories, vol. 1104, 463 Dershowitz, 1990, Rewriting systems, 243 Detlefs, D., Nelson, G., Saxe, J., 1996. Simplify: the ESC Prover. COMPAQ. Available from: http://www.research.digital.com/SRC/esc/Esc.html Giunchiglia, F., Pecchiari, P., Talcott, C.L., 1994. Reasoning Theories: Towards an Architecture for Open Mechanized Reasoning Systems. Technical Report TR-9409-15, IRST Jaffar, J., Lassez, J.-L., 1987. Constraint logic programming. In: Proceedings 14th ACM Symposium on Principles of Programming Languages, pp. 111–119 Janičić, 1999, A framework for the flexible integration of a class of decision procedures into theorem provers, vol. 1632, 127 Kapur, D., Musser, D.R., Nie, X., 1994. An overview of the tecton proof system. In: Theoretical Computer Science, vol. 133 Kapur, D., Nie, X., 1994. Reasoning about Numbers in Tecton. Technical Report, Department of Computer Science, State University of New York, Albany, NY 12222 Kaufmann, 1997, Industrial strength theorem prover for a logic based on Common Lisp, IEEE Transactions on Software Engineering, 23, 203, 10.1109/32.588534 Klop, 1992, Term rewriting systems, vol. 2, 1 Lassez, 1992, On Fourier’s algorithm’s for linear arithmetic constraints, Journal of Automated Reasoning, 9, 373, 10.1007/BF00245296 Manna, Z., 1994. STeP: The Stanford Temporal Prover. Technical Report CS-TR-94-1518, Stanford University 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 Nelson, G., Oppen, D.C., 1978. Simplification by Cooperating Decision Procedures. Technical Report STAN-CS-78-652, Stanford Computer Science Department Nelson, 1980, Fast decision procedures based on congruence closure, Journal of the ACM, 27, 356, 10.1145/322186.322198 Shostak, 1984, Deciding combination of theories, Journal of the ACM, 31, 1, 10.1145/2422.322411 Steinbach, J., 1994. Termination of Rewriting. Ph.D. Thesis, Universitaat Kaiserslautern Zhang, 1995, Contextual rewriting in automated reasoning, Fundamenta Informaticae, 24, 107, 10.3233/FI-1995-24125 Zhang, 1985, Contextual rewriting, vol. 202, 46