{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:24:17Z","timestamp":1761611057342},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[1999,9,1]],"date-time":"1999-09-01T00:00:00Z","timestamp":936144000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[1999,9]]},"abstract":"<jats:title>Abstract.<\/jats:title>\n          <jats:p>\n            The capabilities of a automated theorem prover's interface are essential for the effective use of (interactive) proof systems.\n            <jats:italic>L<\/jats:italic>\n            \u03a9\n            <jats:italic>UI<\/jats:italic>\n            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.\n            <jats:italic>L<\/jats:italic>\n            \u03a9\n            <jats:italic>UI<\/jats:italic>\n            is realized in an agent-based client-server architecture and implemented in the concurrent constraint programming language Oz.\n          <\/jats:p>","DOI":"10.1007\/s001650050053","type":"journal-article","created":{"date-parts":[[2002,8,25]],"date-time":"2002-08-25T09:25:39Z","timestamp":1030267539000},"page":"326-342","source":"Crossref","is-referenced-by-count":23,"title":["L\u03a9UI: Lovely \u03a9MEGA User Interface"],"prefix":"10.1145","volume":"11","author":[{"given":"J\u00f6rg","family":"Siekmann","sequence":"first","affiliation":[{"name":"FB Informatik, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany, , , , , , DE"}]},{"given":"Stephan","family":"Hess","sequence":"additional","affiliation":[{"name":"FB Informatik, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany, , , , , , DE"}]},{"given":"Christoph","family":"Benzm\u00fcller","sequence":"additional","affiliation":[{"name":"FB Informatik, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany, , , , , , DE"}]},{"given":"Lassaad","family":"Cheikhrouhou","sequence":"additional","affiliation":[{"name":"FB Informatik, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany, , , , , , DE"}]},{"given":"Armin","family":"Fiedler","sequence":"additional","affiliation":[{"name":"FB Informatik, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany, , , , , , DE"}]},{"given":"Helmut","family":"Horacek","sequence":"additional","affiliation":[{"name":"FB Informatik, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany, , , , , , DE"}]},{"given":"Michael","family":"Kohlhase","sequence":"additional","affiliation":[{"name":"FB Informatik, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany, , , , , , DE"}]},{"given":"Karsten","family":"Konrad","sequence":"additional","affiliation":[{"name":"FB Informatik, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany, , , , , , DE"}]},{"given":"Andreas","family":"Meier","sequence":"additional","affiliation":[{"name":"FB Informatik, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany, , , , , , DE"}]},{"given":"Erica","family":"Melis","sequence":"additional","affiliation":[{"name":"FB Informatik, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany, , , , , , DE"}]},{"given":"Martin","family":"Pollet","sequence":"additional","affiliation":[{"name":"FB Informatik, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany, , , , , , DE"}]},{"given":"Volker","family":"Sorge","sequence":"additional","affiliation":[{"name":"FB Informatik, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany, , , , , , DE"}]}],"member":"320","reference":[{"key":"p_1","doi-asserted-by":"crossref","first-page":"252","DOI":"10.1007\/3-540-63104-6_23","volume-title":"Proceedings of the 14th Conference on Automated Deduction, number1249 in LNAI","author":"Benzm\u00fcller C.","year":"1997"},{"key":"p_2","volume-title":"ISSAC'97","author":"Buchberger B.","year":"1997"},{"key":"p_3","first-page":"139","volume-title":"Kirchner and Kirchner [KiK98]","author":"Be"},{"key":"p_4","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1007\/3-540-57887-0_94","article-title":"Proof by Pointing","volume":"789","author":"Bertot Y.","year":"1994","journal-title":"Theoretical Aspects of Computer Software"},{"key":"p_5","volume-title":"Proceedings of the Workshop on User Interfaces for Theorem Provers, number98\/08 in Computing Science Reports, Eindhoven, the Netherlands","author":"Bac","year":"1998"},{"key":"p_6","volume-title":"R.: Natural Deduction Displays of Sequent Proofs: Experience with the Jape Calculator. In First International Workshop on Proof Transformation and Presentation","author":"Bor","year":"1997"},{"key":"p_7","volume-title":"Systems","author":"Be","year":"1998"},{"key":"p_9","volume-title":"Proceedings of 8th International Conference on Artificial Intelligence: Methodology, Systems, Applications (AIMSA'98)","author":"Ch","year":"1998"},{"key":"p_10","first-page":"91","volume-title":"Inference Mechanisms in Knowledge-Based Systems: Theory and Application (Proceedings of WS at KI'98), Fachberichte INFORMATIK 19\/98","author":"Che","year":"1998"},{"key":"p_11","first-page":"75","volume-title":"Using ILF as a User Interface for Many Theorem Provers","author":"Dah"},{"key":"p_12","first-page":"67","volume-title":"Proceedings of the 4th European Workshop on Natural Language Generation","author":"Da","year":"1993"},{"key":"p_13","first-page":"96","volume-title":"Support for Interactive Theorem Proving: Some Design Principles and Their Application","author":"Eas"},{"key":"p_14","volume-title":"First International Workshop on Proof Transformation and Presentation","author":"Eu","year":"1997"},{"issue":"3","key":"p_15","first-page":"156","article-title":"Agent-oriented integration of distributed mathematical services","volume":"5","author":"Franke A.","year":"1999","journal-title":"Journal of Universal Computer Science"},{"key":"p_16","volume-title":"System description: MathWeb, an agent-based communication layer for distributed automated theorem proving. to appear in CADE'99","author":"Fr","year":"1999"},{"key":"p_17","first-page":"216","volume-title":"Design and Implementation of Symbolic Computation Systems, DISCO'96, number1128 in LNCS","author":"Ho","year":"1996"},{"key":"p_18","first-page":"221","volume-title":"Proceedings of the 13th Conference on Automated Deduction, number1104 in LNAI","author":"Hu","year":"1996"},{"key":"p_19","volume-title":"Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI)","author":"Hu","year":"1997"},{"key":"p_20","volume-title":"Verification support environment. High Integrity Systems, 1(6)","author":"Hutter D.","year":"1996"},{"key":"p_21","volume-title":"National Conference on Artificial Intelligence (AAAI-99)","author":"Holland-Minkley A. M.","year":"1999"},{"key":"p_23","volume-title":"International Workshop on User Interface Design for Theorem Proving Systems","author":"Hu","year":"1996"},{"key":"p_24","volume-title":"Computational Linguistics","author":"Ki","year":"1995"},{"key":"p_25","volume-title":"Proceedings of the 15th Conference on Automated Deduction, number1421 in LNAI","author":"Ki","year":"1998"},{"key":"p_26","volume-title":"Journal of Automated Reasoning","author":"Kerber M.","year":"1998"},{"key":"p_28","volume-title":"M","author":"Met","year":"1992"},{"key":"p_29","first-page":"494","volume-title":"European Conference on Artificial Intelligence (ECAI-98)","author":"Mel","year":"1998"},{"key":"p_30","volume-title":"9th International Conference on Artificial Intelligence in Education, AI-ED'99","author":"Me","year":"1999"},{"key":"p_31","volume-title":"International Workshop on User Interface Design for Theorem Proving Systems","author":"Po","year":"1995"},{"key":"p_32","volume-title":"Getting Computers to Talk Like You and Me","author":"Rei","year":"1985"},{"key":"p_33","first-page":"163","volume-title":"Proceedings of the 7th International Workshop on Natural Language Generation","author":"Rei","year":"1994"},{"key":"p_34","first-page":"139","volume-title":"Kirchner and Kirchner [KiK98]","author":"Richardson J."},{"key":"p_35","volume-title":"Designing the User Interface","author":"Shn","year":"1992"},{"key":"p_36","first-page":"324","volume-title":"J. v","author":"Smo","year":"1995"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s001650050053.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s001650050053\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s001650050053","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:36:13Z","timestamp":1641483373000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s001650050053"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,9]]},"references-count":33,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1999,9]]}},"alternative-id":["10.1007\/s001650050053"],"URL":"https:\/\/doi.org\/10.1007\/s001650050053","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1999,9]]}}}