Solid Intuition/Literature

From SE Wiki
Jump to: navigation, search

User Interaction

Pie Menus

  • Callahan J., Hopkins D., Weiser M., Shneiderman B., An Empirical Comparison of Pie versus Linear Menus, Proceedings of CHI ‘88, (1988)
This one cites the following as "inventer" of pie menus:
  • Hopkins, D., Callahan, J., and Weiser, M. Pies: Implementation, Evaluation and Application of Circular Menus. University of Maryland Computer Science Department Technical Report, 1988.
  • Hopkins D., The Design and Implementation of the Pie Menus, Dr Dobb's Journal, December,


  • Martin S Dulberg, Robert St Amant & Luke S Zettlemoyer, An Imprecise Mouse Gesture for the Fast Activation of Controls, in: Angela Sasse and Chris Johnson (Editors), Human–Computer Interaction — INTERACT’99, IOS Press, 1999 ((c) IFIP TC.13)
Introduces the notion of a "flick" which is the use of a pie menu without actually showing the menu.
  • Shengdong Zhao, Ravin Balakrishnan, Simple vs. Compound Mark Hierarchical Marking Menus, ACM UIST Symposium on User Interface Software and Technology, 2004
Quote: Marking menus [6] are a variant of pie or radial menus [4, 12] that allow a user to perform a menu selection by either selecting an item from a popup radial menu, or by making a straight mark in the direction of the desired menu item without popping-up the menu. As with linear menus, marking menus can also support menu hierarchies, where users make “zig-zag” compound marks to select from multiple levels of submenus (Figure 1a). Extensive research [6, 7, 11] has shown that marking menus have significant advantages over regular pie/radial menus and linear menus, including support for seamless transition from novice to expert usage, and selection speeds up to 3.5 times faster.
  • Tapia, M., & Kurtenbach, G. (1995). Some design refinements and principles on the appearance and behavior of marking menus. ACM UIST Symposium on User Interface Software and Technology. p. 189-195.
  • Kurtenbach, G., & Buxton, W. (1993). The limits of expert performance using hierarchical marking menus. ACM CHI Conference on Human Factors in Computing Systems. p. 35-42.
  • George Fitzmaurice, Azam Khan, Robert Pieké, Bill Buxton, Gordon Kurtenbach, Tracking menus, UIST, 2003
Quote: We describe a new type of graphical user interface widget, known as a “tracking menu. ” A tracking menu consists of a cluster of graphical buttons, and as with traditional menus, the cursor can be moved within the menu to select and interact with items. However, unlike traditional menus, when the cursor hits the edge of the menu, the menu moves to continue tracking the cursor. Thus, the menu always stays under the cursor and close at hand. In this paper we define the behavior of tracking menus, show unique affordances of the widget, present a variety of examples, and discuss design characteristics.


  • Richard S. Bird: Small Specification Exercises

Intro: Sometimes it seems easier to construct a program of a problem than a suitable specification of the problem.

Refinement Tools

  • A Review of Existing Refinement Tools[1] David Carrington, Ian Hayes, et al., 1994
This paper compares two tools which work on the Refinement Calculus as defined by Carroll Morgan. Refinement rules are applied by the tools and the proof obligations are left to be done by a prover. Integration of prover and refinement tool is only discussed abstractly as a wish for the future.


  • YET_TO_READ: Manfred Kerber: "Proof Planning: A Practical Approach to Mechanized Reasoning in Mathemtics"

The attempt to mechanize mathematical reasoning belongs to the first experiments in artificial intelligence in the 1950 (Newell et al., 1957). However, the idea to automate or to support deduction turned out to be harder than originally expected. This can not at least be seen in the multitude of approaches that were pursued to model different aspects of mathematical reasoning. There are different dimension according to which these systems can be classified: input language (e.g., order-sorted first-order logic), calculus (e.g., resolution), interaction level (e.g., batch mode), proof output (e.g., refutation graph), and the purpose (e.g., automated theorem proving) as well as many more subtle points concerning the fine tuning of the proof search.

In this contribution the proof planning approach will be presented. Since it is not the mainstream approach to mechanized reasoning, it seems to be worth to look at it in a more principled way and to contrast it to other approaches. In order to do so I categorize the systems according to their purpose. The different attempts can be roughly categorized into three classes: machine-oriented automated theorem provers, interactive proof checkers, and human-oriented theorem provers. In the rest of the introduction we shall take a closerlook at these different categories.

  • PVS: A Prototype Verification System, (1992 paper)

Quote: Although we are reasonably satisfied that PVS is an effective tool for developing readable specifications and formal proofs with considerable human efficiency, we are sill significantly short of our goal of employing mechanization to produce proofs that humans find truly perspicuous.

  • Notes on PVS from a HOL perspective (Mike Gordon, 1995)
PVS is a tightly integrated and coherent system that is easy and fun to use. Compared with HOL it is much simpler to learn and (at least for beginners) much quicker at proving theorems.
There is an ‘engineering philosophy’ associated with PVS that emphasizes getting useful work done. HOL, perhaps because of its academic (ivory tower) origins, has historically placed more emphasis on logical foundations and less on usability.
  • ProofPower: a HOL88 based prover with support for Z. Typical X window and latex interface.

Logic and Presentation

Leslie Lamport: How to Write a Proof, 1993

Advocates semi-formal natural-deduction based proof with a nice abbreviation for proposition-numbers. becomes <4>2.

"I have also found structured proofs very helpful when I need a variant of an existing theorem, perhaps with a slightly weaker hypothesis. In a properly written proof, where every use of an assumption or a proof step is explicit, simple text searching reveals exactly where every hypothesis is used."

History of Logic

Quote from Leibniz: "La maniere d'enoncer vulgaire regarde plustost les individus, mais celle d'Aristote a plus d'egard aux idées ou universaux. Car disant ‘tout homme est animal’, je veux dire que tous les hommes sont compris dans tous les animaux; mais j'entends en même temps que l'idée de l'animal est comprise dans l'idée de l'homme. L'animal comprend plus d'individus que l'homme, mais l'homme comprend plus d'idées ou plus de formalités; l'un a plus d'exemples, l'autre plus de degrés de realité; l'un a plus d'extension, l'autre plus d'intension."
I like to replace homme/animal with bool/number and thus obtain a statement that talks about Rick's Unified Algebra.