| Publication type: |
Article in Proceedings |
| Author: |
Klaus Lüttich, Till Mossakowski |
| Editor: |
J. Fiadeiro |
| Title: |
Reasoning Support for CASL with Automated Theorem Proving Systems |
| Book / Collection title: |
WADT 2006 |
| Volume: |
4409 |
| Page(s): |
74 – 91 |
| Year published: |
2007 |
| 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.
|
| PDF Version: |
http://www.informatik.uni-bremen.de/~till/papers/casl2spass.pdf |
| PostScript Version: |
http://www.informatik.uni-bremen.de/~till/papers/casl2spass.ps |
| Keywords: |
CASL SPASS prover automatic FOL SoftFOL MathServe Vampire |
| Status: |
Reviewed |
| Last updated: |
13. 02. 2007 |
