## Contact

Swiss National Science Foundation (SNSF)

Wildhainweg 3P.O. Box

CH-3001 Bern

Phone +41 31 308 22 22

English title | Algebraic and logical aspects of knowledge processing |
---|---|

Applicant | Jäger Gerhard |

Number | 119759 |

Funding scheme | Project funding (Div. I-III) |

Research institution | Institut für Informatik Universität Bern |

Institution of higher education | University of Berne - BE |

Main discipline | Mathematics |

Start/End | 01.04.2008 - 30.09.2011 |

Approved amount | 730'480.00 |

Discipline |
---|

Mathematics |

Information Technology |

Explicit mathematics; theories of types and names; operational set theories; second order arithmetic; hither type recursion; operational set theory; higher type recursion

Lead |
---|

Lay summary |

In this project, we employ and set up conceptual frameworks, in particular, theories relating classical mathematics with constructive mathematics and feasible mathematics. Thereby we always emphasize the computational properties and complexities of our formalisms. We use proof theory as our main tool for analyzing the constructive and computational content of various formalisms and aim at further exploiting the proofs as computations paradigm. Besides the traditional subsystems of first- and second-order arithmetic and (admissible) set theory, we will focus on theories of explicit mathematics, operational set theories, and theories of partial truth. |

Direct link to Lay Summary | Last update: 21.02.2013 |

Name | Institute |
---|

Name | Institute |
---|

Publication |
---|

A Buchholz rule for modal fixed point logics |

Admissible closures of polynomial time computable arithmetic |

On the relationship between choice schemes and iterated class comprehension in set theory (PhD dissertation) |

Realizability in weak systems of explicit mathematics |

The provably terminating operations of the subsystem PETJ of explicit mathematics |

The Suslin operator in applicative theories: its proof-theoretic analysis via ordinal theories |

$\Sigma^1_1$ choice in a theory of sets and classes |

Unfolding finitist arithmetic |

Weak theories of operations and types |

Elementary explicit types and polynomial time operations |

Full operational set theory with unbounded existential quantification and power set |

Operations, sets and classes |

Weak systems of explicit mathematics (PhD dissertation) |

An algorithmic interpretation of a deep inference system |

Primitive recursive selection functions for existential assertions over abstract algebras |

Soft linear set theory |

Group / person | Country |
---|

Types of collaboration |
---|

Universität München | Germany (Europe) |

- in-depth/constructive exchanges on approaches, methods or results - Exchange of personnel |

Number | Title | Start | Funding scheme |
---|

107443 | Algebraische und logische Aspekte der Wissensverarbeitung | 01.04.2005 | Project funding (Div. I-III) |

137678 | Algebraic and Logical Aspects of Knowledge Processing | 01.10.2011 | Project funding (Div. I-III) |

Swiss National Science Foundation (SNSF)

Wildhainweg 3P.O. Box

CH-3001 Bern

Phone +41 31 308 22 22

Enter and manage your applications

Enter your e-mail address to receive the SNSF Newsletter regularly

© SNSF 2018