[go: up one dir, main page]

Pitt, 1995 - Google Patents

MacKE: Yet another proof assistant & automated pedagogic tool

Pitt, 1995

View PDF
Document ID
3132937643724133839
Author
Pitt J
Publication year
Publication venue
International Workshop on Theorem Proving with Analytic Tableaux and Related Methods

External Links

Snippet

In this paper, we describe the implementation of (yet another) proof assistant and/or automated pedagogic tool. This one is based on the calculus KE and our Prolog implementation of free variable KE. The new system is written in LPA MacProlog™, and …
Continue reading at www.researchgate.net (PDF) (other versions)

Classifications

    • 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
    • G06F17/21—Text processing
    • G06F17/24—Editing, e.g. insert/delete
    • 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/30943—Information retrieval; Database structures therefor; File system structures therefor details of database functions independent of the retrieved data type
    • G06F17/30994—Browsing or visualization
    • 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/30943—Information retrieval; Database structures therefor; File system structures therefor details of database functions independent of the retrieved data type
    • G06F17/30946—Information retrieval; Database structures therefor; File system structures therefor details of database functions independent of the retrieved data type indexing structures
    • 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/10—Complex mathematical operations
    • 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
    • G06F17/5009—Computer-aided design using simulation
    • 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
    • G09—EDUCATION; CRYPTOGRAPHY; DISPLAY; ADVERTISING; SEALS
    • G09B—EDUCATIONAL OR DEMONSTRATION APPLIANCES; APPLIANCES FOR TEACHING, OR COMMUNICATING WITH, THE BLIND, DEAF OR MUTE; MODELS; PLANETARIA; GLOBES; MAPS; DIAGRAMS
    • G09B7/00—Electrically-operated teaching apparatus or devices working with questions and answers
    • G09B7/02—Electrically-operated teaching apparatus or devices working with questions and answers of the type wherein the student is expected to construct an answer to the question which is presented or wherein the machine gives an answer to the question presented by a student
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06T—IMAGE DATA PROCESSING OR GENERATION, IN GENERAL
    • G06T11/00—2D [Two Dimensional] image generation
    • G06T11/20—Drawing from basic elements, e.g. lines or circles
    • G06T11/206—Drawing of charts or graphs
    • G—PHYSICS
    • G09—EDUCATION; CRYPTOGRAPHY; DISPLAY; ADVERTISING; SEALS
    • G09B—EDUCATIONAL OR DEMONSTRATION APPLIANCES; APPLIANCES FOR TEACHING, OR COMMUNICATING WITH, THE BLIND, DEAF OR MUTE; MODELS; PLANETARIA; GLOBES; MAPS; DIAGRAMS
    • G09B23/00—Models for scientific, medical, or mathematical purposes, e.g. full-sized devices for demonstration purposes
    • G09B23/28—Models for scientific, medical, or mathematical purposes, e.g. full-sized devices for demonstration purposes for medicine
    • G—PHYSICS
    • G09—EDUCATION; CRYPTOGRAPHY; DISPLAY; ADVERTISING; SEALS
    • G09B—EDUCATIONAL OR DEMONSTRATION APPLIANCES; APPLIANCES FOR TEACHING, OR COMMUNICATING WITH, THE BLIND, DEAF OR MUTE; MODELS; PLANETARIA; GLOBES; MAPS; DIAGRAMS
    • G09B5/00—Electrically-operated educational appliances
    • G09B5/02—Electrically-operated educational appliances with visual presentation of the material to be studied, e.g. using film strip
    • G—PHYSICS
    • G06—COMPUTING; CALCULATING; COUNTING
    • G06N—COMPUTER SYSTEMS BASED ON SPECIFIC COMPUTATIONAL MODELS
    • G06N5/00—Computer systems utilising knowledge based models
    • 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
    • G06F—ELECTRICAL DIGITAL DATA PROCESSING
    • G06F3/00—Input arrangements for transferring data to be processed into a form capable of being handled by the computer; Output arrangements for transferring data from processing unit to output unit, e.g. interface arrangements
    • G06F3/01—Input arrangements or combined input and output arrangements for interaction between user and computer
    • G06F3/048—Interaction techniques based on graphical user interfaces [GUI]
    • G—PHYSICS
    • G09—EDUCATION; CRYPTOGRAPHY; DISPLAY; ADVERTISING; SEALS
    • G09B—EDUCATIONAL OR DEMONSTRATION APPLIANCES; APPLIANCES FOR TEACHING, OR COMMUNICATING WITH, THE BLIND, DEAF OR MUTE; MODELS; PLANETARIA; GLOBES; MAPS; DIAGRAMS
    • G09B19/00—Teaching not covered by other main groups of this subclass

Similar Documents

Publication Publication Date Title
US5469538A (en) Mathematical document editor and method performing live symbolic calculations for use with an electronic book
Santhanam et al. Improving end-user proficiency: Effects of conceptual training and nature of interaction
Mumtaz et al. Exploranative code quality documents
Graham et al. ClockWorks: Visual programming of component-based software architectures
Macías et al. An authoring tool for building adaptive learning guidance systems on the web
Billingsley et al. Student proof exercises using MathsTiles and Isabelle/HOL in an intelligent book
Pitt MacKE: Yet another proof assistant & automated pedagogic tool
McDonald Interactive pushdown automata animation
Huber et al. HyperCOSTOC: a comprehensive computer-based teaching support system
Paternò Tools for Task Modelling: Where we are, Where we are headed.
Brey Temporal network analysis with R
Blessing A programming by demonstration authoring tool for model-tracing tutors
Pitt Automated Pedagogic Tool
Moreno et al. Interactive visualization of dependencies
Desmarais et al. The diagnosis of user strategies
Shi et al. An integrated framework of generating quizzes based on linked data and its application on medical education field
Thompson Student modeling in an intelligent tutoring system
Kaltenbach et al. Dynaboard: User animated display of deductive proofs in mathematics
Aris Object-oriented programming semantics representation utilizing agents
Jerinic et al. The EduSof Intelligent Tutoring System
Atolagbe et al. A generic architecture for intelligent instruction for simulation modelling software packages
Zheliazkova An intelligent system for teaching and learning algorithms
Williams et al. Comparison of visual and textual languages via task modeling
Klar et al. InterACT: An interactive theorem and completeness prover for algebraic specifications with conditional equations
Eisenstadt et al. A Fine-Grained Account of Prolog Execution for Teaching and Debugging 1