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.

With the advent of reasoning problems in dynamic environments, there is an increasing need for automated reasoning systems to automatically adapt to unexpected changes in representations. In particular, the automation of the evolution of their ontologies needs to be enhanced without substantially sacrificing expressivity in the underlying representation. Revision of beliefs is not enough, as adding to or removing from beliefs does not change the underlying formal language. General reasoning systems employed in such environments should also address situations in which the language for representing knowledge is not shared among the involved entities, e.g., the ontologies in a multi-ontology environment or the agents in a multi-agent environment. Our techniques involve diagnosis of faults in existing, possibly heterogeneous, ontologies and then resolution of these faults by manipulating the signature and/or the axioms. This thesis describes the design, development and evaluation of GALILEO (Guided Analysis of Logical Inconsistencies Lead to Evolution of Ontologies), a system designed to detect conflicts in highly expressive ontologies and resolve the detected conflicts by performing appropriate repair operations. The integrated mechanism that handles ontology evolution is able to distinguish between various types of conflicts, each corresponding to a unique kind of ontological fault. We apply and develop our techniques in the domain of Physics. This an excellent domain because many of its seminal advances can be seen as examples of ontology evolution, i.e. changing the way that physicists perceive the world, and case studies are well documented – unlike many other domains. Our research covers analysing a wide ranging development set of case studies and evaluating the performance of the system on a test set. Because the formal representations of most of the case studies are non-trivial and the underlying logic has a high degree of expressivity, we face some tricky technical challenges, including dealing with the potentially large number of choices in diagnosis and repair. In order to enhance the practicality and the manageability of the ontology evolution process, GALILEO incorporates the functionality of generating physically meaningful diagnoses and repairs and, as a result, narrowing the search space to a manageable size.

No description available.

No description available.

Automated reasoning, and in particular automated theorem proving, has become a very important research field within the world of mathematics. Besides being used to verify proofs of theorems, it has also been used to discover proofs of theorems which were previously open problems. In this thesis, an automated reasoning assistant based on Godel's class theory is used to deduce several theorems.

No description available.

This doctoral thesis addresses one major difficulty in formal proof: removing obstructions to intuition which hamper the proof endeavour. We investigate this in the context of formally verifying geometric algorithms using the theorem prover Isabelle, by first proving the Graham’s Scan algorithm for finding convex hulls, then using the challenges we encountered as motivations for the design of a general, modular framework for combining mathematical tools. We introduce our integration framework — the Prover’s Palette, describing in detail the guiding principles from software engineering and the key differentiator of our approach — emphasising the role of the user. Two integrations are described, using the framework to extend Eclipse Proof General so that the computer algebra systems QEPCAD and Maple are directly available in an Isabelle proof context, capable of running either fully automated or with user customisation. The versatility of the approach is illustrated by showing a variety of ways that these tools can be used to streamline the theorem proving process, enriching the user’s intuition rather than disrupting it. The usefulness of our approach is then demonstrated through the formal verification of an algorithm for computing Delaunay triangulations in the Prover’s Palette.

No description available.

Search engines are the most popular tools for finding answers to questions, but unfortunately they do not always provide complete direct answers. Answers often need to be extracted by the user, from the web pages returned by the search engine. This research addresses this problem, and shows how an automated theorem prover, combined with existing ontologies and the web, is able to reason about world knowledge and return direct answers to users' questions. The use of an automated theorem prover also allows more complex questions to be asked. Automated theorem provers that exhibit these capabilities are called World Knowledge Reasoning systems. This research discusses one such system, the CNL-WKR system. The CNL-WKR system uses the ACE controlled natural language as its user-input language. It then calls upon external sources on the web, as well as internal ontological sources, during the theorem proving process, in order to find answers. The system uses the automated theorem prover, SPASS-XDB. The result is a system that is capable of answering complex questions about the world.

The thesis investigates methods for uniform interpolation in expressive description logics. Description logics are formalisms commonly used to model ontologies. Ontologies store terminological information and are used in a wide range of applications, such as the semantic web, medicine, bio-informatics, software development, data bases and language processing. Uniform interpolation eliminates terms from an ontology such that logical entailments in the remaining language are preserved. The result, the uniform interpolant, is a restricted view of the ontology that can be used for a variety of tasks such as ontology analysis, ontology reuse, ontology evolution and information hiding. Uniform interpolation for description logics has only gained an interest in the research community in the last years, and theoretical results show that it is a hard problem requiring specialised reasoning approaches. We present a range of uniform interpolation methods that can deal with expressive description logics such as ALC and many of its extensions. For all these logics, these are the first methods that are able to compute uniform interpolants for all inputs. The methods are based a new family of saturation-based reasoning methods, which make it possible to eliminate symbols in a goal-oriented manner. The practicality of this approach is shown by an evaluation on realistic ontologies.