- Introduction
- Design philosophy
- A sample proof
- Getting started
- Sample declarations for sorts, operators
- Sample axioms for finite sets
- Useful kinds of axioms
- Sample conjectures
- Two easy theorems
- Three theorems about union
- Alternative proofs of theorems about union
- Three theorems about subset
- An alternate induction rule
- Two final theorems about subset
- How to guide a proof

- Notational conventions
- Command summary

- Logical syntax and semantics
- Operational syntax and semantics
- Forward inference
- Backward inference
- Overview of proof methods for formulas
- Proofs by normalization
- Proofs by cases
- Proofs by contradiction
- Proofs by induction
- Proof mechanisms for particular syntactic forms
- Proofs by explicit commands
- Backward inference commands

- Other commands
- The clear command
- The comment command
- The define-class command
- The delete command
- The display command
- The execute command
- The forget command
- The freeze and thaw commands
- The help command
- The history command
- The push-settings and pop-settings commands
- The quit command
- The set command
- The activity setting
- The automatic-ordering setting
- The automatic-registry setting
- The box-checking setting
- The completion-mode setting
- The directory setting
- The display-mode setting
- The hardwired-usage setting
- The immunity setting
- The log-file setting
- The lp-path setting
- The name-prefix setting
- The ordering-method setting
- The page-mode setting
- The prompt setting
- The proof-methods setting
- The reduction-strategy setting
- The rewriting-limit setting
- The script-file setting
- The statistics-level setting
- The trace-level setting
- The write-mode setting

- The show command
- The statistics command
- The stop command
- The unset command
- The version command
- The write command

- Hints on using LP
- Current development
- Glossary
- Accessible quantifiers
- Confluent rewriting systems
- Conjecture
- Conservative extension
- Convergent rewriting systems
- Equational term-rewriting
- Flattened representations for terms
- Matching
- Normalization
- Reduction by rewrite rules
- Skolem constants and functions
- Substitutions
- Subgoal
- Terminating rewriting systems
- Unification