Allens Intervall-Logik

Webinterface zur Intervall-Logik von James F. Allen

Eingabeformat:

Es koennen nur Allensche Constraints eingegeben werden, diese werden mit Kommata getrennt. Atomare Constraints koennen entweder als A r B (bei Basisrelation r) oder als A {r1,r2} B fuer die Disjunktion mehrerer Basisconstraints eingegeben werden. Die Basisrelationen werden als =,<,m,d,o,s,f eingegeben, die Inversen werden im Allgemeinen durch Grossbuchstaben dargestellt, also als: >,M,D,O,S,F. Ein Beispiel ist:

A {<,o,m} B, B {=,m} C, C {D} D, D {m,M,=} A

Ein widerspruechliches Beispiel, wobei der Allensche Abschluss diesen nicht findet, ist:

D o B, D {s,m} C, D {s,m} A, A  {d,D} B, B {d,D} C, A {f,F} C

Die folgenden Abbildungen erlaeutern die Basisrelationen.

   A = B

    A
   <-------->
    B
   <-------->

   A < B

    A             B
   <-------->    <-------->

         A > B

    B             A
   <-------->    <-------->

   A m B

    A         B
   <--------><-------->

         A M B

    B         A
   <--------><-------->

   A s B

    A        
   <-------->
    B
   <------------->

         A S B

    A
   <------------->
    B        
   <-------->

   A f B

         A        
        <-------->
    B
   <------------->

         A F B

    A
   <------------->
         B        
        <-------->

   A o B

    A        
   <-------->
         B
        <--------->

         A O B

         A
        <--------->
    B        
   <-------->

   A d B

        A        
       <-------->
    B
   <----------------->

         A D B

    A
   <----------------->
        B        
       <-------->

Hinweise zur Ausgabe

Die Ausgabe besteht aus bis zur 4 Teilen.

Im ersten Teil wird die Eingabe als Tabelle dargestellt, dabei sind schon offensichtliche Vereinfachungen vorgenommen (Symmetrien, Vervollstaendigung leerer Eintraege und A = A fuer alle Intervalle A.

Im zweiten Teil wird der berechnete Allensche Abschluss als quadratische Matrix dargestellt. Ein Ausrufezeichen bedeutet: 'Widerspruch gefunden'.

Im dritten Teil wird die Erfuellbarkeit des Allenschen Constraints (falls entsprechend angekreuzt) mit einem vollstaendigen Verfahren getestet. Da der Allenscheabschluss weder Herleitungs- noch Widerspruchsvollstaendig ist, kann das Ergebnis von der Tabelle (Allenscher Abschluss) abweichen.

Wenn der Allensche Constraint erfuellbar ist, folgen in zwei weiteren Teilen Modelle (falls angekreuzt, in Form von Tabellen und in graphischer Darstellung).

Implementierung

Dieses Webinterface wurde in Haskell programmiert. Es basiert auf dem Programm zur Bachelorarbeit:

Alexey Mosesov: Implementierung von Inferenzverfahren fuer die Allensche Zeitlogik, 2012