Automated reasoning and machine learning

dc.contributor.author Huang, Guoxiang en_US
dc.date.accessioned 2009-07-15T17:59:30Z
dc.date.available 2009-07-15T17:59:30Z
dc.date.issued 1996 en_US
dc.description Thesis (Ph. D.)--University of Hawaii at Manoa, 1996. en_US
dc.description Includes bibliographical references (leaves 140-144). en_US
dc.description Microfiche. en_US
dc.description x, 144 leaves, bound ill. 29 cm en_US
dc.description.abstract This dissertation introduces new theorem-proving strategies and uses these strategies to solve a wide variety of difficult problems requiring logical reasoning. It also shows how to use theorem-proving to solve the problem of learning mathematical concepts. Our first algorithm constructs formulas called Craig interpolants from the refutation proofs generated by contemporary theorem-provers using binary resolution, paramodulation, and factoring. This algorithm can construct the formulas needed to learn concepts expressible in the full first-order logic from examples of the concept. It can also find sentences which distinguish pairs of nonisomorphic finite structures. We then apply case analysis to solve hard problems such as the zebra problem, the pigeonhole problem, and the stable marriage problem. The case analysis technique we use is the first to be fully compatible with resolution and rewriting and powerful enough to solve these problems. Our primary new theorem-proving strategies generate subgoals and efficient sets of rules. We show how to divide problems into smaller parts with intermediate goals by reversing logical implications. We solve these subdivided parts by discovering efficient subsets of rules or by generating efficient new rules. We apply these and other new search strategies to solve difficult problems such as the 15-puzzle, central solitaire, TopSpin, Rubik's cube, and masterball. Our strategies apply universally to all such problems and can solve them quite efficiently: the 15-puzzle, Rubik's cube and masterball can all be done in 300 seconds. Finally we apply our search strategies to solve real-world problems such as sorting, solving equations and inverting nonsingular matrices. en_US
dc.identifier.uri http://hdl.handle.net/10125/9963
dc.language.iso en-US en_US
dc.relation Theses for the degree of Doctor of Philosophy (University of Hawaii at Manoa). Mathematics; no. 3315 en_US
dc.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. en_US
dc.subject Automatic theorem proving en_US
dc.subject Logic, Symbolic and mathematical en_US
dc.subject Artificial intelligence en_US
dc.title Automated reasoning and machine learning en_US
dc.type Thesis en_US
dc.type.dcmi Text en_US
Files
Original bundle
Now showing 1 - 2 of 2
No Thumbnail Available
Name:
uhm_phd_9629830_uh.pdf
Size:
3.32 MB
Format:
Adobe Portable Document Format
Description:
Version for UH users
No Thumbnail Available
Name:
uhm_phd_9629830_r.pdf
Size:
3.37 MB
Format:
Adobe Portable Document Format
Description:
Version for non-UH users. Copying/Printing is not permitted