LP, the Larch Prover — Table of contents

• 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
    • Syntax descriptions
    • Symbols
    • Keywords
  • Command summary
    • Command arguments
    • Abbreviations for commands and arguments
    • Interrupting command execution
• Logical syntax and semantics
  • Sorts
  • Variables
  • Operators
    • Signatures
    • Constants
    • Equality operators
    • Logical operators
    • Conditional operators
    • Notations
      • Bracketed operators
      • Functional operators
      • Infix, prefix, and postfix operators
  • Quantifiers
    • Prenex form
    • Capturing variables
  • Terms
    • Overloaded identifiers
    • Precedence of operators
  • Formulas
    • Equations
• Operational syntax and semantics
  • Inconsistencies
  • Rewrite rules
  • Operator theories
  • Induction rules
  • Deduction rules
  • Partitioned-by rules
  • Naming
    • Assigning names to facts
    • Naming facts in commands
    • Name classes
  • The assert command
  • The declare command
  • The make command
  • The order command
    • Brute force orderings
    • Registered orderings
    • The dsmpos ordering
    • Polynomial orderings
    • Interactive ordering mechanisms
  • The register command
    • Operator height
    • Operator status
  • The unorder command
  • The unregister command
• Forward inference
  • The apply command
  • The complete command
  • The critical-pairs command
  • The fix command
  • The instantiate command
  • The normalize command
  • The rewrite command
  • Proofs by consistency
• Backward inference
  • Overview of proof methods for formulas
  • Proofs by normalization
  • Proofs by cases
  • Proofs by contradiction
  • Proofs by induction
    • Structural induction
    • Multilevel structural induction
    • Well founded induction
  • Proof mechanisms for particular syntactic forms
    • Proofs by generalization
    • Proofs by specialization
    • Proofs of conjunctions
    • Proofs of implications
    • Proofs of logical equivalence
    • Proofs of conditionals
    • Proofs of deduction rules
    • Proofs of induction rules
    • Proofs of operator theories
  • Proofs by explicit commands
  • Backward inference commands
    • The apply command
    • The cancel command
    • The normalize command
    • The prove command
    • The qed command
    • The resume command
    • The rewrite command
    • The box and diamond 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
  • Preparing input and recording work
  • Formalizing axioms and conjectures
  • Orienting formulas into rewrite rules
  • Managing proofs
  • Making proofs go faster
  • Unix command line options
• Releases
  • Installing LP
  • Reporting problems
  • Development history
    • Features added in Release 3.1
    • Changes from Release 2.4 to Release 3.1
    • Release 3.1a
    • Release 3.1b
• 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