| Art der Veröffentlichung: |
Artikel in Konferenzband |
| Autor: |
Klaus Lüttich, Till Mossakowski |
| Herausgeber: |
J. Fiadeiro |
| Titel: |
Reasoning {S}upport for {CASL} with {A}utomated {T}heorem {P}roving {S}ystems |
| Buch / Sammlungs-Titel: |
WADT 2006 |
| Band: |
4409 |
| Seite(n): |
74 – 91 |
| Erscheinungsjahr: |
2007 |
| Verleger: |
Springer-Verlag Heidelberg |
| Abstract / Kurzbeschreibung: |
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 |
| Schlagworte: |
CASL SPASS prover automatic FOL SoftFOL MathServe Vampire |
| Status: |
Reviewed |
| Letzte Aktualisierung: |
13. 02. 2007 |
