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)
| Identifer | oai:union.ndltd.org:netd.ac.za/oai:union.ndltd.org:unisa/oai:uir.unisa.ac.za:10500/2793 |
| Date | 31 January 2009 |
| Creators | Steyn, Paul Stephanes |
| Contributors | Van der Poll, John Andrew |
| Source Sets | South African National ETD Portal |
| Language | English |
| Detected Language | English |
| Type | Thesis |
| Format | 1 online resource (ix, 217 leaves) |
Page generated in 0.0026 seconds