[Next]
Go forward to The Main Window


Welcome to RALF

RALF is a relation-algebraic formula manipulation system and interactive proof checker. Its meta language is first-order predicate logic in calculational style, that is the major tools are substitution of equals for equals, weakening and strengthening. RALF supports this proof style by a graphical user interface: Theorems are represented as trees and the subexpression to be transformed can be selected by mouse click. In the first sections we describe the theory RALF is based on and then how to work with the system.

  • The Main Window
  • Signature, Terms, Formulae and Theorems
  • Inference Rules
  • Basic inference rules
  • Meta rules
  • Assumptions
  • Example Proof
  • RALF Superuser
  • Your First Session
  • The INFORMATION Menu
  • What is ...
  • ...an axiom
  • ...a RALF theorem
  • ...a definition
  • ...a transformation rule
  • ...a meta rule
  • ...a RALF theory
  • ...a RALF module
  • ...the signature
  • How to ...
  • ...get and install RALF
  • ...initialize a RALF user
  • ...start RALF
  • ...quit RALF
  • ...get information about the signature
  • ...enter a theorem
  • ...load a theorem
  • ...start proving a new theorem
  • ...save a theorem
  • ...delete a theorem
  • ...rename a theorem
  • ...print all theorems
  • ...print all definitions
  • ...print all axioms an proven theorems of RALF superuser
  • ...print all definitions of RALF superuser
  • ...print a proof
  • ...save the proof as a LaTeX document
  • ...undo a proof step
  • ...continue a proof
  • ...change the part of the proof to continue with
  • ...apply a meta rule
  • ...apply a transformation rule
  • ...define a function or predicate
  • ...delete a function or predicate
  • ...rename a function or predicate
  • ...create a module
  • ...delete a module
  • ...load a module
  • ...unload a module
  • ...modify a module
  • ...find out in which proofs a transformation rule was applied
  • ...find out what was applied in the current proof
  • ...check consistency of your theories
  • ...become a RALF superuser
  • ...change the RALF superuser password
  • ...enter an axiom
  • ...change an axiom
  • ...delete an axiom
  • ...enter a meta rule
  • ...use the mouse
  • ...change the operator signs in the LaTeX file
  • Suggestions
  • claudia@informatik.unibw-muenchen.de

    [Next]
    -->