Xlsabelle: A Graphical User Interface to the Isabelle Theorem Prover.

Abstract

Interactive theorem provers such as Isabelle are powerful tools, but are difficult and time-consuming to learn. If a suitable Graphical User Interface (GUI) is provided for such a tool, it can speed up the learning process considerably, leading to greater productivity for users of the tool, and increased takeup in industry. In this paper, we discuss the user-interface aspects of Isabelle, and formulate requirements for a GUI. XIsabelle, a GUI for XIsabelle, is described in detail. XIsabelle uses standard, easily available, methods for providing X Windows wrappers to interactive non-GUI programs, namely Tcl/Tk and the program Expect.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Dec 01, 1995
Accession Number
ADA307301

Entities

People

  • A. Cant
  • M. A. Ozols

Organizations

  • Defence Science and Technology Group

Tags

Communities of Interest

  • C4I
  • Human Systems
  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Australia
  • Computer Programming
  • Computer Programs
  • Computers
  • Directories
  • Electronics
  • Engineering
  • Engineers
  • Graphical User Interface
  • Human Systems Integration
  • Language
  • Law
  • New Jersey
  • Software Development
  • United States
  • User Interface
  • Word Processors

Fields of Study

  • Computer science

Readers

  • Database Systems and Applications
  • Manufacturing Engineering.