Ursprünglich entstanden als einfache Syntaxchecker s "tks.AL" und "tks.FO" für die Arbeitsgruppe "Theorie komplexer Systeme" am Institut für Informatik der Goethe-Universität Frankfurt am Main.

Es wird keine Haftung für Schäden an Soft- oder Hardware, Vermögen oder Gesundheit übernommen, welche durch das Benutzen oder Nichtbenutzen des Programms entstehen. Es gibt keine Garantie dafür, dass die Nutzung zu einem bestimmten Zeitpunkt möglich ist, noch das die gelieferten Ergebnisse, auch nicht zufällig, richtig sind. Dies gilt insbesondere bei der Nutzung zur Lösung von Übungsaufgaben.

Fehlermeldungen sind willkommen (email an):

andre dot frochaux at informatik dot hu-berlin dot de

3. Februar 2020
bug fix:Kleiner Bug bei der unit propagation (bei DPLL-Algorithmus
known bugs:
none

9. November 2018
bug fix:Kleiner Bug in Resolventenberechnung (bei Resolutionswiderlegung und - algorithmus
known bugs:
none

4. Oktober 2018
bug fix:Klammersetzung im Tseitin-Verfahren
known bugs:
none

2. Oktober 2018
Tseitin-Verfahren
Eingabe erlaubt jetzt auch ∧, ∨, → und ↔. (Für copy & paste)
known bugs:
none

12. Juli 2018
Syntaxbäume können wahlweise auch in der ausführlichen Form dargestellt werden
known bugs:
none

9. Juli 2018
Umzug zur HU
Umstellung auf php7
Resolutionswiderlegung
Resolutionsalgorithmus
DPLL-Algorithmus
known bugs:
none

17. Mai 2018
Test auf Hornklauselmengen und Streichungsalgorithmus
Ausgabe von Subscripts in Klauseln und Formeln
known bugs:
none

16. Mai 2018
Eingabe einzelner Klauseln ist jetzt auch möglich. (Vorbereitung für Resolventenbildung)
Neuer Header der auch eine Klausel und eine Klauselmenge beinhaltet
Bigfix: Mit gestrigem Update gab es einen kleinen Fehler beim Starten der Auswertung unter gegebene Interpretation
known bugs:
none

15. Mai 2018
Aufgeräumt und neues Design (altes über Einstellungen verfügbar)
known bugs:
none

23. März 2015
Ändern der Reihenfolge der Variablen in der WT
known bugs:
none

6. März 2015
Berechnen der dualen Formel
known bugs:
none

5. Februar 2015
Berechnen der NNF
Bigfix: Fehlermeldungen bei Formeln ohne Variablen
Bigfix: Einige Formeln passierten NNF check, obwohl sie nicht NNF waren
known bugs:
none

12. Dezember 2014
Test auf Normalformen wird standardmäßig ausgeführt
Eingabe per konj/disj Klauseln
Roadmap
known bugs:
none

15. November 2014
Test auf Normalformen
Erzeugen einer KNF
known bugs:
none

22. Oktober 2014
Kontaktmail aktualisiert
known bugs:
none

2./6. Oktober 2014
Support ENG/FRA (unvollendet)
known bugs:
none

28. Juli 2014
Anpassung an Syntax mit PHP-upgrade
known bugs:
none

03. November 2008
Diverse kleine Anpassungen an DisMod.
known bugs:
none

21. Oktober 2008
Eingabehilfe, Minimierung ausgegraut da nicht Stoff in DisMod.
known bugs:
none

03. März 2008
Minimierung der DNF (Bsp. )
known bugs:
none

02. März 2008
Nach dem der AL-Checker und erste zusätzliche Funktionen fertig sind. Startet About und changelog.
Logo
DNF (aus erfüllenden Belegungen - vorerst ohne Minimierung)
known bugs:
none