hets.bib revision a17349d0247036407c22e632ece0e8f2b736253c
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski author = {L. Schr\"oder and T. Mossakowski and C. Maeder},
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski title = {{\HasCASL} -- {I}ntegrated functional specification and programming. {L}anguage Summary},
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich note = {Available at \url{http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/HasCASL}},
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski year = {2003},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski@Article{Schroder05b,
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski author = {Lutz Schr{\"o}der},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski title = {The {HasCASL} Prologue - Categorical Syntax and Semantics of the Partial {$\lambda$}-calculus},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski year = {2006},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski journal = {Theoret. Comput. Sci.},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski volume = {353},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski pages = {1-25},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski keywords = {partial lambda-calculus partial cartesian closed category Henkin model HasCASL CASL},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski pdfurl = {http://www.informatik.uni-bremen.de/~lschrode/hascasl/prologue.pdf},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski psurl = {http://www.informatik.uni-bremen.de/~lschrode/hascasl/prologue.ps},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski abstract = {We develop the semantic foundations of the specification language HasCASL, which combines algebraic specification and functional programming on the basis of Moggi's partial {$\lambda$}-calculus. Generalizing Lambek's classical equivalence between the simply typed {$\lambda$}-calculus and cartesian closed categories, we establish an equivalence between partial cartesian closed categories (pccc's) and partial {$\lambda$}-theories. Building on these results, we define (set-theoretic) notions of intensional Henkin model and syntactic {$\lambda$}-algebra for Moggi's partial {$\lambda$}-calculus. These models are shown to be equivalent to the originally described categorical models in pccc's via the global element construction. The semantics of HasCASL is defined in terms of syntactic {$\lambda$}-algebras. Correlations between logics and classes of categories facilitate reasoning both on the logical and on the categorical side; as an application, we pinpoint unique choice as the distinctive feature of topos logic (in comparison to intuitionistic higher-order logic of partial functions, which by our results is the logic of pccc's with
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiequality). Finally, we give some applications of the model-theoretic equivalence result to the semantics of HasCASL and its relation to first-order CASL.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski status = {Reviewed}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski@unpublished{Schroder-habil,
30256573a343132354b122097b0ee1215dda1364Till Mossakowski author = {Lutz Schr\"oder},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski title = {Higher order and reactive algebraic specification and development},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski school = {University of Bremen},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski year = {2005},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski note = {Summary of papers constituting a cumulative habilitation thesis; available under \url{http://www.informatik.uni-bremen.de/~lschrode/papers/Summary.pdf}},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski@Misc{ModalCASL,
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski author = {T. Mossakowski},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski title = {Modal{CASL} - Specification with Multi-Modal Logics. Language Summary},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski year = {2004},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski keywords = {modal logic CASL},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski pdfurl = {http://www.tzi.de/~till/papers/Modal-Summary.pdf},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski psurl = {http://www.tzi.de/~till/papers/Modal-Summary.ps},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski abstract = {ModalCASL extends CASL by modal operators. Syntax for ordinary
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski modalities, multi-modal logics as well as term-modal
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski logic (also covering dynamic logic) is provided.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski Specific modal logics can be obtained via restrictions to
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski sublanguages.
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiThis document provides a detailed definition of the ModalCASL syntax
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiand an informal description of the semantics, building on the existing
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiCASL Summary.},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski status = {Other}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski@article{RiazanovV02,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski author = {Alexandre Riazanov and
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski Andrei Voronkov},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski title = {The design and implementation of {VAMPIRE}},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski journal = {AI Communications},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski volume = {15},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski number = {2-3},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski year = {2002},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski pages = {91-110},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski ee = {http://iospress.metapress.com/openurl.asp?genre=article{\&}issn=0921-7126{\&}volume=15{\&}issue=2{\&}spage=91},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski bibsource = {DBLP, http://dblp.uni-trier.de}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski@InProceedings{ZimmerAutexier06,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiauthor = {J{\"u}rgen Zimmer and Serge Autexier},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskititle = {The {M}ath{S}erve {S}ystem for {S}emantic {W}eb {R}easoning {S}ervices},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskibooktitle = {3rd IJCAR},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskieditor = {U. Furbach and N. Shankar},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiseries = {LNCS 4130},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskipublisher = {Springer},
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph Lange@INPROCEEDINGS{LuettichEA06a,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski author = {Klaus L{\"u}ttich and Till Mossakowski},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski title = {Reasoning {S}upport for {CASL} with {A}utomated {T}heorem {P}roving {S}ystems},
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph Lange pages = {74--91},
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph Lange crossref={WADT06},
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph Lange url = {http://www.informatik.uni-bremen.de/~till/papers/casl2spass.pdf}}
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph Lange@PROCEEDINGS{WADT06,
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph Lange booktitle = {WADT 2006},
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph Lange title = {WADT 2006},
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph Lange year = {2007},
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph Lange editor = {J. Fiadeiro},
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph Lange series = {LNCS},
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph Lange number = {4409},
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph Lange publisher = {Springer}}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski@article{Mossakowski02,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski author = {Till Mossakowski},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski title = {Relating {\CASL} with Other Specification Languages:
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski the Institution Level},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski journal = {Theoretical Computer Science},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski volume = {286},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski pages = {367--475},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski@ARTICLE{GoguenBurstall92,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiAUTHOR = "J. A. Goguen and R. M. Burstall",
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiTITLE = "Institutions: Abstract Model Theory for Specification and
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiJOURNAL = "Journal of the Association for Computing Machinery",
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiPAGES = {95--146},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiNOTE = {Predecessor in: LNCS 164, 221--256, 1984.},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski@article{GoguenRosu02,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski author = {J. Goguen and G. Ro\c{s}u},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski title = {Institution morphisms},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski journal = {Formal aspects of computing},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski volume = {13},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski year = {2002},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski pages = {274-307},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski@unpublished{Habil,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski Author = {T. Mossakowski},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski Title = {Heterogeneous specification and the heterogeneous tool set},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski Note = {Habilitation thesis, University of Bremen},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski@InProceedings{MossakowskiEA06,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski author = {Till Mossakowski and Christian Maeder and Klaus L{\"u}ttich},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski title = {The {H}eterogeneous {T}ool {S}et},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski year = {2007},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski editor = {Orna Grumberg and Michael Huth},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski booktitle = {TACAS 2007},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski publisher = {Springer-Verlag Heidelberg},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski series = {Lecture Notes in Computer Science},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski volume = {4424},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski pages = {519-522},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski keywords = {proof heterogeneity logic institution prover theorem integration development graph},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski pdfurl = {http://www.tzi.de/~till/papers/hets-tacas-toolpaper.pdf},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski psurl = {http://www.tzi.de/~till/papers/hets-tacas-toolpaper.ps},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski abstract = {Heterogeneous specification becomes more and more important because
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskicomplex systems are often specified using multiple viewpoints,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiinvolving multiple formalisms. Moreover, a formal software development
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiprocess may lead to a change of formalism during the development.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiHowever, current research in integrated formal methods only deals
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiwith ad-hoc integrations of different formalisms.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiThe heterogeneous tool set (Hets) is a parsing, static analysis and
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiproof management tool combining various such tools for individual
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskispecification languages, thus providing a tool for heterogeneous
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskimulti-logic specification. Hets is based on a graph of logics and
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskilanguages (formalized as so-called institutions), their tools, and
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskitheir translations. This provides a clean semantics of heterogeneous
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskispecification, as well as a corresponding proof calculus. For proof
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskimanagement, the calculus of development graphs (known from other
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskilarge-scale proof management systems) has been adapted to
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiheterogeneous specification. Development graphs provide an overview of
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskithe (heterogeneous) specification module hierarchy and the current
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiproof state, and thus may be used for monitoring the overall
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskicorrectness of a heterogeneous development.},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski status = {Reviewed}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski@Article{MossakowskiEtAl05,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski author = {T. Mossakowski and S. Autexier and D. Hutter},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski title = {Development Graphs -- Proof Management for Structured Specifications},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski year = {2006},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski journal = {Journal of Logic and Algebraic Programming},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski volume = {67},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski pages = {114-145},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski number = {1-2},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski keywords = {development graph proof logic institution completeness},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski url = {http://www.sciencedirect.com/science?_ob=GatewayURL&_origin=CONTENTS&_method=citationSearch&_piikey=S1567832605000810&_version=1&md5=7c18897e9ffad42e0649c6b41203f41e},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski psurl = {http://www.tzi.de/~till/papers/dgh_journal.ps},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski abstract = {Development graphs are a tool for dealing with structured
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski specifications in a formal program development in order to ease the
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski management of change and reusing proofs. In this work, we extend
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski development graphs with hiding (e.g. hidden operations). Hiding is
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski a particularly difficult to realize operation, since it does not
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski admit such a good decomposition of the involved specifications as
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski other structuring operations do. We develop both a semantics and
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski proof rules for development graphs with hiding. The rules are proven
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski to be sound, and also complete relative to an oracle for
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski conservative extensions. We also show that an absolutely complete set
4b41220e2b76251e0bb0760c016e79994bb2c2bbChristian Maeder of rules cannot exist.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski The whole framework is developed in a way independent of the
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski underlying logical system (and thus also does not prescribe the
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski nature of the parts of a specification that may be hidden). We also
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski show how various other logic independent specification formalisms
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski can be mapped into development graphs; thus, development graphs can
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski serve as a kernel formalism for management of proofs and of change.},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski issn = {1567-8326},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski status = {Reviewed}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski@Book{blackburn_p-etal:2001a,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski author = "Patrick BLackburn and Maarten de Rijke and Yde
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski title = "Modal Logic",
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski publisher = "Cambridge University Press",
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski year = "2001",
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski address = "Cambridge, England",
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski ISBN = "0 521 52714 7 (pbk)",
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski topic = "modal-logic;",
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski@unpublished{TorriniEtAl07,
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski author = {Paolo Torrini and Christoph L\"{u}th and
4b41220e2b76251e0bb0760c016e79994bb2c2bbChristian Maeder Christian Maeder and Till Mossakowski},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski title = {Translating {Haskell} to {Isabelle}},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski note = {Isabelle workshop at CADE-21},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski year = {2007},
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski@MastersThesis{Groening05,
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski author = {Sonja Gr\"{o}ning},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski title = {Beweisunterst\"{u}tzung f\"{u}r {HasCASL} in {Isabelle
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski school = {University of Bremen},
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski note = {Diplomarbeit},
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski year = {2005},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski@InCollection{MossakowskiEtAl07b,
30256573a343132354b122097b0ee1215dda1364Till Mossakowski author = {Till Mossakowski and Christian Maeder and Klaus L{\"u}ttich},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski title = {The {H}eterogeneous {T}ool {S}et},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski year = {2007},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski editor = {Bernhard Beckert},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski booktitle = {VERIFY 2007},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski series = {CEUR Workshop Proceedings},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski volume = {259},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski status = {Reviewed}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski@TechReport{Herbstritt03,
30256573a343132354b122097b0ee1215dda1364Till Mossakowski author = "Marc Herbstritt",
30256573a343132354b122097b0ee1215dda1364Till Mossakowski title = "{zChaff}: Modifications and Extensions",
30256573a343132354b122097b0ee1215dda1364Till Mossakowski institution = "Institut f{\"u}r Informatik, Universit{\"a}t
30256573a343132354b122097b0ee1215dda1364Till Mossakowski type = "report00188",
30256573a343132354b122097b0ee1215dda1364Till Mossakowski month = jul # " 17",
30256573a343132354b122097b0ee1215dda1364Till Mossakowski year = "2003",
30256573a343132354b122097b0ee1215dda1364Till Mossakowski URL = "ftp://ftp.informatik.uni-freiburg.de/documents/reports/report188/report00188.ps.gz",
30256573a343132354b122097b0ee1215dda1364Till Mossakowski abstract = "The application of SAT solver in industrial
30256573a343132354b122097b0ee1215dda1364Till Mossakowski verification tools is mandatory for the successful
30256573a343132354b122097b0ee1215dda1364Till Mossakowski analysis of problems derived from hardware design,
30256573a343132354b122097b0ee1215dda1364Till Mossakowski e.g.~Combinational Equivalence Checking (CEC) and
30256573a343132354b122097b0ee1215dda1364Till Mossakowski Bounded Model Checking (BMC). Moskewicz et al. have
30256573a343132354b122097b0ee1215dda1364Till Mossakowski developed a new powerful SAT solver in 2001 that
30256573a343132354b122097b0ee1215dda1364Till Mossakowski outperforms most of the existing publicly available SAT
30256573a343132354b122097b0ee1215dda1364Till Mossakowski solvers when applied to hard real-world problems,
30256573a343132354b122097b0ee1215dda1364Till Mossakowski e.g.~from VLSI CAD. There are two versions available of
30256573a343132354b122097b0ee1215dda1364Till Mossakowski Chaff: {\tt mChaff} and {\tt zChaff}. Both are
30256573a343132354b122097b0ee1215dda1364Till Mossakowski instances of Chaff, but from the viewpoint of
30256573a343132354b122097b0ee1215dda1364Till Mossakowski implementation they are totally different since they
30256573a343132354b122097b0ee1215dda1364Till Mossakowski were developped independently by M.~Moskewicz ({\tt
30256573a343132354b122097b0ee1215dda1364Till Mossakowski mChaff}) and L. Zhang ({\tt zChaff}). In this paper we
30256573a343132354b122097b0ee1215dda1364Till Mossakowski concentrate on {\tt zChaff}. We analyze the core issues
30256573a343132354b122097b0ee1215dda1364Till Mossakowski and propose modifications and extensions.",
30256573a343132354b122097b0ee1215dda1364Till Mossakowski note = "Thu, 17 Jul 2003 17:11:37 GET",
30256573a343132354b122097b0ee1215dda1364Till Mossakowski@Misc{Mossakowski04,
30256573a343132354b122097b0ee1215dda1364Till Mossakowski author = {T. Mossakowski},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski title = {{HetCASL} - Heterogeneous Specification. Language Summary},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski year = {2004},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski pdfurl = {http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/HetCASL/HetCASL-Summary.pdf},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski psurl = {http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/HetCASL/HetCASL-Summary.ps},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski abstract = {Heterogeneous CASL (HetCASL) allows
30256573a343132354b122097b0ee1215dda1364Till Mossakowskimixing specifications written in different logics (using
30256573a343132354b122097b0ee1215dda1364Till Mossakowskitranslations between the logics). It extends
30256573a343132354b122097b0ee1215dda1364Till MossakowskiCASL only at the level of structuring constructs, by adding constructs
30256573a343132354b122097b0ee1215dda1364Till Mossakowskifor choosing the logic and translating specifications among
30256573a343132354b122097b0ee1215dda1364Till Mossakowskilogics. HetCASL is needed when combining specifications written in
30256573a343132354b122097b0ee1215dda1364Till MossakowskiCASL with specifications written in its sublanguages and
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiextensions. HetCASL also allows the integration of logics
30256573a343132354b122097b0ee1215dda1364Till Mossakowskithat are completely different from the CASL logic.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThis document provides a detailed definition of the HetCASL syntax
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiand an informal description of the semantics, building on the existing
30256573a343132354b122097b0ee1215dda1364Till MossakowskiCASL Summary.},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski status = {Other}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski title = "{OMD}oc - An Open Markup Format for Mathematical
30256573a343132354b122097b0ee1215dda1364Till Mossakowski Documents [version 1.2]",
30256573a343132354b122097b0ee1215dda1364Till Mossakowski author = "Michael Kohlhase",
30256573a343132354b122097b0ee1215dda1364Till Mossakowski publisher = "Springer",
30256573a343132354b122097b0ee1215dda1364Till Mossakowski year = "2006",
30256573a343132354b122097b0ee1215dda1364Till Mossakowski volume = "4180",
30256573a343132354b122097b0ee1215dda1364Till Mossakowski bibdate = "2006-12-13",
30256573a343132354b122097b0ee1215dda1364Till Mossakowski ISBN = "3-540-37897-9",
30256573a343132354b122097b0ee1215dda1364Till Mossakowski series = "Lecture Notes in Computer Science",
30256573a343132354b122097b0ee1215dda1364Till Mossakowski URL = "http://dx.doi.org/10.1007/11826095",
30256573a343132354b122097b0ee1215dda1364Till Mossakowski@Unpublished{SparQ06,
30256573a343132354b122097b0ee1215dda1364Till Mossakowski author = {Jan Oliver Wallgr\"un and Lutz Frommberger and Frank Dylla and Diedrich Wolter},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski title = {{SparQ} User Manual V0.6.2},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski note = {University of Bremen},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski year = {2006},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski@incollection{TypeClasses,
30256573a343132354b122097b0ee1215dda1364Till Mossakowski author = {Simon {Peyton Jones} and Mark Jones and Erik Meijer},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski title = {Type classes: exploring the design space},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski booktitle = {Haskell Workshop},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski year = {1997},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski@techreport{Parsec,
30256573a343132354b122097b0ee1215dda1364Till Mossakowski author = {Daan Leijen and Erik Meijer},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski title = {Parsec: Direct Style Monadic Parser Combinators for the Real World},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski note = {UU-CS-2001-35},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski school = {Departement of Computer Science, Universiteit Utrecht},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski@unpublished{GHC,
30256573a343132354b122097b0ee1215dda1364Till Mossakowski title = {The {G}lasgow {H}askell compiler},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski note = {available at \texttt{http://www.haskell.org/ghc}},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski@Article{Roggenbach06,
30256573a343132354b122097b0ee1215dda1364Till Mossakowski author = {M. Roggenbach},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski title = {{CSP-CASL} - A new integration of process algebra and algebraic specification},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski journal = {Theoretical Computer Science},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski year = {2006},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski volume = {354},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski number = {1},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski pages = {42--71},
4b41220e2b76251e0bb0760c016e79994bb2c2bbChristian Maeder@article{VSE00,
4b41220e2b76251e0bb0760c016e79994bb2c2bbChristian Maeder author = {Autexier, S. and Hutter, D. and Langenstein, B. and Mantel, H. and
4b41220e2b76251e0bb0760c016e79994bb2c2bbChristian MaederRock, G. and Schairer, A. and Stephan, W. and Vogt, R. and Wolpers, A.},
4b41220e2b76251e0bb0760c016e79994bb2c2bbChristian Maeder title = {{VSE}: Formal methods meet industrial needs},
4b41220e2b76251e0bb0760c016e79994bb2c2bbChristian Maeder journal = {International Journal on Software Tools for Technology Transfer, Sp
4b41220e2b76251e0bb0760c016e79994bb2c2bbChristian Maederecial issue on Mechanized Theorem Proving for Technology},
4b41220e2b76251e0bb0760c016e79994bb2c2bbChristian Maeder volume = {3},
4b41220e2b76251e0bb0760c016e79994bb2c2bbChristian Maeder number = {1},
4b41220e2b76251e0bb0760c016e79994bb2c2bbChristian Maeder publisher = {Springer},
4b41220e2b76251e0bb0760c016e79994bb2c2bbChristian Maeder month = {september},
4b41220e2b76251e0bb0760c016e79994bb2c2bbChristian Maeder year = {2000},
dd29aea0190ac8707f2a0896a4a4b8bb2aac13ffEugen Kuksa@Misc{HetsUserGuide,
dd29aea0190ac8707f2a0896a4a4b8bb2aac13ffEugen Kuksa author = {Till Mossakowski, Christian Maeder, Mihai Codescu},
dd29aea0190ac8707f2a0896a4a4b8bb2aac13ffEugen Kuksa title = {Hets User Guide},
dd29aea0190ac8707f2a0896a4a4b8bb2aac13ffEugen Kuksa year = {2011},
dd29aea0190ac8707f2a0896a4a4b8bb2aac13ffEugen Kuksa pdfurl = {http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/UserGuide.pdf},
dd29aea0190ac8707f2a0896a4a4b8bb2aac13ffEugen Kuksa note = {\url{http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/UserGuide.pdf}},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski@inproceedings{DBLP:conf/cade/BenzmullerRS08,
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski author = {Christoph Benzm{\"u}ller and
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski Florian Rabe and
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski Geoff Sutcliffe},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski title = {{THF0} - The Core of the {TPTP} Language for Higher-Order Logic},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski booktitle = {Automated Reasoning, 4th International Joint Conference,
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski pages = {491-506},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski ee = {http://dx.doi.org/10.1007/978-3-540-71070-7_41},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski editor = {Alessandro Armando and
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski Peter Baumgartner and
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski Gilles Dowek},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski bibsource = {DBLP, http://dblp.uni-trier.de},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski publisher = {Springer},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski series = {Lecture Notes in Computer Science},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski volume = {5195},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski year = {2008},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski isbn = {978-3-540-71069-1},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski@inproceedings{DBLP:conf/lpar/Sutcliffe10,
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski author = {Geoff Sutcliffe},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski title = {The {TPTP} World - Infrastructure for Automated Reasoning},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski booktitle = {LPAR (Dakar)},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski year = {2010},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski pages = {1-12},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski ee = {http://dx.doi.org/10.1007/978-3-642-17511-4_1},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski bibsource = {DBLP, http://dblp.uni-trier.de},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski editor = {Edmund M. Clarke and
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski Andrei Voronkov},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski - 16th International Conference, LPAR-16, Dakar, Senegal,
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski April 25-May 1, 2010, Revised Selected Papers},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski publisher = {Springer},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski series = {Lecture Notes in Computer Science},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski volume = {6355},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski year = {2010},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski isbn = {978-3-642-17510-7},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski@Article{Schulz:AICOM-2002,
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski author = {S. Schulz},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski title = {{E -- A Brainiac Theorem Prover}},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski journal = {Journal of AI Communications},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski year = {2002},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski volume = {15},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski number = {2/3},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski pages = {111--126},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski annote = {StS},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski@inproceedings{DBLP:conf/cade/PelzerW07,
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski author = {Bj{\"o}rn Pelzer and
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski Christoph Wernhard},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski title = {System Description: E-KRHyper},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski booktitle = {CADE},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski year = {2007},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski pages = {508-513},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski ee = {http://dx.doi.org/10.1007/978-3-540-73595-3_37},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski bibsource = {DBLP, http://dblp.uni-trier.de},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski editor = {Frank Pfenning},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski booktitle = {Automated Deduction - CADE-21, 21st International Conference
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski on Automated Deduction, Bremen, Germany, July 17-20, 2007,
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski Proceedings},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski publisher = {Springer},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski series = {Lecture Notes in Computer Science},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski volume = {4603},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski year = {2007},
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski isbn = {978-3-540-73594-6},