Please use this identifier to cite or link to this item:

A computer model for axiomatic systems

File Description SizeFormat 
uhm_phd_7801048_uh.pdfVersion for UH users4.5 MBAdobe PDFView/Open
uhm_phd_7801048_r.pdfVersion for non-UH users. Copying/Printing is not permitted4.54 MBAdobe PDFView/Open

Item Summary

Title: A computer model for axiomatic systems
Authors: Ibrahim, Rosalind L.
Keywords: Automatic theorem proving
Problem solving
Artificial intelligence
Logic, Symbolic and mathematical
Issue 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.
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.
Appears in Collections:Ph.D. - Electrical Engineering

Please contact if you need this content in an alternative format.

Items in ScholarSpace are protected by copyright, with all rights reserved, unless otherwise indicated.