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.