Validating reasoning heuristics using next generation theorem provers

Steyn, Paul Stephanes

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.citation	Steyn, Paul Stephanes (2009) Validating reasoning heuristics using next generation theorem provers, University of South Africa, Pretoria, <http://hdl.handle.net/10500/2793>	en
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)