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.

Download full text

Cite this publication

  • Export Bibtex
  • Export RIS

Citable URL (?):

Search for this publication

Search Google Scholar Search Catalog of German National Library Search OCLC WorldCat Search Catalog of GBV Common Library Network Search Catalog of Jacobs University Library Search Bielefeld Academic Search Engine
Meta data
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
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

$Rev: 13581 $