[go: up one dir, main page]

Aitken et al., 1998 - Google Patents

Interactive theorem proving: An empirical study of user activity

Aitken et al., 1998

View PDF
Document ID
7751605508317886918
Author
Aitken J
Gray P
Melham T
Thomas M
Publication year
Publication venue
Journal of Symbolic Computation

External Links

Snippet

In this paper the interaction between users and the interactive theorem prover HOL is investigated from a human–computer interaction perspective. First, we outline three possible views of interaction, and give a brief survey of some current interfaces and how they may be …
Continue reading at www.sciencedirect.com (PDF) (other versions)

Classifications

    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F8/00—Arrangements for software engineering
    • G06F8/30—Creation or generation of source code
    • G06F8/34—Graphical or visual programming
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/30—Information retrieval; Database structures therefor; File system structures therefor
    • G06F17/30286—Information retrieval; Database structures therefor; File system structures therefor in structured data stores
    • G06F17/30386—Retrieval requests
    • G06F17/30389—Query formulation
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/20—Handling natural language data
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06N—COMPUTER SYSTEMS BASED ON SPECIFIC COMPUTATIONAL MODELS
    • G06N5/00—Computer systems utilising knowledge based models
    • G06N5/02—Knowledge representation
    • G06N5/022—Knowledge engineering, knowledge acquisition
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
    • G06F17/50—Computer-aided design
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06Q—DATA PROCESSING SYSTEMS OR METHODS, SPECIALLY ADAPTED FOR ADMINISTRATIVE, COMMERCIAL, FINANCIAL, MANAGERIAL, SUPERVISORY OR FORECASTING PURPOSES; SYSTEMS OR METHODS SPECIALLY ADAPTED FOR ADMINISTRATIVE, COMMERCIAL, FINANCIAL, MANAGERIAL, SUPERVISORY OR FORECASTING PURPOSES, NOT OTHERWISE PROVIDED FOR
    • G06Q10/00—Administration; Management
    • G06Q10/10—Office automation, e.g. computer aided management of electronic mail or groupware; Time management, e.g. calendars, reminders, meetings or time accounting
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F8/00—Arrangements for software engineering
    • G06F8/10—Requirements analysis; Specification techniques
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F9/00—Arrangements for programme control, e.g. control unit
    • G06F9/06—Arrangements for programme control, e.g. control unit using stored programme, i.e. using internal store of processing equipment to receive and retain programme
    • G06F9/44—Arrangements for executing specific programmes
    • G06F9/4443—Execution mechanisms for user interfaces
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06Q—DATA PROCESSING SYSTEMS OR METHODS, SPECIALLY ADAPTED FOR ADMINISTRATIVE, COMMERCIAL, FINANCIAL, MANAGERIAL, SUPERVISORY OR FORECASTING PURPOSES; SYSTEMS OR METHODS SPECIALLY ADAPTED FOR ADMINISTRATIVE, COMMERCIAL, FINANCIAL, MANAGERIAL, SUPERVISORY OR FORECASTING PURPOSES, NOT OTHERWISE PROVIDED FOR
    • G06Q10/00—Administration; Management
    • G06Q10/06—Resources, workflows, human or project management, e.g. organising, planning, scheduling or allocating time, human or machine resources; Enterprise planning; Organisational models
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F11/00—Error detection; Error correction; Monitoring
    • G06F11/36—Preventing errors by testing or debugging software
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F19/00—Digital computing or data processing equipment or methods, specially adapted for specific applications
    • Y—GENERAL TAGGING OF NEW TECHNOLOGICAL DEVELOPMENTS; GENERAL TAGGING OF CROSS-SECTIONAL TECHNOLOGIES SPANNING OVER SEVERAL SECTIONS OF THE IPC; TECHNICAL SUBJECTS COVERED BY FORMER USPC CROSS-REFERENCE ART COLLECTIONS [XRACs] AND DIGESTS
    • Y10—TECHNICAL SUBJECTS COVERED BY FORMER USPC
    • Y10S—TECHNICAL SUBJECTS COVERED BY FORMER USPC CROSS-REFERENCE ART COLLECTIONS [XRACs] AND DIGESTS
    • Y10S715/00—Data processing: presentation processing of document, operator interface processing, and screen saver display processing
    • Y10S715/961—Operator interface with visual structure or function dictated by intended use
    • Y10S715/965—Operator interface with visual structure or function dictated by intended use for process control and configuration
    • Y10S715/966—Computer process, e.g. operation of computer
    • Y—GENERAL TAGGING OF NEW TECHNOLOGICAL DEVELOPMENTS; GENERAL TAGGING OF CROSS-SECTIONAL TECHNOLOGIES SPANNING OVER SEVERAL SECTIONS OF THE IPC; TECHNICAL SUBJECTS COVERED BY FORMER USPC CROSS-REFERENCE ART COLLECTIONS [XRACs] AND DIGESTS
    • Y10—TECHNICAL SUBJECTS COVERED BY FORMER USPC
    • Y10S—TECHNICAL SUBJECTS COVERED BY FORMER USPC CROSS-REFERENCE ART COLLECTIONS [XRACs] AND DIGESTS
    • Y10S707/00—Data processing: database and file management or data structures
    • Y10S707/99941—Database schema or data structure
    • Y10S707/99943—Generating database or data structure, e.g. via user interface

Similar Documents

Publication Publication Date Title
Rolland et al. A proposal for a scenario classification framework
Rieman et al. A dual-space model of iteratively deepening exploratory learning
US5720007A (en) Expert system and method employing hierarchical knowledge base, and interactive multimedia/hypermedia applications
JP2002197245A (en) Work process model creation system
Motta et al. Methodological foundations of KEATS, the knowledge engineer's assistant
Aitken et al. Interactive theorem proving: An empirical study of user activity
US7895219B2 (en) System and method for guided and assisted structuring of unstructured information
Blandford et al. Models of interactive systems: a case study on programmable user modelling
Wang et al. Data Formulator 2: Iterative Creation of Data Visualizations, with AI Transforming Data Along the Way
Murray et al. A framework for describing visual interfaces to databases
Baron et al. SUIDT: A task model based GUI-Builder
Dengler et al. Wiki-based maturing of process descriptions
Olsen Jr et al. Research directions for user interface software tools
Wrobel Design goals for sloppy modeling systems
Rhyne et al. Tools and methodology for user interface development
Luo A human-computer collaboration paradigm for bridging design conceptualization and implementation
Moher et al. Monolingual, articulated modeling of users, devices, and interfaces
Bramwell et al. Exploring design options rationally
Puerta et al. Toward ontology-based frameworks for knowledge-acquisition tools
Eriksson Models for knowledge-acquisition tool design
Kim et al. Building a Rule-Based Goal-Model from the IEC 62304 Standard for Medical Device Software.
Kitajima et al. LICAI+: A comprehension-based model of the recall of action sequences
Singh Graphical support for programming: A survey and taxonomy
Lethbridge et al. Integrating techniques for conceptual modeling
Dickson Utilization of Deep Learning for the Automatic Classification of Software Aspects