Towards Logical Frameworks in the Heterogeneous Tool Set Hets

Mihai Codescu, Fulya Horozal, Michael Kohlhase, Till Mossakowski, Florian Rabe, Kristina Sojakova

In: Hans-Jörg Kreowski , Till Mossakowski (Hrsg.). Recent Trends in Algebraic Development Techniques. International Workshop on Algebraic Development Techniques (WADT-10) 20th July 1-4 Schloss Etelsen Germany Lecture Notes in Computer Science (LNCS) 7137 Springer 2012.


LF is a meta-logical framework that has become a standard tool for representing logics and studying their properties. Its focus is proof theoretic, employing the Curry-Howard isomorphism: propositions are represented as types, and proofs as terms. Hets is an integration tool for logics, logic translations and provers, with a model theoretic focus, based on the meta-framework of institutions, a formalisation of the notion of logical system. In this work, we combine these two worlds. The benefit for LF is that logics represented in LF can be (via Hets) easily connected to various interactive and automated theorem provers, model finders, model checkers, and conservativity checkers - thus providing much more efficient proof support than mere proof checking as is done by systems like Twelf. The benefit for Hets is that (via LF) logics become represented formally, and hence trustworthiness of the implementation of logics is increased, and correctness of logic translations can be mechanically verified. Moreover, since logics and logic translations are now represented declaratively, the effort of adding new logics or translations to Hets is greatly reduced. This work is part of a larger effort of building an atlas of logics and translations used in computer science and mathematics.


Weitere Links

wadt_submission_20_final.pdf (pdf, 474 KB )

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence