Reasoning {S}upport for {CASL} with {A}utomated {T}heorem {P}roving {S}ystems
Type of publication: | Inproceedings |
Citation: | LuettichEA06a |
Booktitle: | WADT 2006 |
Volume: | 4409 |
Year: | 2007 |
Pages: | 74-91 |
Publisher: | Springer-Verlag Heidelberg |
Abstract: | We connect the algebraic specification language CASL with a variety of automated first-order provers. The heart of this connection is an institution comorphism from CASL to SoftFOL (softly typed first-order logic); the latter is then translated to the provers' input syntaxes. We also describe a GUI integrating the translations and the provers into the Heterogeneous Tool Set. We report on experiences with provers, which led to fine-tuning of the translations. This framework can also be used for checking consistency of specifications. |
Userfields: | pdfurl={http://www.informatik.uni-bremen.de/~till/papers/casl2spass.pdf}, project={I4-SPIN}, psurl={http://www.informatik.uni-bremen.de/~till/papers/casl2spass.ps}, status={Reviewed}, |
Keywords: | CASL SPASS prover automatic FOL SoftFOL MathServe Vampire |
Authors | |
Editors | |
Attachments
|
|
Notes
|
|
|
|
Topics
|
|
|