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 Conversions between strings and lists of quoted identifiers
 7.12 Basic theories and standard views
 7.13 Containers: lists and sets
 7.14 Maps and arrays
 7.15 A linear Diophantine equation solver
 7.16 Predefined Parameterized Views
8 Object-Based Programming
 8.1 Configurations
 8.2 Object-message fair rewriting
 8.3 Example: data agents
9 External Objects and IO
 9.1 Standard streams
 9.2 File I/O
 9.3 Sockets
 9.4 Processes
 9.5 Control-C on external events
10 Strategy Language
 10.1 The strategy language
 10.2 Strategy modules
 10.3 Parameterization in strategy modules
 10.4 Strategy search and the dsrewrite command
 10.5 Case study: logic programming
11 Model Checking Invariants Through Search
 11.1 Invariants
 11.2 Model checking of invariants
 11.3 Bounded model checking of invariants
 11.4 Verifying infinite-state systems through abstractions
12 LTL Model Checking
 12.1 LTL formulas and the LTL module
 12.2 Associating Kripke structures to rewrite theories
 12.3 LTL model checking
 12.4 The LTL satisfiability and tautology checker
 12.5 Other model-checking examples
13 Unification
 13.1 Introduction
 13.2 Order-sorted unification
 13.3 Theories currently supported
 13.4 The unify command
 13.5 Some applications of unification
 13.6 Endogenous vs. exogenous order-sorted unification algorithms
 13.7 Some notes on the implementation of unification
14 Variants and Variant Unification
 14.1 Introduction
 14.2 Term variants
 14.3 Theories currently supported
 14.4 The get variants command
 14.5 Variant generation with irreducibility constraints
 14.6 Incremental variant generation
 14.7 Variant generation in incomplete unification examples
 14.8 Variant-based equational order-sorted unification
 14.9 The variant unify command
 14.10 Variant-based unification with irreducibility constraints
 14.11 Incremental variant unification
 14.12 Variant unification in incomplete unification examples
 14.13 The variant match command
15 Narrowing
 15.1 Introduction
 15.2 Applications
 15.3 Completeness of narrowing
 15.4 Narrowing with simplification
 15.5 Theories supported for narrowing reachability
 15.6 The vu-narrow command
 15.7 The fvu-narrow command
 15.8 Narrowing with extra variables in righthand sides of rules
16 SMT Solving
 16.1 Boolean formulas
 16.2 Formulas using integer linear arithmetic
 16.3 Formulas using rational linear arithmetic
 16.4 Formulas using rational and integer linear arithmetic
 16.5 Satisfiability of formulas
 16.6 A brief introduction to variant satisfiability
17 Reflection, Metalevel Computation, and Internal Strategies
 17.1 Reflection and metalevel computation
 17.2 The META-TERM module
 17.3 The META-STRATEGY module: Metarepresenting the strategy language
 17.4 The META-MODULE module: Metarepresenting modules
 17.5 The META-VIEW module: Metarepresenting views
 17.6 The META-LEVEL module: Metalevel operations
 17.7 Internal strategies
18 User Interfaces and Metalanguage Applications
 18.1 User interfaces
 18.2 The interaction with the system
 18.3 Tokens, bubbles, and metaparsing
 18.4 The LOOP-MODE module (deprecated)
19 Meta-interpreters
 19.1 Maude meta-interpreters
 19.2 A Russian dolls example
 19.3 An execution environment for Mini-Maude
20 Debugging and Troubleshooting
 20.1 Debugging approaches
 20.2 Debugging strategy executions
 20.3 Traps and known problems