Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1007/978-3-642-28412-0_10 | WADT |
Keywords | Field | DocType |
logic translation,mere proof checking,model theoretic focus,model checker,efficient proof support,automated theorem provers,new logic,proof theoretic,towards logical framework,model finder,integration tool,heterogeneous tool set hets | T-norm fuzzy logics,Twelf,Computer science,Correctness,Proof theory,Algorithm,Theoretical computer science,Isomorphism,Mathematical proof,Logical framework,AND gate | Conference |
Citations | PageRank | References |
13 | 0.65 | 22 |
Authors | ||
6 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Mihai Codescu | 1 | 89 | 12.58 |
| Fulya Horozal | 2 | 55 | 4.32 |
| Michael Kohlhase | 3 | 1095 | 127.65 |
| Till Mossakowski | 4 | 1052 | 90.11 |
| Florian Rabe | 5 | 333 | 41.66 |
| Kristina Sojakova | 6 | 22 | 2.86 |