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

Your First Session

The INFORMATION Menu

...a RALF theorem

...a definition

...a transformation rule

...a RALF theory

...a RALF module

...the signature

...get and install RALF

...initialize a RALF user

...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

claudia@informatik.unibw-muenchen.de

-->