Equational completion in order-sorted algebras. (English) Zbl 0698.68028
See the review in Zbl 0647.68036.
MSC:
| 68Q65 | Abstract data types; algebraic specification |
| 03D03 | Thue and Post systems, etc. |
| 08B05 | Equational logic, Mal’tsev conditions |
| 68W30 | Symbolic computation and algebraic computation |
Keywords:
completion procedures; equational term rewriting systems; order-sorted algebras; order-sorted equational logicReferences:
| [1] | Bachmair, L., Proof methods for equational theories, (PhD thesis (August 1988), University of Illinois: University of Illinois Urbana-Champaign), Revised version |
| [2] | Bachmair, L.; Dershowitz, N., Completion for rewriting module a congruence, (Proc. 2nd Conf. on Rewriting Techniques and Applications (1987), Springer: Springer Berlin), Bordeaux, France · Zbl 0659.68114 |
| [3] | Bachmair, L.; Dershowitz, N.; Hsiang, J., Orderings for equational proofs, Proc. Symp. Logic in Computer Science, 346-357 (1986), Boston, MA |
| [4] | Burstall, R. M.; MacQueen, D. B.; Sannella, D. T., Hope: an experimental applicative language, Conf. Record of the 1980 LISP Conference, 136-143 (1980) |
| [5] | Cunningham, R. J.; Dick, A. J.J., Rewrite systems on a lattice of types, (Technical Report (1983), Imperial College, Department of Computing) · Zbl 0575.68043 |
| [6] | Dershowitz, N., Orderings for term-rewriting systems, Theoret. Comput. Sci., 17, 279-301 (1982) · Zbl 0525.68054 |
| [7] | Dershowitz, N., Termination of rewriting, J. Symbolic Comput., 3, 1, 2, 69-116 (1987) · Zbl 0637.68035 |
| [8] | Dershowitz, N.; Manna, Z., Proving termination with multiset orderings, Comm. ACM, 22, 8, 465-476 (1979) · Zbl 0431.68016 |
| [9] | Dershowitz, N.; Plaisted, D. A., Equational programming, (Hayes, J. E.; Michie, D.; Richards, J., Machine Intelligence 11: The Logic and Acquisition of Knowledge (1988), Oxford University Press: Oxford University Press Oxford), 21-56 · Zbl 0722.68070 |
| [10] | Dick, A. J.J., ERIL equational reasoning: an interactive laboratory, (Buchberger, B., Proc. EUROCAL Conf. (1985), Springer-Verlag: Springer-Verlag Linz, Austria) |
| [11] | Futatsugi, K.; Goguen, J.; Jouannaud, J.-P.; Meseguer, J., Principles of OBJ-2, (Reid, B., Proc. 12th ACM Symp. on Principles of Programming Languages (1985), Association for Computing Machinery), 52-66 |
| [12] | Ganzinger, H., Order-sorted completion: the many-sorted way, (Proc. Internat. Joint Conf. on Theory and Practice of Software Development: Colloquium on Software Engineering (1989), Springer: Springer Berlin) · Zbl 0736.68050 |
| [13] | Gnaedig, I.; Kirchner, C.; Kirchner, H., Equational completion in order-sorted algebras, (Dauchet, M.; Nivat, M., Proc. 13th Colloquium on Trees in Algebra and Programming (1988), Springer, Berlin), 165-184, Nancy, France · Zbl 0647.68036 |
| [14] | Gogolla, M., Algebraic specifications with partially ordered sorts and declarations, (Internet Bericht FB-169 (1983), Universität of Dortmund, Abteilung Informatik) · Zbl 0544.68015 |
| [15] | Goguen, J., Order sorted algebras: exceptions and error sorts, coercions and overloaded operators, (Semantics and Theory of Computation Report 14, 14 (December 1978), Computer Science Department, UCLA) |
| [16] | Goguen, J.; Kirchner, C.; Kirchner, H.; Megrelis, A.; Meseguer, J.; Winkler, T., An introduction to OBJ-3, (Jouannaud, J.-P.; Kaplan, S., Proc. 1st Internat. Workshop on Conditional Term Rewriting Systems (1988), Springer: Springer Berlin), (also as internal report CRIN: 88-R-001). · Zbl 0666.68010 |
| [17] | Goguen, J.; Meseguer, J., Order-sorted algebra I: partial and overloaded operations, errors and inheritance, (Technical Report (June 1983), SRI International, Computer Science Lab), given as lecture at Seminar on Types, Carnegie-Mellon University, June 1983. |
| [18] | Goguen, J.; Meseguer, J., Order-sorted algebra solves the constructor-selector, multiple representation and coercion problem, (Proc. 2nd Symp. on Logic in Computer Science (1987), IEEE Computer Society Press), 18-29 |
| [19] | Goguen, J.; Meseguer, J.; Plaisted, D., Programming with parameterized abstract objects in OBJ, Theory Practice Software Technol., 163-193 (1982) |
| [20] | Goguen, J. A.; Jouannaud, J.-P.; Meseguer, J., Operational semantics for order-sorted algebra, (Proc. 12th Internat. Colloquium on Automata, Languages and Programming (1985), Nafplion: Nafplion Greece), 221-231 · Zbl 0591.68041 |
| [21] | Goguen, J. A.; Meseguer, J., Completeness of many-sorted equational logic, (Technical Report CSLI-84-15 (1984), Center for the Study of Language and Information, Stanford University) · Zbl 0498.03018 |
| [22] | Goguen, J. A.; Meseguer, J., Models and equality for logical programming, (Ehrig, H.; Kowalski, R.; Levi, G.; Montanari, U., Proc. Internat. Joint Conf. on Theory and Practice of Software Development (1987), Springer: Springer Berlin), 1-22, Pisa, Italy · Zbl 0626.68032 |
| [23] | Goguen, J. A.; Meseguer, J., Remarks on remarks on many-sorted equational logic, EATCS Bull.. EATCS Bull., SIGPLAN Notices, 22, 30, 41-48 (1987) |
| [24] | Hoffman, C. M.; O’Donnell, M. J., Programming with equations, Trans. Programming Languages Systems, 4, 1, 83-112 (1982) · Zbl 0481.68008 |
| [25] | Hsiang, J.; Dershowitz, N., Rewrite methods for clausal and non-clausal theorem proving, (Proc. 10th Internat. Colloquium on Automata, Languages and Programming (1983), Springer: Springer Berlin), 331-346, Barcelona, Spain · Zbl 0523.68080 |
| [26] | Huet, G., A complete proof of corectness of the Knuth and Bendix completion algorithm, J. Comput. System Sci., 23, 11-21 (1981) · Zbl 0465.68014 |
| [27] | Huet, G., Confluent reductions: abstract properties and applications to term rewriting systems, J. ACM. J. ACM, 18th Symp. on Foundations of Computer Science, 27, 4, 797-821 (1977), IEEE, preliminary version in · Zbl 0458.68007 |
| [28] | Huet, G.; Hullot, J.-M., Proofs by induction in equational theories with constructors, J. Comput. System Sci.. J. Comput. System Sci., Proc. 21st Symp. Foundations of Computer Science, 25, 2, 239-266 (1980), IEEE, preliminary version in · Zbl 0532.68041 |
| [29] | Huet, G.; Oppen, D., Equations and rewrite rules: a survey, (Book, R., Formal Language Theory: Perspectives and Open Problems (1980), Academic Press: Academic Press New York), 349-405 |
| [30] | Isakowitz, T.; Gallier, J., Congruence closure in order-sorted algebra, Technical report (June 1988) |
| [31] | Isakowitz, T.; Gallier, J., Rewriting in order-sorted equational logic, (Kowalski, R.; Bowen, K., Proc. Logic Programming Conf. (1988), MIT Press: MIT Press Seattle) |
| [32] | Jouannaud, J.-P., Confluent and coherent equational term rewriting systems, (Ausiello, G.; Protasi, M., Proc. 8th Colloquium on Trees in Algebra and Programming (1983), Springer: Springer Berlin), L’Aquila, Italy · Zbl 0522.68013 |
| [33] | Jouannaud, J.-P., Proof algebras, Rewriting Techniques and Applications Conference (1987), Bordeaux, France · Zbl 0666.68003 |
| [34] | Jouannaud, J.-P.; Kirchner, H., Completion of a set of rules modulo a set of equations, SIAM J. Comput.. SIAM J. Comput., Proc. 11th ACM Symp. on Principles of Programming Languages, 15, 4, 1155-1194 (1984), Salt Lake City · Zbl 0665.03005 |
| [35] | Jouannaud, J.-P.; Lescanne, P., On multiset orderings, Inform. Process. Lett., 10, 57-63 (1982) · Zbl 0486.68041 |
| [36] | Jouannaud, J.-P.; Muñoz, M., Termination of a set of rules modulo a set of equations, (Proc. 7th Conf. on Automated Deduction (1984), Springer: Springer Berlin) · Zbl 0546.68077 |
| [37] | Kirchner, C., Computing unification algorithms, Proc. 1st Symp. on Logic in Computer Science, 206-216 (1986), Boston, U.S.A. |
| [38] | Kirchner, C., Méthodes et outils de conception systématique d’algorithmes d’unification dans les théories équationnelles, Thése d’état de l’Universite de Nancy, 1 (1985) |
| [39] | Kirchner, C., Methods and tools for equational unification, Proc. Colloquium on Resolution of Equations in Algebraic Structures (May 1987), Austin, Texas |
| [40] | Kirchner, C., Order-sorted equational unification, 5th Internat. Conf. on Logic Programming, Seattle, U.S.A.. 5th Internat. Conf. on Logic Programming, Seattle, U.S.A., Rapport de Recherche INRIA 954, Dec. 88 (August 1988), also as |
| [41] | Kirchner, C.; Kirchner, H., Reveur-3: implementation of a general completion procedure parametrized by built-in theories and strategies, Sci. Comput. Programming, 20, 8 (1986) · Zbl 0635.68017 |
| [42] | Kirchner, C.; Kirchner, H.; Meseguer, J., Operational semantics of OBJ-3, (Technical Report 87-R-87 (1987), Centre de Recherche en Informatique de Nancy) · Zbl 0649.68028 |
| [43] | Kirchner, C.; Kirchner, H.; Meseguer, J., Operational semantics of OBJ-3, (Proc. 15th Internat. Colloquium on Automata, Languages and Programming (1988), Springer: Springer Berlin), 287-301 · Zbl 0649.68028 |
| [44] | Kirchner, H., A general inductive completion algorithm and application to abstract data types, (Shostak, R., Proc. 7th Internat. Conf. on Automated Deduction. Proc. 7th Internat. Conf. on Automated Deduction, Lecture Notes in Computer Science (1984), Springer: Springer Berlin), 282-302 · Zbl 0562.68068 |
| [45] | Kirchner, H., Preuves par complétion dans les variétés d’algébres, Thése d’état de l’Université de Nancy, 1 (1985) |
| [46] | Knuth, D.; Bendix, P., Simple word problems in universal algebra, (Leech, J., Computational Problems in Abstract Algebras (1970), Pergamon Press: Pergamon Press Oxford), 263-297 · Zbl 0188.04902 |
| [47] | Lankford, D.; Ballantyne, A., Decision procedures for simple equational theories with associative commutative axioms: complete sets of associative commutative reductions, (Technical Report (1977), University of Texas at Austin, Department of Mathematics and Computer Science) |
| [48] | Lankford, D.; Ballantyne, A., Decision procedures for simple equational theories with commutative axioms: complete sets of commutative reductions, (Technical Report (1977), University of Texas at Austin, Department of Mathematics and Computer Science) · Zbl 0449.20059 |
| [49] | Lankford, D.; Ballantyne, A., Decision procedures for simple equational theories with permutative axioms: complete sets of permutative reductions, (Technical Report (1977), University of Texas at Austin, Department of Mathematics and Computer Science) |
| [50] | Lescanne, P., Computer experiments with the REVE term rewriting systems generator, (Proc. 10th ACM Symp. on Principles of Programming Languages (1983), ACM), 99-108 |
| [51] | Megrelis, A., A logic of semi-functions, inclusion and equality. The setting, (Technical Report 89-R-58 (1989), Centre de Recherche en Informatique de Nancy) |
| [52] | Meseguer, J.; Goguen, J. A., Initiality, induction and computability, (Nivat, M.; Reynolds, J., Algebraic Methods in Semantics (1985), Cambridge University Press: Cambridge University Press New York) · Zbl 0571.68004 |
| [53] | Meseguer, J.; Goguen, J. A.; Smolka, G., Order sorted unification, Proc. Colloquium on Resolution of Equations in Algebraic Structures (May 1987), Austin, Texas |
| [54] | Newman, M-H-A., On theories with a combinatorial definition of Equivalence, Ann. Math., 223-243 (1942) · Zbl 0060.12501 |
| [55] | Oberschelp, A., Untersuchungen zur mehrsortigen Quantorenlogik, Math. Ann., 145, 297-333 (1962) · Zbl 0101.25001 |
| [56] | Peterson, G.; Stickel, M., Complete sets of reductions for some equational theories, J. ACM, 28, 233-264 (1981) · Zbl 0479.68092 |
| [57] | Poigné, A., Parameterisation for order-sorted algebraic specifications, (Technical Report (1986), Department of Computing, Imperial College: Department of Computing, Imperial College London) |
| [58] | Schmidt-Schauss, M., Unification in many sorted equational theories, (Siekmann, J., Proc. 8th Conf. on Automated Deduction (1986), Springer: Springer Berlin) · Zbl 0643.68138 |
| [59] | Smolka, G., Order-sorted Horn logic semantics and deduction, (Technical Report seki-SR-86-17 (1986), Universität Kaiserslautern) |
| [60] | Smolka, G.; Nutt, W.; Goguen, J. A.; Meseguer, J., Order sorted equational computation, Proc. Colloquium on Resolution of Equations in Algebraic Structures (May 1987), Austin, Texas |
| [61] | Toyama, Y., Confluent term rewriting systems with membership conditions, (Kaplan, S.; Jouannaud, J.-P., Proc. 1st Internat Workshop on Conditional Term Rewriting Systems (1987), Springer: Springer Berlin), 228-241, Orsay, France · Zbl 0667.68041 |
| [62] | Turner, D. A., MIRANDA: a non-strict functional language with polymorphic types, (Jouannaud, J.-P., Proc. 2nd Conf. on Functional Programming Languages and Computer Architecture. Proc. 2nd Conf. on Functional Programming Languages and Computer Architecture, Lecture Notes in Computer Science (1985), Springer: Springer Berlin), 1-16 · Zbl 0592.68014 |
| [63] | Waldmann, U., Semantics of order-sorted specifications, (Technical Report 297 (1989), Universität Dortmund) · Zbl 0746.68064 |
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.
