## Representing logics and logictranslations

- Logic is the study of formal languages for propositions and truth. Logics are used both as a foundation of mathematics and as specification languages in mathematics and computer science. Since logic is intricately intertwined with the nature of mathematics, the question how to represent logics in our minds is a constant challenge to our understanding. And only when it is understood can we begin to answer the corresponding question about logic translations. At the same time logics are used to a large extent in computer science to reason about both mathematics and software systems. This brings up the question how logics and their translations can be represented in a computer system. Throughout the 20th century several answers have already been provided. Most of them can be grouped into two kinds, which can be denoted by set/model theory and type/proof theory. We base our investigation on the desire to reconcile these two views. Our focus is on extending the existing notions of logic and logic translation in a way that retains their nature and the accumulated knowledge about them while leading them into a new direction. Our goal is to enrich both research fields by applying them more cogently to and making them more accessible and understandable to one another. While this answers the question how to represent logics and logic translations in our minds, it is not adequate for the specific constraints and use cases of software systems. Therefore, in a second investigation, we explore how to make our representations more concrete and robust enough to permit a mechanized treatment on a large scale. Taking these two results together, we obtain a triangle of different mathematical communities, research objectives, and philosophies consisting of set/model theory, proof/type theory, and mathematical knowledge management. Our main contribution is to integrate its corners into a coherent framework centered around logic that capitalizes on their comparative advantages.

Publishing Institution: | IRC-Library, Information Resource Center der Jacobs University Bremen |
---|---|

Granting Institution: | Jacobs Univ. |

Author: | Florian Rabe |

Referee: | Michael Kohlhase, Herbert Jaeger, Till Mossakowski, Frank Pfenning |

Advisor: | Michael Kohlhase |

Persistent Identifier (URN): | urn:nbn:de:101:1-201305237073 |

Document Type: | PhD Thesis |

Language: | English |

Date of Successful Oral Defense: | 2008/06/19 |

Date of First Publication: | 2008/12/05 |

PhD Degree: | Computer Science |

School: | SES School of Engineering and Science |

Other Countries Involved: | United States of America |

Library of Congress Classification: | Q Science / Q Science (General) / Q300-390 Cybernetics / Q325-342 Self-organizing systems. Conscious automata / Q334-342 Artificial intelligence |

Call No: | Thesis 2008/24 |