Off-campus University of Miami users: To download campus access theses, please use the following link to log into our proxy server with your University of Miami CaneID and Password.

Non-University of Miami users: Please talk to your librarian about requesting this thesis through interlibrary loan.

Publication Date

2008-01-01

Availability

UM campus only

Degree Type

Thesis

Degree Name

Master of Science (MS)

Department

Computer Science (Arts and Sciences)

Date of Defense

2008-11-13

First Committee Member

Geoff Sutcliffe - Committee Chair

Second Committee Member

Burton Rosenberg - Committee Member

Third Committee Member

Otavio Bueno - Committee Member

Abstract

One aspect of Automated Reasoning (AR) deals with writing computer programs that can answer questions using logical reasoning. An Automated Theorem Proving system (ATP system) translates a question to be answered to a first-order logic conjecture, and attempts to prove the conjecture from a set of axioms provided, thereby leading to a proof. If a proof is found an answer extraction method can be applied to answer the original question. If more than one proof is possible, more than one answer may need to be extracted. For ATP systems that can find only one answer at a time, to answer questions that yield multiple answers, the ATP system can be re-invoked with a modified question to find other possible answers. In this thesis, an answer extraction method has been designed to extract more than one answer when an ATP system is used to answer a question that has multiple answers. The method is implemented in an interactive computer program and the process is called multiple-answer extraction. The answer extraction software, called the multi-answer system, is a three layered software architecture model. SNARK, at the bottom-most layer, serves as the ATP system that finds single answers. The answer extractor, in the middle layer, extracts possible answers by re-invoking the ATP system. The top layer compares the answers extracted to the user's expected answers. The software is command line driven. Keywords such as all, some, n (where n is a number), while and until are specified on the command line to limit the number of answers to be extracted. The top layer allows the user to check properties of the answer, e.g., if a specific element belongs to the set of answers obtained, or if the user's set of answers is a subset of the answers returned by the multi-answer system. This is done using set operations, such as subset, element of, union, difference, intersection, on the user's set of answers and the extracted set of answers.

Keywords

Automated Reasoning

Share

COinS