• search hit 29 of 73
Back to Result List

E-Hyper Tableaux with Distinct Object Identifiers

  • E-KRHyper is a versatile theorem prover and model generator for firstorder logic that natively supports equality. Inequality of constants, however, has to be given by explicitly adding facts. As the amount of these facts grows quadratically in the number of these distinct constants, the knowledge base is blown up. This makes it harder for a human reader to focus on the actual problem, and impairs the reasoning process. We extend E-Hyper- underlying E-KRhyper tableau calculus to avoid this blow-up by implementing a native handling for inequality of constants. This is done by introducing the unique name assumption for a subset of the constants (the so called distinct object identifiers). The obtained calculus is shown to be sound and complete and is implemented into the E-KRHyper system. Synthetic benchmarks, situated in the theory of arrays, are used to back up the benefits of the new calculus.

Download full text files

Export metadata

Additional Services

Share in Twitter Search Google Scholar
Metadaten
Author:Markus Bender
URN:urn:nbn:de:kola-7071
Series (Volume no.):Arbeitsberichte, FB Informatik (2013,1)
Document Type:Part of Periodical
Language:English
Date of completion:2013/02/06
Date of publication:2013/02/06
Publishing institution:Universität Koblenz-Landau, Universitätsbibliothek
Release Date:2013/02/06
Tag:Calculus; E-KRHyper; Theorem prover
Number of pages:42
Institutes:Fachbereich 4 / Fachbereich 4
Fachbereich 4 / Institut für Informatik
Dewey Decimal Classification:0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik
Licence (German):License LogoEs gilt das deutsche Urheberrecht: § 53 UrhG