Project

Back to overview

Algebraische und logische Aspekte der Wissensverarbeitung

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
Show all

All Disciplines (2)

Discipline
Mathematics
Information Technology

Keywords (7)

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

Lay Summary (English)

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

Responsible applicant and co-applicants

Employees

Publications

Publication
A Buchholz rule for modal fixed point logics
Jäger Gerhard, Studer Thomas (2011), A Buchholz rule for modal fixed point logics, in Logica Universalis, 5(1), 1-19.
Admissible closures of polynomial time computable arithmetic
Probst Dieter, Strahm Thomas (2011), Admissible closures of polynomial time computable arithmetic, in Archive for Mathematical Logic, 50(5-6), 643-660.
On the relationship between choice schemes and iterated class comprehension in set theory (PhD dissertation)
Juerg Kraehenbuehl (2011), On the relationship between choice schemes and iterated class comprehension in set theory (PhD dissertation), dissertation, Bern.
Realizability in weak systems of explicit mathematics
Spescha Daria, Strahm Thomas (2011), Realizability in weak systems of explicit mathematics, in Mathematical Logic Quarterly, 57(6), 551-565.
The provably terminating operations of the subsystem PETJ of explicit mathematics
Probst Dieter (2011), The provably terminating operations of the subsystem PETJ of explicit mathematics, in Annals of Pure and Applied Logic, 162(11), 934-947.
The Suslin operator in applicative theories: its proof-theoretic analysis via ordinal theories
Jäger Gerhard, Probst Dieter (2011), The Suslin operator in applicative theories: its proof-theoretic analysis via ordinal theories, in Annalas of Pure and Apllied Logic, 162(8), 647-660.
$\Sigma^1_1$ choice in a theory of sets and classes
Jäger Gerhard, Krähenbühl Jürg (2010), $\Sigma^1_1$ choice in a theory of sets and classes, in Ways of Proof, MünsterOntos Verlag, Frankfurt.
Unfolding finitist arithmetic
Feferman Solomon, Strahm Thomas (2010), Unfolding finitist arithmetic, in Review of Symbolic Logic, 3(4), 665-689.
Weak theories of operations and types
Strahm Thomas (2010), Weak theories of operations and types, in Ways of Proof, MünsterOntos, Frankfurt.
Elementary explicit types and polynomial time operations
Spescha Daria, Strahm Thomas (2009), Elementary explicit types and polynomial time operations, in Mathematical Logic Quarterly, 55(3), 245-258.
Full operational set theory with unbounded existential quantification and power set
Jäger Gerhard (2009), Full operational set theory with unbounded existential quantification and power set, in Annals of Pure and Applied Logic, 160(1), 33-52.
Operations, sets and classes
Jäger Gerhard (2009), Operations, sets and classes, in Glymour C. Wei W. Westerstahl D. (ed.), College Publications, King's College, London, 74-96.
Weak systems of explicit mathematics (PhD dissertation)
Spescha Daria (2009), Weak systems of explicit mathematics (PhD dissertation), Dissertation, Bern.
An algorithmic interpretation of a deep inference system
Brünnler Kai, McKinley Richard (2008), An algorithmic interpretation of a deep inference system, in Logic for Programming, Artificial Intelligence, and Reasoning, Doha, QatarSpringer, Lecture Notes in Artificial Intelligence, 5330, Berlin.
Primitive recursive selection functions for existential assertions over abstract algebras
Strahm Thomas, Zucker Jeff (2008), Primitive recursive selection functions for existential assertions over abstract algebras, in Journal of Logic and Algebraic Programming, 76(2), 175-197.
Soft linear set theory
McKinley Richard (2008), Soft linear set theory, in Journal of Logic and Algebraic Programming, 76(2), 226-245.

Collaboration

Group / person Country
Types of collaboration
Universität München Germany (Europe)
- in-depth/constructive exchanges on approaches, methods or results
- Exchange of personnel

Associated projects

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)

-