Interesting Research: mostly proof theory
Dec. 31st, 2003 12:11 am![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
guslDeep Inference and Symmetry in Classical Proofs (includes an Intro to Proof Theory)
http://www.iam.unibe.ch/%7ekai/Papers/phd.pdf
Inference and Deduction: An Approach Integrating Logic and Probability
http://www.iam.unibe.ch/%7Etil/projects/InferenceDeduction.html
Proof Theory
http://alessio.guglielmi.name/res/cos/index.html
http://www.ki.inf.tu-dresden.de/~guglielm/WPT2/
includes
Proof Analysis
Explicit Mathematics
Proof Theory with Deep Inference
As we discovered recently, deep inference allows for a radically new, simple and elegant proof theory, when coupled with a notion of premise-conclusion symmetry. A new range of possibilities is open, with direct impact on computer science. We can in fact design deductive systems for important logics, like classical, linear and modal logics, whose rules are all local and atomic, including cut, contraction, promotion, additive context management, etc. Moreover, several modularity properties hold that are provably impossible for shallow calculi. We can study logics arising from process algebras for which no presentation in shallow calculi exists. We can also study new, meaningful notions of normalisation.
http://www.iam.unibe.ch/%7ekai/Papers/phd.pdf
Inference and Deduction: An Approach Integrating Logic and Probability
http://www.iam.unibe.ch/%7Etil/projects/InferenceDeduction.html
Proof Theory
http://alessio.guglielmi.name/res/cos/index.html
http://www.ki.inf.tu-dresden.de/~guglielm/WPT2/
includes
Proof Analysis
Explicit Mathematics
Proof Theory with Deep Inference
As we discovered recently, deep inference allows for a radically new, simple and elegant proof theory, when coupled with a notion of premise-conclusion symmetry. A new range of possibilities is open, with direct impact on computer science. We can in fact design deductive systems for important logics, like classical, linear and modal logics, whose rules are all local and atomic, including cut, contraction, promotion, additive context management, etc. Moreover, several modularity properties hold that are provably impossible for shallow calculi. We can study logics arising from process algebras for which no presentation in shallow calculi exists. We can also study new, meaningful notions of normalisation.