LΩUI: Lovely ΩMEGA User Interface
Jörg Siekmann, Stephan Hess, Christoph Benzmüller, Lassaad Cheikhrouhou, Armin Fiedler, Helmut Horacek, Michael Kohlhase, Karsten Konrad, Andreas Meier, Erica Melis⋆, Martin Pollet, Volker Sorge · Formal Aspects of Computing · 1999
Abstract. The capabilities of a automated theorem prover's interface are essential for the effective use of (interactive) proof systems. L Ω UI is the multi-modal interface that combines several features: a graphical display of information in a proof graph, a selective term browser with hypertext facilities, proof and proof plan presentation in natural language, and an editor for adding and maintaining the knowledge base. L Ω UI is realized in an agent-based client-server architecture and implemented in the concurrent constraint programming language Oz.