SEP
Einfaches Rechnen mit Ungleichungen
SEP
a <= b & b < c & b <= d & c < e & d <= f
sieht man recht schnell, ob daraus eine andere Ungleichung folgt (im Beispiel folgt b < e aber nicht notwendig b < f). Hat man mehr Ungleichungen, so ist das nicht mehr so einfach zu sehen. Insbesondere dann, wenn die Gleichungen nicht vorsortiert sind. (Gibt es immer eine geeignete Sortierung?) Die Sache wird außerdem komplizierter, wenn man Ungleichungen der Form x <> y zulässt.
Im SEP soll ein effizienter Algorithmus für dieses Problem entwickelt werden (dieser könnte z. B. auf Graphen basieren), und in der funktionalen Sprache ML implementiert werden. Damit dieses Programm an Isabelle angebunden werden kann, muss der Algorithmus neben einer ja/nein-Entscheidung auch eine Begründung dafür zurückliefern.