zbMATH — the first resource for mathematics

Abstract canonical presentations. (English) Zbl 1099.03047
Summary: Solving goals – like proving properties, deciding word problems or resolving constraints – is much easier with some presentations of the underlying theory than with others. Typically, what have been called “completion processes”, in particular in the study of equational logic, involve finding appropriate presentations of a given theory to more easily solve a given class of problems. We provide a general proof-theoretic setting that relies directly on the fundamental concept of “good”, that is, normal-form, proofs, itself defined using well-founded orderings on proof objects. This foundational framework allows for abstract definitions of canonical presentations and very general characterizations of saturation and redundancy criteria.

03F03 Proof theory, general (including proof-theoretic semantics)
03B35 Mechanization of proofs and logical operations
68Q42 Grammars and rewriting systems
Full Text: DOI
[1] Baader, F.; Nipkow, T., Term rewriting and all that, (1998), Cambridge University Press Cambridge
[2] Bachmair, L.; Dershowitz, N., Equational inference, canonical proofs, and proof orderings, J. assoc. comput. Mach., 41, 2, 236-276, (1994) · Zbl 0806.68095
[3] L. Bachmair, N. Dershowitz, J. Hsiang, Orderings for equational proofs, in: Proc. First IEEE Symp. on Logic in Computer Science, Cambridge, MA, June 1986, pp. 346-357.
[4] Bachmair, L.; Dershowitz, N.; Plaisted, D.A., Completion without failure, (), 1-30
[5] L. Bachmair, H. Ganzinger, Completion of first-order clauses with equality by strict superposition (Extended abstract), in: M. Okada, S. Kaplan (Eds.), Proc. Second Internat. Workshop on Conditional and Typed Term Rewriting Systems, Montreal, Canada, June 1990, Lecture Notes in Computer Science, Vol. 516, Springer, Berlin, 1991, pp. 162-180.
[6] Bachmair, L.; Ganzinger, H., Resolution theorem proving, (), 19-99, (Chapter 2) · Zbl 0993.03008
[7] Barthe, G.; Cirstea, H.; Kirchner, C.; Liquori, L., Pure patterns type systems, (), 250-261 · Zbl 1321.68137
[8] M.P. Bonacina, Distributed automated deduction, Ph.D. Thesis, Department of Computer Science, State University of New York at Stony Brook, December 1992.
[9] M.-P. Bonacina, N. Dershowitz, Abstract canonical inference, ACM Trans. Comput. Logic, 2006, to appear. · Zbl 1367.03023
[10] Bonacina, M.-P.; Hsiang, J., Towards a foundation of completion procedures as semidecision procedures, Theoret. comput. sci., 146, 199-242, (1995) · Zbl 0873.68107
[11] B. Buchberger, Ein Algorithmus zum auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal, Dissertation, University of Innsbruck, Austria, 1965. · Zbl 1245.13020
[12] Buchberger, B., Multidimensional systems theory, (), 184-232
[13] Buchberger, B., History and basic features of the critical-pair/completion approach, J. symbolic comput., 3, 1 & 2, 3-38, (1987) · Zbl 0645.68094
[14] H. Cirstea, C. Kirchner, L. Liquori, The Rho cube, in: F. Honsell (Ed.), Proc. Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science, Genova, Italy, April 2001, pp. 166-180. · Zbl 0978.68072
[15] Comon, H.; Kirchner, C., Constraint solving on terms, lecture notes in computer science, Vol. 2002, (2001)
[16] Dershowitz, N., Orderings for term-rewriting systems, Theoret. comput. sci., 17, 3, 279-301, (1982) · Zbl 0525.68054
[17] N. Dershowitz, Completion and its applications, in: H. Aı¨t-Kaci, M. Nivat (Eds.), Resolution of Equations in Algebraic Structures, Vol. 2: Rewriting Techniques, Academic Press, New York, 1989, pp. 31-86.
[18] N. Dershowitz, C. Kirchner, Abstract canonical inference systems, in: Proc. 16th Internat. Workshop on Unification, Copenhagen, Denmark, July 2002. · Zbl 1099.03047
[19] Dershowitz, N.; Kirchner, C., Abstract saturation-based inference, (), 65-74
[20] Dershowitz, N.; Marcus, L.; Tarlecki, A., Existence, uniqueness and construction of rewrite systems, SIAM J. comput., 17, 4, 629-639, (1988) · Zbl 0658.68029
[21] Dershowitz, N.; Okada, M., Proof-theoretic techniques and the theory of rewriting, (), 104-111
[22] Dershowitz, N.; Plaisted, D.A., Rewriting, (), 535-610, (Chapter 9) · Zbl 0992.68123
[23] Doggaz, N.; Kirchner, C., Completion for unification, Theoret. comput. sci., 85, 1, 231-251, (1991) · Zbl 0735.68078
[24] Dowek, G.; Hardin, T.; Kirchner, C., Theorem proving modulo, J. automated reason., 31, 1, 33-72, (2003) · Zbl 1049.03011
[25] Girard, J.-Y.; Lafont, Y.; Taylor, P., Proofs and types, Cambridge tracts in theoretical computer science, Vol. 7, (1989), Cambridge University Press UK
[26] I. Gnaedig, C. Kirchner, H. Kirchner, Equational completion in order-sorted algebras, in: M. Dauchet, M. Nivat (Eds.), Proc. 13th Colloq. on Trees in Algebra and Programming, Lecture Notes in Computer Science, Vol. 299, Springer, Berlin, 1988, pp. 165-184. · Zbl 0647.68036
[27] Grätzer, G., Universal algebra, (1979), Springer Berlin · Zbl 0182.34201
[28] Hsiang, J.; Rusinowitch, M., Proving refutational completeness of theorem proving strategies. the transfinite semantic tree method, J. assoc. comput. Mach., 38, 3, 559-587, (1991) · Zbl 0799.68170
[29] G. Huet, Confluent reductions: abstract properties and applications to term rewriting systems, J. ACM 27 (4) (1980) 797-821. · Zbl 0458.68007
[30] Huet, G., A complete proof of correctness of the knuth – bendix completion algorithm, J. computer system sci., 23, 1, 11-21, (1981) · Zbl 0465.68014
[31] Jouannaud, J.-P.; Kirchner, H., Completion of a set of rules modulo a set of equations, SIAM J. comput., 15, 4, 1155-1194, (1986) · Zbl 0665.03005
[32] Jouannaud, J.-P.; Rubio, A., The higher-order recursive path ordering, (), 402-411
[33] Kandri-Rody, A.; Kapur, D.; Winkler, F., Knuth – bendix procedures and buchberger algorithm—A synthesis, (), 55-67
[34] Kapur, D.; Musser, D.R., Proof by consistency, Artificial intelligence, 13, 2, 125-157, (1987) · Zbl 0631.68073
[35] Knuth, D.E.; Bendix, P.B., Simple word problems in universal algebras, (), 263-297 · Zbl 0188.04902
[36] D.S. Lankford, Canonical inference, Memo ATP-32, Automatic Theorem Proving Project, University of Texas, Austin, TX, December 1975.
[37] Metivier, Y., About the rewriting systems produced by the knuth – bendix completion algorithm, Inform. process. lett., 16, 1, 31-34, (1983) · Zbl 0506.68032
[38] Nieuwenhuis, R.; Rubio, A., Paramodulation-based theorem proving, (), 371-443, (Chapter 7) · Zbl 0997.03012
[39] Peterson, G.E.; Stickel, M.E., Complete sets of reductions for some equational theories, J. assoc. comput. Mach., 28, 2, 233-264, (1981) · Zbl 0479.68092
[40] M. Rusinowitch, Démonstration Automatique: Techniques de Réécriture. Science Informatique. InterEditions, Paris, 1989.
[41] Rusinowitch, M., Theorem-proving with resolution and superposition, J. symbolic comput., 11, 21-50, (1991) · Zbl 0723.68094
[42] Smyth, M.B., Powerdomains, J. computer systems sci., 16, 23-36, (1977) · Zbl 0408.68017
[43] W. Taylor, Equational logic, Houston J. Math. 5 (1979) 1-51. Appears also in G. Grätzer, Universal Algebra, second ed., Springer, Berlin, 1979, Appendix 4.
[44] “Terese”, M. Bezem, J.W. Klop, R. de Vrijer (Eds.), Term Rewriting Systems, Cambridge University Press, Cambridge, UK, 2002.
[45] R. Virga, Higher-order rewriting with dependent types. Ph.D. Thesis, Department of Mathematical Sciences, Carnegie Mellon University, available as Technical Report CMU-CS-99-167, September 1999.
[46] G. Burel, C. Kirchner, Completion is an instance of abstract canonical system inference, in: K. Futatsugi, J.-P. Jouannaud, J. Meseguer (Eds.), Meaning and Computation, Festschrift in Honor of Prof. Joseph Goguen, Lecture Notes in Computer Science, Springer Verlag, 2006. · Zbl 1132.03314
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.