Return to search

Validating reasoning heuristics using next generation theorem provers

The specification of enterprise information systems using formal specification languages
enables the formal verification of these systems. Reasoning about the properties of a formal
specification is a tedious task that can be facilitated much through the use of an automated
reasoner. However, set theory is a corner stone of many formal specification languages and
poses demanding challenges to automated reasoners. To this end a number of heuristics has
been developed to aid the Otter theorem prover in finding short proofs for set-theoretic
problems. This dissertation investigates the applicability of these heuristics to next generation
theorem provers. / Computing / M.Sc. (Computer Science)

Identiferoai:union.ndltd.org:netd.ac.za/oai:union.ndltd.org:unisa/oai:umkn-dsp01.int.unisa.ac.za:10500/2793
Date31 January 2009
CreatorsSteyn, Paul Stephanes
ContributorsVan der Poll, John Andrew
Source SetsSouth African National ETD Portal
LanguageEnglish
Detected LanguageEnglish
TypeThesis
Format1 online resource (ix, 217 leaves)

Page generated in 0.0022 seconds