@inproceedings{LuettichEA06a,
  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.
},
  added-at = {2016-08-05T15:59:03.000+0200},
  author = {L{\"u}ttich, Klaus and Mossakowski, Till},
  biburl = {https://www.bibsonomy.org/bibtex/2744c7e37e27241f3f180823b776bcf11/tillmo},
  booktitle = {WADT 2006},
  editor = {Fiadeiro, J.},
  interhash = {f1cd4e92ed77680c4a09176ee8e946f2},
  intrahash = {744c7e37e27241f3f180823b776bcf11},
  keywords = {CASL FOL MathServe SPASS SoftFOL Vampire automatic prover},
  pages = {74-91},
  pdfurl = {http://www.informatik.uni-bremen.de/~till/papers/casl2spass.pdf},
  psurl = {http://www.informatik.uni-bremen.de/~till/papers/casl2spass.ps},
  publisher = {Springer-Verlag Heidelberg},
  status = {Reviewed},
  timestamp = {2016-08-05T15:59:03.000+0200},
  title = {Reasoning {S}upport for {CASL} with {A}utomated {T}heorem {P}roving {S}ystems},
  volume = 4409,
  year = 2007
}