Demo

• √2 is not rational
  • √2 interactive
  • √2 with islands
  • √2 with proof planning

• Proof Planning
  • The ε-δ-domain
  • Meta-reasoning in the ε-δ-domain

  • Classification of residue classes
  • Isomorphisms between residue classes
  • Non-isomorphic residue classes with randomization
  • Non-isomorphic residue classes with HR

  • Verification of GAP computations on permutation groups

  • Optimization problems in economics

• Agent-based Mathematical Reasoning
  • Some examples of set equations
  • Exploration of set equations
  • Cooperation between Omega and MBase

• Learning with LearnOmatic
  • Learning of control knowledge for methods
  • Application of learnt knowledge

• Interactive Proof Planning
  • Properties of residue classes
  • Group homomorphisms
  • The interactive ε-δ-domain

Either start your local LOUI (the graphical user interface of the OMEGA system) or the online version with before you begin. The button on the subsequent pages will load the corresponding demo into LOUI. (You have to enable the execution of OZ-applets in your browser.)

Ω