Part I
Core Maude

2 Using Maude
 2.1 Getting Maude
 2.2 Running Maude
 2.3 Getting support and more information
 2.4 Reporting bugs in Maude
3 Syntax and Basic Parsing
 3.1 Identifiers
 3.2 Modules
 3.3 Sorts and subsorts
 3.4 Operator declarations
 3.5 Kinds
 3.6 Operator overloading
 3.7 Variables
 3.8 Terms and preregularity
 3.9 Parsing
4 Functional Modules
 4.1 Unconditional equations
 4.2 Unconditional memberships
 4.3 Conditional equations and memberships
 4.4 Operator attributes
 4.5 Statement attributes
 4.6 Admissible functional modules
 4.7 Matching and equational simplification
 4.8 More on matching and simplification modulo
 4.9 The reduce, match, trace, and show commands
5 System Modules
 5.1 Unconditional rules
 5.2 Conditional rules
 5.3 Admissible system modules
 5.4 The rewrite, frewrite, and search commands
6 Module Operations
 6.1 Module importation
 6.2 Module summation and renaming
 6.3 Parameterized programming
7 Predefined Data Modules
 7.1 Boolean values
 7.2 Natural numbers
 7.3 Random numbers and counters
 7.4 Integer numbers
 7.5 Machine integers
 7.6 Rational numbers
 7.7 Floating-point numbers
 7.8 Strings
 7.9 String and number conversions
 7.10 Quoted identifiers
 7.11 Basic theories and standard views
 7.12 Containers: lists and sets
 7.13 Maps and arrays
 7.14 A linear Diophantine equation solver
8 Object-Based Programming
 8.1 Configurations
 8.2 Object-message fair rewriting
 8.3 Example: data agents
 8.4 External objects
9 Model Checking Invariants Through Search
 9.1 Invariants
 9.2 Model checking of invariants
 9.3 Bounded model checking of invariants
 9.4 Verifying infinite-state systems through abstractions
10 LTL Model Checking
 10.1 LTL formulas and the LTL module
 10.2 Associating Kripke structures to rewrite theories
 10.3 LTL model checking
 10.4 The LTL satisfiability and tautology checker
 10.5 Other model-checking examples
11 Reflection, Metalevel Computation, and Strategies
 11.1 Reflection and metalevel computation
 11.2 The META-TERM module
 11.3 The META-MODULE module: Metarepresenting modules
 11.4 The META-LEVEL module: Metalevel operations
 11.5 Internal strategies
12 Unification
 12.1 Introduction
 12.2 Order-sorted unification modulo a set of axioms
 12.3 Theories currently supported
 12.4 The unify command
 12.5 Unification at the metalevel: metaUnify and metaDisjointUnify
 12.6 Some applications of unification
 12.7 Endogenous vs. exogenous order-sorted unification algorithms
13 User Interfaces and Metalanguage Applications
 13.1 The LOOP-MODE module
 13.2 User interfaces
 13.3 Using the loop
 13.4 Tokens, bubbles, and metaparsing
14 Debugging and Troubleshooting
 14.1 Debugging approaches
 14.2 Traps and known problems