Class SimpRule

java.lang.Object
  extended bySimpRule

class SimpRule
extends java.lang.Object

Eine SimpRule enthält die verschiedenen Muster einer Vereinfachungsregel des Beweisers.
Eine solche Regel besteht im Allgemeinen (je nach Typ) aus einem Muster, einem Vereinfachungsmuster und einer Bedingung, jeweils in Form eines Baumes (ein Objekt vom Typ SimpleNode). Es existieren 7 verschiedene Regeltypen. Diese unterscheiden sich im Wesentlichen durch ihre Anwendung. Einige besitzen beispielsweise eine Bedingung, andere nicht. Eine genaue Beschreibung der Regeln mit Beispielen befindet sich in der zum Programm gehörenden Dokumentation.

See Also:
Rules, BoolSimp, OrdSimp, AlgSimp, Simplifier, SimpleNode

Field Summary
(package private)  SimpleNode condPattern
          Bedingung.
(package private)  java.lang.String idNameOfSimplifiedCondPattern
          Name einer speziellen freien Variablen im Muster condPattern.
(package private)  SimpleNode pattern
          Muster.
(package private)  SimpleNode simpPattern
          Vereinfachungsmuster.
(package private)  short type
          Typ der Vereinfachungsregel.
 
Constructor Summary
SimpRule(SimpleNode pattern, SimpleNode simpPattern)
          Erzeugt eine SimpRule, welche nur aus einem Muster und dem Vereinfachungsmuster besteht.
SimpRule(SimpleNode pattern, SimpleNode simpPattern, SimpleNode condPattern, int type, java.lang.String idName)
          Erzeugt eine SimpRule bestehend aus einem Muster pattern, einem Vereinfachungsmuster simpPattern, einer Bedingung condPattern, dem Typ der Vereinfachungsregel type und dem Namen idName einer speziellen freien Variablen.
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

pattern

SimpleNode pattern
Muster.
Damit diese Vereinfachungsregel auf eine Verifikationsbedingung angewendet werden kann, muss die Bedingung auf das Muster passen.


simpPattern

SimpleNode simpPattern
Vereinfachungsmuster.
Passt die Verifikationsbedingung auf das Muster, wird sie anhand dieses Vereinfachungsmusters umgeformt.


condPattern

SimpleNode condPattern
Bedingung.
Manche Regeln besitzen eine Bedingung, die erfüt sein muss, damit die Regel angewendet werden kann.


type

short type
Typ der Vereinfachungsregel. Für Einzelheiten siehe Klassenbeschreibung.


idNameOfSimplifiedCondPattern

java.lang.String idNameOfSimplifiedCondPattern
Name einer speziellen freien Variablen im Muster condPattern. Entstandene Bindungen dieser Variablen müssen im Muster simpPattern eingesetzt werden.

Constructor Detail

SimpRule

public SimpRule(SimpleNode pattern,
                SimpleNode simpPattern)
Erzeugt eine SimpRule, welche nur aus einem Muster und dem Vereinfachungsmuster besteht.

Parameters:
pattern - Das Muster.
simpPattern - Das Vereinfachungsmuster.

SimpRule

public SimpRule(SimpleNode pattern,
                SimpleNode simpPattern,
                SimpleNode condPattern,
                int type,
                java.lang.String idName)
Erzeugt eine SimpRule bestehend aus einem Muster pattern, einem Vereinfachungsmuster simpPattern, einer Bedingung condPattern, dem Typ der Vereinfachungsregel type und dem Namen idName einer speziellen freien Variablen.