A computer model for axiomatic systems

Date
1977
Authors
Ibrahim, Rosalind L.
Contributor
Advisor
Department
Instructor
Depositor
Speaker
Researcher
Consultant
Interviewer
Annotator
Journal Title
Journal ISSN
Volume Title
Publisher
Volume
Number/Issue
Starting Page
Ending Page
Alternative Title
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
Keywords
Automatic theorem proving, Problem solving, Artificial intelligence, Logic, Symbolic and mathematical
Citation
Extent
Format
Geographic Location
Time Period
Related To
Theses for the degree of Doctor of Philosophy (University of Hawaii at Manoa). Electrical Engineering; no. 1016
Table of Contents
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.
Rights Holder
Local Contexts
Email libraryada-l@lists.hawaii.edu if you need this content in ADA-compliant format.