Getting Started
Introduction
System Requirements
Using the CPL
Overview
The ToolBox
Map
Rule Menus
Rule Form Pane
Instantiation Pane
Apply Rule Button
The Fitch Diagram
Map
Title Bar
Minimize Button
Maximize Button
Line Numbers
Formulae
Justification
Subderivations/Scope Boxes
Scroll Bars
The Goal Tree
Overview
Interpreting What You See in the Goal Tree
Selecting Formulae
Subderivations and Scope Overview

Advanced Features
Previewing Problems
Loading Problems
Saving Problems
Editing Proofs
Glossary
Elimination Rules
Introduction Rules

Introduction Rules
Conjunction: &I
Rule Definition
How to Apply &I Forwards
How to Apply &I Backwards
Troubleshooting
Disjunction: vI
Rule Definition
How to Apply vIL Forwards
How to Apply vIR Forwards
How to Apply vIL Backwards
How to Apply vIR Backwards
Troubleshooting
Conditional: →I
Rule Definition
How to Apply →I Forwards
How to Apply →I Backwards
Troubleshooting

Falsum: ⊥I
Rule Definition
How to Apply ⊥I
Troubleshooting
Negation: ¬I
Rule Definition
How to Apply ¬I Forwards
How to Apply ¬I Backwards
Troubleshooting

Biconditional: ↔I
Rule Definition
How to Apply ↔I Forwards
How to Apply ↔I Backwards
Troubleshooting

Universal Quantifier: ∀I
Rule Definition
How to Apply ∀I Forwards
How to Apply ∀I Backwards
Understanding the Restrictions
Troubleshooting
Existential Quantifier: ∃I
Rule Definition
How to Apply ∃I Forwards
How to Apply ∃I Backwards
Troubleshooting
Elimination Rules
Conjunction: &E
Rule Definition
How to apply &EL
How to apply &ER
Troubleshooting
Disjunction: vE
Rule Definition
How to Apply vE
Troubleshooting
Conditional: →E
Rule Definition
How to Apply →E
Troubleshooting

Negation: ¬E
Rule Definition
How to Apply ¬E Forwards
How to Apply ¬E Backwards
Troubleshooting

Biconditional: ↔E
Rule Definition
How to Apply ↔EL
How to Apply ↔ER
Troubleshooting

Universal Quantifier: ∀E
Rule Definition
How to Apply ∀E
Troubleshooting
Existential Quantifier: ∃E
Rule Definition
How to Apply ∃E
Understanding the Restrictions
Troubleshooting
Assumptions
Making Assumptions
Sentential Derived Rules
Coming Soon...
Predicate Derived Rules
Coming Soon...
Identity Rules
Identity Introduction: =I
Rule Definition
How to Apply =I
Troubleshooting
Identity Elimination: =E
Rule Definition
How to Apply =E
Troubleshooting

E

• Elimination Rules
  • Biconditional (↔E)
  • Conditional (→E)
  • Conjunction (&E)
  • Disjunction (vE)
  • Negation (¬E)

I

• Introduction Rules
  • Biconditional (↔I)
  • Conditional (→I)
  • Conjunction (&I)
  • Disjunction (vI)
  • Falsum (⊥I)
  • Negation (¬I)