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.

Cited By

View all

Jakubův JKaliszyk C(2023)VizAR: Visualization of Automated Reasoning Proofs (System Description)Intelligent Computer Mathematics10.1007/978-3-031-42753-4_22(303-308)Online publication date: 4-Sep-2023
https://dl.acm.org/doi/10.1007/978-3-031-42753-4_22
Melcer DChang S(2021)ProofViz: An Interactive Visual Proof ExplorerTrends in Functional Programming10.1007/978-3-030-83978-9_6(116-135)Online publication date: 17-Feb-2021
https://dl.acm.org/doi/10.1007/978-3-030-83978-9_6
Jackson P(2021)Dynamic Proof PresentationMathematical Reasoning: The History and Impact of the DReaM Group10.1007/978-3-030-77879-8_4(63-86)Online publication date: 24-May-2021
https://doi.org/10.1007/978-3-030-77879-8_4
Show More Cited By

Index Terms

LΩUI: Lovely ΩMEGA User Interface

Index terms have been assigned to the content through auto-classification.

Recommendations

The University of Alberta user interface management system

In this paper the design and implementation of the University of Alberta user interface management system (UIMS) is discussed. This UIMS is based on the Seeheim model of user interfaces, which divides the user interface into three separate components. ...
The University of Alberta user interface management system
SIGGRAPH '85: Proceedings of the 12th annual conference on Computer graphics and interactive techniques

In this paper the design and implementation of the University of Alberta user interface management system (UIMS) is discussed. This UIMS is based on the Seeheim model of user interfaces, which divides the user interface into three separate components. ...
A Dialog-Oriented User Interface Generation Mechanism
APSEC '96: Proceedings of the Third Asia-Pacific Software Engineering Conference

Nowadays, for GUI application development, there are a number of interface builders, which make it possible for the user to create user interfaces easily, and UIMSs, which help to specify and design user interfaces. However, interface builders lack the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

Formal Aspects of Computing Volume 11, Issue 3

Sep 1999

135 pages

ISSN:0934-5043

EISSN:1433-299X

Issue’s Table of Contents

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 September 1999

Published in FAC Volume 11, Issue 3

Author Tag

Keywords: Automated deduction; Mathematics; User interface; Agents; Distributed Artificial Intelligence; Human Computer Interaction

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

23
Total Citations
View Citations
56
Total Downloads

Downloads (Last 12 months)28
Downloads (Last 6 weeks)6

Reflects downloads up to 20 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Jakubův JKaliszyk C(2023)VizAR: Visualization of Automated Reasoning Proofs (System Description)Intelligent Computer Mathematics10.1007/978-3-031-42753-4_22(303-308)Online publication date: 4-Sep-2023
https://dl.acm.org/doi/10.1007/978-3-031-42753-4_22
Melcer DChang S(2021)ProofViz: An Interactive Visual Proof ExplorerTrends in Functional Programming10.1007/978-3-030-83978-9_6(116-135)Online publication date: 17-Feb-2021
https://dl.acm.org/doi/10.1007/978-3-030-83978-9_6
Jackson P(2021)Dynamic Proof PresentationMathematical Reasoning: The History and Impact of the DReaM Group10.1007/978-3-030-77879-8_4(63-86)Online publication date: 24-May-2021
https://doi.org/10.1007/978-3-030-77879-8_4
Ring MLüth C(2017)Interactive Proof Presentations with CobraElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.239.4239(43-52)Online publication date: 24-Jan-2017
https://doi.org/10.4204/EPTCS.239.4
Grov GLin Y(2017)The Tinker tool for graphical tactic developmentInternational Journal on Software Tools for Technology Transfer10.1007/s10009-017-0452-720:2(139-155)Online publication date: 17-Mar-2017
https://doi.org/10.1007/s10009-017-0452-7
Schuppan V(2016)Enhancing unsatisfiable cores for LTL with information on temporal relevanceTheoretical Computer Science10.1016/j.tcs.2016.01.014655:PB(155-192)Online publication date: 6-Dec-2016
https://dl.acm.org/doi/10.1016/j.tcs.2016.01.014
Grov GKissinger ALin Y(2014)Tinker, tailor, solver, proofElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.167.5167(23-34)Online publication date: 29-Oct-2014
https://doi.org/10.4204/EPTCS.167.5
Kieffer S(2014)Argument Mapping for Mathematics in ProofscapeDiagrammatic Representation and Inference10.1007/978-3-662-44043-8_10(57-63)Online publication date: 2014
https://doi.org/10.1007/978-3-662-44043-8_10
Aspinall DDenney ELüth C(2010)Tactics for Hierarchical ProofMathematics in Computer Science10.1007/s11786-010-0025-63:3(309-330)Online publication date: 10-Mar-2010
https://doi.org/10.1007/s11786-010-0025-6
Autexier SBenzmüller CDietrich DSiekmann J(2010)ΩMEGA: Resource-Adaptive Processes in an Automated Reasoning SystemResource-Adaptive Cognitive Processes10.1007/978-3-540-89408-7_17(389-423)Online publication date: 5-Feb-2010
https://doi.org/10.1007/978-3-540-89408-7_17
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Abstract.

Cited By

Index Terms

Recommendations

The University of Alberta user interface management system

The University of Alberta user interface management system

A Dialog-Oriented User Interface Generation Mechanism

Comments

Information

Published In

Publisher

Publication History

Author Tag

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

PDF

eReader

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations