1 Manual En

• 1. Introduction
• 2. Examples
  • 2.1. Transitivity of inclusion
    • Rule def_concl_pred : if the conclusion is C
  • 2.2. Power set of the intersection of two sets
• 3. From Muscadet1 to Muscadet4
• 4. Machine representations
  • 4.1. Expression of mathematical statements
  • 4.2. Expression of facts
  • 4.3. Expression of rules
  • 4.4. Expression of super-actions
• 5. How to use Muscadet4
  • 5.1. Direct proof
  • 5.2 From files containing theorems and definitions
  • 5.3. From the TPTP library
  • 5.4 Modification of default options
• 6. Definitions and lemmas
• 7. Elimination of functional symbols
• 8. Building rules
• 9. Activation and order of rules
• 10. Some strategies
  • 10.1. Processing of universal conclusions and of implications
  • 10.2. Processing of conjunctive conclusions
  • 10.3. Processing of universal hypotheses
  • 10.4. Processing of existential conclusions
  • 10.5. Processing of existential hypotheses
  • 10.6. Processing of disjunctive conclusions
  • 10.7. Processing of disjunctive hypotheses
  • 10.8. Knowledge specific to certain domains
• 11. Second order statements
• 12. Distribution
• 13. References