[BibTeX] [RIS]
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 L├╝ttich, Klaus
Mossakowski, Till
Editors Fiadeiro, J.
Attachments
  • http://www.informatik.uni-brem...
  • http://www.informatik.uni-brem...
Notes
    Topics