Maude is a declarative programming language based on rewriting logic that incorporates many features that in order 
to prove certain computational properties lead to difficulties.
The task of proving termination of rewrite systems in indeed quite hard but applied to real programming languages, 
becomes more complicated due to these inherent features. 
Therefore, methods for proving termination of such programs require specific techniques and a careful analysis.

Several papers have studied how to prove termination of  (a subset of)  Maude programs. However, all of them follow a 
transformational approach where the original program is transformed
until it reaches a rewrite system that can  be managed with existing techniques and termination tools.
In practice, the fact of transforming the original systems used to complicate the proof of termination since it introduces 
new symbols and rules in the system.
In this thesis, we tackle the problem of proving termination of (a subset of) Maude programs by means of direct methods.

On the one hand, we pay attention to the strategy of Maude. Maude is an eager language  where the
 arguments of a function are always evaluated before the application of the function
 that uses them. This strategy (known as call by value) can lead to nontermination if programs are not written carefully. 
 For this reason, Maude (specifically) incorporates mechanisms to control the  program execution such as syntactic annotations, 
which are associated to arguments of symbols. In rewriting, this strategy is known as innermost context-sensitive rewriting.

On the other hand, Maude also incorporates the possibility of declaring attributes.
Semantically, declaring a set of equational attributes for an operator is equivalent to declaring the corresponding
 equations for the operator; however, it avoids termination problems and leads to a more efficient evaluation.
The effect of declaring equational attributes is to compute with equivalence classes modulo these equations.

The dependency pair framework  develops the idea of an incremental application of different termination
  techniques for solving termination problems. It has shown to be a powerful and efficient way to prove termination of
  rewriting automatically. In this thesis, we  deal with  termination of innermost context-sensitive rewriting and of rewriting 
modulo specific axioms  by extending the dependency pair framework.