Abstract
When a first-order automated theorem prover is applied in a specific domain a number of pre- and postprocessing steps have to be performed such that the system fulfills the requirements set up in Chapter 5. These processing steps have been researched in depth by the author with the help of various case studies (some of which have been presented in the previous chapter). From this experience and based on numerous discussions with other researchers, a relatively generic scheme and skeleton architecture has been developed. Although not a universal recipe, this scheme can be methodically used as a basis for most applications in the area of software engineering.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Schumann, J.M. (2001). Specific Techniques for ATP Applications. In: Automated Theorem Proving in Software Engineering. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-22646-9_7
Download citation
DOI: https://doi.org/10.1007/978-3-662-22646-9_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-08759-2
Online ISBN: 978-3-662-22646-9
eBook Packages: Springer Book Archive