@inproceedings(AlaGutLucNav_ProvingTerminationPropertiesWithMUTERM_AMAST10,
 author       = {Beatriz Alarc{\'{o}}n and Ra{\'{u}}l Guti{\'{e}}rrez and Salvador Lucas and Navarro{-}Marset, Rafael},
 year         = {2010},
 title        = {Proving Termination Properties with mu-term},
 editor       = {Michael Johnson and Dusko Pavlovic},
 booktitle    = {Algebraic Methodology and Software Technology - 13th International Conference, {AMAST} 2010, Lac-Beauport, QC, Canada, June 23-25, 2010. Revised Selected Papers},
 series       = {Lecture Notes in Computer Science},
 volume       = {6486},
 publisher    = {Springer},
 pages        = {201--208},
 doi          = {10.1007/978-3-642-17796-5\_12},
)
@book(BooBurJef_ComputabilityAndLogic_2002,
 author       = {George Boolos and Richard C. Jeffrey},
 year         = {1987},
 title        = {Computability and logic {(2.} ed.)},
 publisher    = {Cambridge University Press},
)
@proceedings(ClavelEtAl_MaudeBook_2007,
 editor       = {Manuel Clavel and Francisco Dur{\'{a}}n and Steven Eker and Patrick Lincoln and Mart{\'{\i}}{-}Oliet, Narciso and Jos{\'{e}} Meseguer and Carolyn L. Talcott},
 year         = {2007},
 title        = {All About Maude - {A} High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic},
 series       = {Lecture Notes in Computer Science},
 volume       = {4350},
 publisher    = {Springer},
 doi          = {10.1007/978-3-540-71999-1},
)
@article(ConMarTomUrb_MechProvTermPolInterp_JAR06,
 author       = {Evelyne Contejean and Claude March{\'{e}} and Ana Paula Tom{\'{a}}s and Xavier Urbain},
 year         = {2005},
 title        = {Mechanically Proving Termination Using Polynomial Interpretations},
 journal      = {J. Autom. Reasoning},
 volume       = {34},
 number       = {4},
 pages        = {325--363},
 doi          = {10.1007/s10817-005-9022-x},
)
@incollection(GogThaWag_AnInitialAlgebraApproachToSpecificationCorrectnessAndImplementationOfADTs_1978,
 author       = {J. A. Goguen and J. W. Thatcher and E. G. Wagner},
 year         = {1978},
 title        = {An initial algebra approach to the specification, correctness and implementation of abstract data types},
 editor       = {R. Yeh},
 booktitle    = {Current Trends in Programming Methodology},
 publisher    = {Prentice-Hall},
 pages        = {80--149},
)
@inproceedings(GogMes_ModelsAndEqualityForLogicalProgramming_TAPSOFT87,
 author       = {Joseph A. Goguen and Jos{\'{e}} Meseguer},
 year         = {1987},
 title        = {Models and Equality for Logical Programming},
 editor       = {Hartmut Ehrig and Robert A. Kowalski and Giorgio Levi and Ugo Montanari},
 booktitle    = {TAPSOFT'87: Proceedings of the International Joint Conference on Theory and Practice of Software Development, Pisa, Italy, March 23-27, 1987, Volume 2: Advanced Seminar on Foundations of Innovative Software Development {II} and Colloquium on Functional and Logic Programming and Specifications {(CFLP)}},
 series       = {Lecture Notes in Computer Science},
 volume       = {250},
 publisher    = {Springer},
 pages        = {1--22},
 doi          = {10.1007/BFb0014969},
)
@article(GogMes_OrderSortedAlgebraI_TCS92,
 author       = {Joseph A. Goguen and Jos{\'{e}} Meseguer},
 year         = {1992},
 title        = {Order-Sorted Algebra {I:} Equational Deduction for Multiple Inheritance, Overloading, Exceptions and Partial Operations},
 journal      = {Theor. Comput. Sci.},
 volume       = {105},
 number       = {2},
 pages        = {217--273},
 doi          = {10.1016/0304-3975(92)90302-V},
)
@book(Hodges_AShorterModelTheory_1997,
 author       = {Wilfried Hodges},
 year         = {1997},
 title        = {A shorter model theory},
 publisher    = {Cambridge University Press},
)
@article(Lucas_PolOverRealsTheoPrac_TIA05,
 author       = {Salvador Lucas},
 year         = {2005},
 title        = {Polynomials over the reals in proofs of termination: from theory to practice},
 journal      = {{ITA}},
 volume       = {39},
 number       = {3},
 pages        = {547--586},
 doi          = {10.1051/ita:2005029},
)
@article(LucMarMes_OpTermCTRSs_IPL05,
 author       = {Salvador Lucas and Claude March{\'{e}} and Jos{\'{e}} Meseguer},
 year         = {2005},
 title        = {Operational termination of conditional term rewriting systems},
 journal      = {Inf. Process. Lett.},
 volume       = {95},
 number       = {4},
 pages        = {446--453},
 doi          = {10.1016/j.ipl.2005.05.002},
)
@inproceedings(LucMes_ModelsForLogicsAndConditionalConstraintsInAutomatedProofsOfTermination_AISC14,
 author       = {Salvador Lucas and Jos{\'{e}} Meseguer},
 year         = {2014},
 title        = {Models for Logics and Conditional Constraints in Automated Proofs of Termination},
 editor       = {Aranda{-}Corral, Gonzalo A. and Jacques Calmet and Mart{\'{\i}}n{-}Mateos, Francisco J.},
 booktitle    = {Artificial Intelligence and Symbolic Computation - 12th International Conference, {AISC} 2014, Seville, Spain, December 11-13, 2014. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {8884},
 publisher    = {Springer},
 pages        = {9--20},
 doi          = {10.1007/978-3-319-13770-4\_3},
)
@inproceedings(LucMes_ProvingOperationalTerminationOfDeclarativeProgramsInGeneralLogics_PPDP14,
 author       = {Salvador Lucas and Jos{\'{e}} Meseguer},
 year         = {2014},
 title        = {Proving Operational Termination of Declarative Programs in General Logics},
 editor       = {Olaf Chitil and Andy King and Olivier Danvy},
 booktitle    = {Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming, Kent, Canterbury, United Kingdom, September 8-10, 2014},
 publisher    = {{ACM}},
 pages        = {111--122},
 doi          = {10.1145/2643135.2643152},
)
@inproceedings(LucMes_LocalOperationalTerminationInGeneralLogics_FWirsing15,
 author       = {Salvador Lucas and Jos{\'{e}} Meseguer},
 year         = {2015},
 title        = {Localized Operational Termination in General Logics},
 editor       = {Rocco De Nicola and Rolf Hennicker},
 booktitle    = {Software, Services, and Systems - Essays Dedicated to Martin Wirsing on the Occasion of His Retirement from the Chair of Programming and Software Engineering},
 series       = {Lecture Notes in Computer Science},
 volume       = {8950},
 publisher    = {Springer},
 pages        = {91--114},
 doi          = {10.1007/978-3-319-15545-6\_9},
)
@inproceedings(Meseguer_GeneralLogics_LC87,
 author       = {Jos\'{e} Meseguer},
 year         = {1989},
 title        = {General Logics},
 editor       = {H.-D. {Ebbinghaus} et al.},
 booktitle    = {Logic Colloquium'87},
 publisher    = {North-Holland},
 pages        = {275--329},
)
@incollection(Rabin_DecidableTheories_1977,
 author       = {Michael O. Rabin},
 year         = {1977},
 title        = {Decidable Theories},
 editor       = {J. Barwise},
 booktitle    = {Handbook of Mathematical Logic},
 publisher    = {Elsevier},
 pages        = {595--629},
 doi          = {10.1016/S0049-237X(08)71116-9},
)
@mastersthesis(Reinoso_LogicalModelsForAutomatedSemanticsDirectedProgramAnalysis_TFM15,
 author       = {Patricio Reinoso},
 year         = {2015},
 title        = {Logical Models For Automated Semantics-Directed Program Analysis},
 school       = {DSIC, Master in Software Systems Engineering and Technology (MITSS), Universitat Polit\`ecnica de Val\`encia},
)
@book(Schrijver_TheoryOfLinearAndIntProg_1986,
 author       = {Alexander Schrijver},
 year         = {1986},
 title        = {Theory of linear and integer programming},
 publisher    = {John Wiley \& sons},
)
@article(Toyama_CountExTermDirectSumTRSs_IPL87,
 author       = {Yoshihito Toyama},
 year         = {1987},
 title        = {Counterexamples to Termination for the Direct Sum of Term Rewriting Systems},
 journal      = {Inf. Process. Lett.},
 volume       = {25},
 number       = {3},
 pages        = {141--143},
 doi          = {10.1016/0020-0190(87)90122-0},
)