Refine
Year of publication
Document Type
- Diploma Thesis (196) (remove)
Keywords
- Augmented Reality (4)
- Bildverarbeitung (4)
- RIP-MTI (4)
- Routing (4)
- Analyse durch Synthese (3)
- Interaktion (3)
- Java (3)
- Kamera (3)
- Logistik (3)
- Markerloses Tracking (3)
Institute
- Institut für Computervisualistik (81)
- Fachbereich 4 (47)
- Institut für Wirtschafts- und Verwaltungsinformatik (27)
- Institut für Informatik (24)
- Institut für Softwaretechnik (14)
- Institute for Web Science and Technologies (3)
- Institut für Kommunikationspsychologie und Medienpädagogik (2)
- Fachbereich 5 (1)
- Institut für Management (1)
In automated theorem proving, there are some problems that need information on the inequality of certain constants. In most cases this information is provided by adding facts which explicitly state that two constants are unequal. Depending on the number of constants, a huge amount of this facts can clutter the knowledge base and distract the author and readers of the problem from its actual proposition. For most cases it is save to assume that a larger knowledge base reduces the performance of a theorem prover, which is another drawback of explicit inequality facts. Using the unique name assumption in those reasoning tasks renders the introduction of inequality facts obsolete as the unique name assumptions states that two constants are identical iff their interpretation is identical. Implicit handling of non-identical constants makes the problems easier to comprehend and reduces the execution time of reasoning. In this thesis we will show how to integrate the unique name assumption into the E-hyper tableau calculus and that the modified calculus is sound and complete. The calculus will be implemented into the E-KRHyper theorem prover and we will show, by empiric evaluation, that the changed implementation, which is able to use the unique name assumption, is superior to the traditional version of E-KRHyper.