PKL-BEWEISER Version 1.0 ======================== Fertiggestellt: 24.9.92 Autoren: Johannes 5 Joemann, Steven Bashford Features: -------- 1. Definition von Tableau-Regeln und Konstruktion von neuen Regeln basierend auf alten Beispiele ... i. ... fuer Tableau-Regeln ----------------------- aaa(X,Y) := [T1: T1: X && T1: Y ] [F1: F1: X || F1: Y ] [T2: T2: X && T2: Y ] [F2: F2: X || F2: Y ] [T3: T3: X && T3: Y ] [F3: F3: X || F3: Y ] laa(X,Y) := [T1: (T1: X && T1: Y) || (T1: X && F1: Y) ] [F1: F1: X && F1: Y ] [T2: T2: X && T2: Y /// F1: X && F1: Y /// [] /// [] ] [F2: F2: X || F2: Y /// F1: X && T1: Y /// [] /// [] ] [T3: T3: X && T3: Y /// T1: X && T1: Y /// [] /// [] ] [F3: F3: X || F3: Y /// F1: X && T1: Y /// [] /// [] ] n1 3 (X):= [T1: F1:X] [F1: T1:X] [T2: T3:X] [F2: F3:X] [T3: T2:X] [F3: F2:X] n2 3 (X):= [T1: T3:X] [F1: F3:X] [T2: F2:X] [F2: T2:X] [T3: T1:X] [F3: F1:X] ii. ... fuer die Tableaurueckfuehrung --------------------------------- taa (X,Y) := (X laa Y) aaa (Y laa X), n3 3 (X) := (n1 (n2 X)), n4 3 (X) := (n2 (n1 X)), n5 3 (X) := (n1 (n2 (n1 X))) 2. Beweisen von Aussagenlogischen Formeln der Pkl Der Beweismechanismus ist noch nicht vollstaendig automatisiert. Der Mechanismus fuehrt alle moeglichen Reduktionen in einem Schritt aus. Der Benutzer muss Schrittweise den Beweis zu Ende fuehren. 3. Baum-Darstellung sowie Term-Darstellung von Beweisbaeumen Die Term-Darstellung bietet eine kompaktere Repraesentation als die Baum-Darstellung. Man kann waehrend eines Beweises zwischen den Darstellungen hin und herschalten. Formel 1: (X aaa Y) ooo Z Baumdarstellung: | +-----O-R-+ | | | t1:Z +--AND-+ | | t1:X t1:Y Termdarstellung: ((t1:X) & (t1:Y)) | (t1:Z) Formel 2: (X laa Y) aaa (Y laa X) Baumdarstellung: | +------------------------AND------------+ | | | | +-----///-----------+ +-----///-----------+ | | | | | +---------------------+ | +---------------------+ +--AND-+ | | ||+-+||+-+| +--AND-+ | | ||+-+||+-+| | | | +--AND-+ ||| |||| || | | | +--AND-+ ||| |||| || t2:X t2:Y | | | ||+-+||+-+| t2:Y t2:X | | | ||+-+||+-+| |f1:X f1:Y|| || | |f1:Y f1:X|| || | +---------------------+ +---------------------+ Termdarstellung: (((t2:X) & (t2:Y)) //(f1:X) & (f1:Y)/LB/LB//) & (((t2:Y) & (t2:X)) //(f1:Y) & (f1:X)/LB/LB//) 4. Durchwandern der Beweisbaeume mit der Moeglichkeit zum partiellen Ausfuehren von Beweisschritten Man kann den aktuellen Beweisbaum durchwandern und dann Teilbaeume partiell reduzieren. Dies ist hilfreich um den Ablauf eines Beweises besser zu verstehen. Beim durchwandern des Baumes ist die Darstellung auf den aktuellen Teilbaum beschraenkt. 5. Lokale Variablendarstellung Variablen einer Formel werden mit einer Nummer gekennzeichnet. Mehrmaliges Vorkommen einer Variablen in einer Formel bedeutet, das jedes Vorkommen der Variablen mit einer anderen Nummer versehen wird. Das ist im Laufe eines Beweises hilfreich, um zu sehen welcher Teil einer Formel an welchen Auswirkungen beteiligt war. (X aaa Y) ooo (X aaa Z) ==> (X1 aaa Y1) ooo (X2 aaa Z1) i. Normal | +-----O-R-----+ | | | | +--AND-+ +--AND-+ | | | | t2:X t2:Y t2:X t2:Z ii. mit lokaler Darstellung | +------O-R------+ | | | | +--AND--+ +--AND--+ | | | | t2:X1 t2:Y1 t2:X2 t2:Z1 Bemerkungen: ----------- - In dieser Version wurde zunaechst Wert auf die Funktionalitaet der Bweismechanismen und auf eine Benutzerfreundliche Methode zur Spezifikation von Tableauregeln gelegt. Benutzerschnittstelle sowie Menusystem sind daher noch etwas mager und auf das Noetigste eingeschraenkt. Etwas Zum Beweis-Mechanismus ============================ In dieser Version wurde noch mit der Annahme von unabhaengigen Systemen innerhalb von Transjunktiven Anteilen geaerbeitet. Die Untersuchungen haben ergeben,dass dem warscheinlich nicht so ist, und das ein Systemwechsel einer Variablen in einem T-Anteil Auswirkungen auf das System hat, in das gewechselt wurde. Weiterhin unklar ist noch der Umgang mit geschachtelten T-Anteilen. D.h. T-Anteile in T-Anteilen. Ein weiteres Problem, dass mir aufgefallen ist, ist das konjunktive Zusammenfuegen von T-Anteilen, wenn z.B. in einem der beiden Alpha-Aeste kein T-Anteil vorhanden ist. Uebr diese Regeln muss auch nochmal intensiv nachgedacht werden. In diesem Zusammenhang ist auch die Unabhaengig von lokalen Anteilen und T-Anteilen zu erwaehnen. Hier bin ich mir gar nicht mehr so sicher ob man generell von Unabhaengigkeit, bzw Abhaengigkeit reden kann. Hier muessten meiner Meinung nach noch viel genauere Untersuchungen stattfinden, wobei man Abhaengigkeit und Unabhaengigkeit sowie Mischformen davon noch im Rahmen der jetzigen Regelbeschreibung formulieren kann. Ich tendiere im augenblick zu einer Mischform. Vor dem Angriff einer neuen Version sollten also folgende Punkte untersucht werden: ---------------------------------------------------------------------------------- 1. Unabhaengigkeit/Abhaengigkeit von lokalen und transjunktiven Anteilen 2. Das Zusammenfuegen von T-Anteilen 3. Welche Auswirkungen 1. und 2. auf den angesprochenen Punkt der Systemwechsel haben Eine neue Implementierung, die die Systemwechsel beruecksichtigt, wird zumindest auf Punkt 2 keinen positiven Einfluss ausueben. Etwas zur Implementierung ========================= Ich werde die Sourcen soweit aufbereiten und dokumentieren, das auch die Implementierungs- technischen Details daraus hervorgehen.