Proofscape Module Tutorial

• Deductions
  • Top-level deductions
  • Targets
  • Expansions
• Modules
  • Libpaths
  • Imports
  • Comments
• Nodes
  • Labels and languages
  • TeX labels
  • PDF labels
  • Other syntaxes
  • Cf references
• Node Types
  • Assertion nodes
  • Intro nodes
  • Supposition nodes
  • Existential nodes
  • Method nodes
  • Citation nodes
  • Falsum nodes
  • Relation chain nodes
• Subdeductions
• Contradictions and Cases
  • Proof by contradiction
  • Proof by cases
  • Using auxiliary deducs
• WOLOG
  • WOLOG without reduction method
  • WOLOG with reduction method
• Running Definitions
  • Recording running defs
  • Using running defs
  • Choosing how to encode definitions
• Downward Flow
• Annotations