ScholarSpace will be brought offline for upgrades on Wednesday December 9th at 11AM HST. Service will be disrupted for approximately 2 hours. Please direct any questions to

Item Description

Show full item record

Title: A computer model for axiomatic systems 
Author: Ibrahim, Rosalind L.
Date: 1977
Abstract: This dissertation describes the development of a computer system that can be used for informal axiomatic investigation of mathematics. A formal mathematics-like language is defined which enables a mathematician to write informal mathematical statements and proofs. Each step of a proof is checked for logical validity, and a user may develop and retain a system of axioms, theorems, dependencies and proofs written in this language. The intended user initially is a college mathematics student, who would use this system to develop proof-writing skills. The language is an LALR(l) language parsed by a simulated pushdown transducer. Although no rules of inference are ever mentioned explicitly in the input language, the rules of natural deduction are accommodated through the block structure and other features of the language. A proof step is represented as a mathematical statement and a (possibly null) list of reasons which are references to other proof steps or to axioms or previous theorems. Proof steps are translated to predicate calculus and then to clause form as the conjunction of the reasons and the negation of the statement. A resolution-based theorem prover, working in first-order logic without equality, seeks to verify each step. The system is basically sound and has been used on a limited experimental basis for proofs in group theory, number theory and set theory. The language appears to be versatile and easy to use. The major problems have arisen regarding axiom selection and dealing with equality. Future plans include building in equality and developing lesson plans.
Description: Typescript. Thesis (Ph. D.)--University of Hawaii at Manoa, 1977. Bibliography: leaves 172-175. Microfiche. vii, 175 leaves ill
Rights: All UHM dissertations and theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission from the copyright owner.
Keywords: Automatic theorem proving, Problem solving, Artificial intelligence, Logic, Symbolic and mathematical

Item File(s)

Description Files Size Format View
Restricted for viewing only uhm_phd_7801048_r.pdf 4.437Mb PDF View/Open
For UH users only uhm_phd_7801048_uh.pdf 4.390Mb PDF View/Open

This item appears in the following Collection(s)


Advanced Search


My Account