Validating reasoning heuristics using next-generation theorem-provers

Steyn P.S.; Van Der Poll J.A.

UnisaIR Home
→
Unisa Research Output
→
Work in progress
→
Scopus
→
View Item

dc.contributor.author	Steyn P.S.	en
dc.contributor.author	Van Der Poll J.A.	en
dc.date.accessioned	2012-11-01T16:31:27Z
dc.date.available	2012-11-01T16:31:27Z
dc.date.issued	2007	en
dc.identifier.citation	Proceedings of the 5th International Workshop on Modelling, Simulation, Verification and Validation of Enterprise Information Systems - MSVVEIS 2007; In Conjunction with ICEIS 2007	en
dc.identifier.isbn	9.78973E+12	en
dc.identifier.uri	http://hdl.handle.net/10500/7243
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	Automated reasoners; Enterprise information systems; Formal specification languages; Formal specifications; Formal verifications; Reasoner; Automata theory; Computational methods; Heuristic methods; Linguistics; Set theory; Specification languages; Specifications; Technical presentations; Information systems	en
dc.title	Validating reasoning heuristics using next-generation theorem-provers	en
dc.type	Conference Paper	en