¬ x (x ∧ y) (x ↔ y) {A,¬B} {{A,¬B},{A,B}}
roadmap about config

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.

Error messages are welcome (email to):

andre dot frochaux at informatik dot hu-berlin dot de

changelog

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. March 2015
You can change the order of the variables in the truth-table (faster verification of your own solution)
known bugs:
none

6. March 2015
Computation of the dual formula.
known bugs:
none

5. Februar 2015
Computation of the Negation normal form
Bigfix: Errors by formulas without variables
Bigfix: Some formulas passed the NNF-check, but they shouldn't
known bugs:
none

12. Dezember 2014
Testing of normal forms by default
Input of clauses enabled (conj/ disj)
Roadmap
known bugs:
none

15. November 2014
Test of normal forms
Transformation to a cnf
known bugs:
none

22. Oktober 2014
Mail adress updated
known bugs:
none

2./6. Oktober 2014
Support english/french (unfinished)
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. March 2015
You can change the order of the variables in the truth-table (faster verification of your own solution)
known bugs:
none

6. March 2015
Computation of the dual formula.
known bugs:
none

5. Februar 2015
Computation of the Negation normal form
Bigfix: Errors by formulas without variables
Bigfix: Some formulas passed the NNF-check, but they shouldn't
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 (fnc)
known bugs:
none

22. Oktober 2014
e-mail updated
known bugs:
none

2/6 octobre 2014
Soutien anglais / français (inachevé)
bugs connus:
aucun