Validating reasoning heuristics using next-generation theorem-provers

dc.contributor.author	Steyn, Paul S.
dc.contributor.author	Van der Poll, John A.
dc.date.accessioned	2012-01-27T09:16:36Z
dc.date.available	2012-01-27T09:16:36Z
dc.date.issued	2007-06
dc.identifier.uri	http://hdl.handle.net/10500/5284
dc.description	Proceedings of the Fifth Workshop on modelling simulation Verification and Validation of Enterprise Information Systems (MSVVEIS'07), pp. 43-52, Funchal, Madeira, Portugal, June 2007.
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 paper investigates the applicability of these heuristics to a next generation theorem prover Vampire.	en
dc.language.iso	en	en
dc.subject	Theorem-provers	en
dc.subject	Reasoning heuristics	en
dc.subject	Vampire theorem prover	en
dc.subject	Set-theoretic	en
dc.title	Validating reasoning heuristics using next-generation theorem-provers	en
dc.type	Article	en