Für die Klasse der Booleschen Algebren hat A. Tarski in einer berühmten Arbeit eine vollständige Klassifikation bezüglich elementarer Äquivalenz durch numerische Invarianten angegeben. Diese Tarski-Invarianten wurden von D. Kozen so verfeinert, daß sie zu einem asymptotisch optimalen Entscheidungsverfahren für die Klasse der Booleschen Algebren führten. Diesen Verfahren wurde zum ersten Mal am Lehrstuhl implementiert und mit Erfolg an nichttrivialen Beispielen getestet.
Ein ähnliches Verfahren für dichte lineare Ordnungen, das auf Ferrante und Geiser zurückgeht, wird ebenfalls - in einem weit allgemeineren Rahmen - zur Zeit implementiert. Dieser Rahmen (nämlich lokal-endliche universelle Theorien) wurde in [][] gefunden und an vielen Beispielen (z.B. universelle partielle Ordnungen, unendliche Zufallsgraphen) verifiziert.
Eine Implementierung dieser und weiterer Beispiele ist geplant.