UnisaIR Repository

Validating reasoning heuristics using next generation theorem provers

Show simple item record

dc.contributor.advisor Van der Poll, John Andrew
dc.contributor.author Steyn, Paul Stephanes
dc.date.accessioned 2009-11-05T07:32:04Z
dc.date.available 2009-11-05T07:32:04Z
dc.date.issued 2009-01
dc.date.submitted 2009-01-31
dc.identifier.uri http://hdl.handle.net/10500/2793
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
dc.description.degree M.Sc. (Computer Science)

Files in this item

This item appears in the following Collection(s)

Show simple item record

Search UnisaIR


My Account