Heuristics for resolution-based set-theoretic proofs

dc.contributor.author	Van der Poll, J.A.
dc.contributor.author	Labuschagne, W.A.
dc.date.accessioned	2012-02-09T06:55:34Z
dc.date.available	2012-02-09T06:55:34Z
dc.date.issued	1999-07
dc.identifier.citation	Van der Poll, J.A. & Labuschange, W.A. 1999,'Heuristics for resolution-based set-theoretic proofs', South African computer journal, Vol. 51, no. 23, pp.3-17.	en
dc.identifier.uri	http://hdl.handle.net/10500/5371
dc.description.abstract	A formal specification language like Z permits the specifier to construct proofs which collaborate the aptness of the specification. This process may be facilitated by establishing a partnership between the specifier and a suitable automated reasoner. However, Z specifications are essentially set-theoretic proofs pose demanding challenges to automated reasoners. Taking the OTTER theorem-prover to be representative of resolution-based automated reasoners, we propose a number of heuristics intended to cut down the search space for proofs involving typical set-theoretic structures.	en
dc.language.iso	en	en
dc.subject	Heuristics	en
dc.subject	Resolution-based set-theoretic proofs	en
dc.subject	Problem frames	en
dc.subject	Resolution	en
dc.subject	Set theories	en
dc.subject	Theorem-proving	en
dc.title	Heuristics for resolution-based set-theoretic proofs	en
dc.type	Article	en