Institutional Repository

Validating reasoning heuristics using next generation theorem provers

Show simple item record

dc.contributor.advisor Van der Poll, John Andrew Steyn, Paul Stephanes 2009-11-05T07:32:04Z 2009-11-05T07:32:04Z 2009-01 2009-01-31
dc.identifier.citation Steyn, Paul Stephanes (2009) Validating reasoning heuristics using next generation theorem provers, University of South Africa, Pretoria, <> en
dc.description.abstract 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. en
dc.format.extent 1 online resource (ix, 217 leaves)
dc.language.iso en en
dc.subject Automated reasoning en
dc.subject Automated theorem proving en
dc.subject Heuristics en
dc.subject Resolution en
dc.subject Zermelo-Fraenkel en
dc.subject First-order logic
dc.subject Formal specification
dc.subject Gandalf
dc.subject Otter
dc.subject Vampire
dc.subject Set theory
dc.subject Z
dc.subject.ddc 004.0151
dc.subject.lcsh Heuristic
dc.subject.lcsh Logic, symbolic and mathematical
dc.subject.lcsh Set theory
dc.title Validating reasoning heuristics using next generation theorem provers en
dc.type Thesis en
dc.description.department Computing M.Sc. (Computer Science)

Files in this item

This item appears in the following Collection(s)

Show simple item record

Search UnisaIR


My Account