Sufficient completeness verification for conditional and constrained TRS

Bouhoula, 1996, Using induction and rewriting to verify and complete parameterized specifications, Theoretical Computer Science, 170, 245, 10.1016/S0304-3975(96)80708-0 Bouhoula, 2008, Automated induction with constrained tree automata, vol. 5195, 539 Bouhoula, 2001, Automata-driven automated induction, Information and Computation, 169, 1, 10.1006/inco.2001.3036 Bouhoula, 1995, Implicit induction in conditional theories, Journal of Automated Reasoning, 14, 189, 10.1007/BF00881856 Bouhoula, 2000, Specification and proof in membership equational logic, Theoretical Computer Science, 236, 35, 10.1016/S0304-3975(99)00206-6 Dauchet, 1995, Automata for reduction properties solving, Journal of Symbolic Computation, 20, 215, 10.1006/jsco.1995.1048 Comon, 1986, Sufficient completeness, term rewriting and anti-unification, vol. 230, 128 Comon, 2005, Tree automata with one memory, set constraints and cryptographic protocols, Theoretical Computer Science, 331, 143, 10.1016/j.tcs.2004.09.036 Comon, 2003, Ground reducibility is exptime-complete, Information and Computation, 187, 123, 10.1016/S0890-5401(03)00134-2 Comon E. Contejean, C. Marché, B. Monate, X. Urbain, Proving termination of rewriting with cime, in: Ext. Abstracts of the 6th Int. Workshop on Termination WSTʼ03, 2003, pp. 71–73, see also http://cime.lri.fr. N. Dershowitz, J.-P. Jouannaud, Rewrite systems, in: Handbook of Theoretical Computer Science, Formal Models and Semantics, vol. B, 1990, pp. 243–320. Dershowitz, 1987, Confluence of conditional rewrite systems, vol. 308, 31 Durán, 2008, MTT: the maude termination tool (system description), vol. 5195, 313 Ganzinger, 1987, Ground term confluence, parametric conditional equational specifications, vol. 247, 286 Giesl, 2006, AProVE 1.2: Automatic termination proofs, the dependency pair framework, vol. 4130, 281 Gnaedig, 2006, Computing constructor forms with non terminating rewrite programs, 121 J.V. Guttag, The specification and application to programming of abstract data types, PhD thesis, Univ. of Toronto, 1975, Report CSRG-59. Guttag, 1978, Notes on type abstraction, vol. 69, 593 Guttag, 1978, The algebraic specification of abstract data types, Acta Informatica, 10, 27, 10.1007/BF00260922 Hendrix, 2005, A sufficient completeness reasoning tool for partial specifications, vol. 3467, 165 J. Hendrix, H. Ohsaki, J. Meseguer, Sufficient completeness checking with propositional tree automata, Technical Report UIUCDCS-R-2005-2635 (CS), UILU-ENG-2005-1825 (ENGR), Univ. of Illinois at Urbana-Champaign, 2005. Huet, 1982, Proofs by induction in equational theories with constructors, J. Comput. Syst. Sci., 25, 239, 10.1016/0022-0000(82)90006-X Jouannaud, 1986, Automatic proofs by induction in equational theories without constructors, 358 Kaplan, 1987, Simplifying conditional term rewriting systems: Unification, termination and confluence, Journal of Symbolic Computation, 4, 295, 10.1016/S0747-7171(87)80010-X Kapur, 1994, An automated tool for analyzing completeness of equational specifications, 28 Kapur, 1987, On sufficient-completeness and related properties of term rewriting systems, Acta Informatica, 24, 395, 10.1007/BF00292110 Kapur, 1990, On ground confluence of term rewriting systems, Information and Computation, 86, 14, 10.1016/0890-5401(90)90023-B Kapur, 1991, Sufficient-completeness, ground-reducibility and their complexity, Acta Informatica, 28, 311, 10.1007/BF01893885 Korp, 2009, Tyrolean termination tool 2, vol. 5595, 295 Kounalis, 1985, Completeness data type specifications, vol. 204, 348 Kounalis, 1992, Studies on the ground convergence property of conditional theories, 363 Lazrek, 1990, Tools for proving inductive equalities, relative completeness, and omega-completeness, Information and Computation, 84, 47, 10.1016/0890-5401(90)90033-E Lucas, 2004, MU-TERM: A tool for proving termination of context-sensitive rewriting, vol. 3091, 200 Misra, 1994, Powerlist: A structure for parallel recursion, ACM Transactions on Programming Languages and Systems, 16, 1737, 10.1145/197320.197356