Answer Extraction In Automated Reasoning

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\u27s 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\u27s 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\u27s set of answers and the extracted set of answers