Changes

The University of Calgary is moving its websites to a Content Management System (Drupal, to be specific). My homepage is scheduled to be migrated tonight. Now, I've tried very hard to not break any URLs or links (the IT people probably hate me by now), but there will be some changes. For instance, all the … Continue reading Changes

TYPES Summer School 2007

TYPES Summer School 2007Proofs of Programs and Formalisation of MathematicsAugust 19-31 2007, Bertinoro, Italyhttp://TypesSummerSchool07.cs.unibo.it During the last ten years major achievements have been made in using computers for interactive proof developments to produce secure software and to show interesting mathematical results. Recent major results are, for instance, the complete formalisation of a proof of the … Continue reading TYPES Summer School 2007

Philosophy Spin-offs

Mark Lance posted this insightful message to FOM yesterday, in response to this thread on "progress in philosophy": "The aim of philosophy, abstractly formulated, is to understand how things in the broadest possible sense of the term hang together in the broadest possible sense of the term. Under "things in the broadest possible sense" I … Continue reading Philosophy Spin-offs

Icosidodecahedral prismatohexacosihecatonicosachoron

Alasdair Urquhart was nice enough to identify the model that's dominating the lounge at BIRS. It's an icosidodecahedral prismatohexacosihecatonicosachoron, and is made of 120 icosidodecahedra, 600 cuboctahedra, 720 pentagonal prisms, its faces are 3600 triangles, 3600 squares, 1440 pentagons, and it has 10,800 edges. I'm sure it's got something to do with E8 (the mapping … Continue reading Icosidodecahedral prismatohexacosihecatonicosachoron

Species/the Reasoner

My colleague Marc has updated his SEP entry on Species. Jon Willimason is starting a new online thing called The Reasoner. The Reasoner is a monthly digest highlighting exciting new research on reasoning and interesting new arguments. It is interdisciplinary, covering research in, e.g., philosophy, logic, AI, statistics, cognitive science, law, psychology, mathematics and the … Continue reading Species/the Reasoner

LaTeX trick: rising diagonal dots

Just in case you ever need it: \ddots going the other direction: \makeatletter\def\Ddots{\mathinner{\mkern1mu\raise\p@ \vbox{\kern7\p@\hbox{.}}\mkern2mu \raise4\p@\hbox{.}\mkern2mu\raise7\p@\hbox{.}\mkern1mu}}\makeatother Then you can say: \varepsilon_0= \omega^{\omega^{\Ddots}}

Antimeta

For some reason I missed the memo that said that Kenny Easwaran's blog moved from antimeta.org to his Berkeley webspace.

Modality Morning

This morning has two talks on modal logic: first up was Marcus Kracht with a survey on the development of modal logic; now Steve Awodey is reporting on joint work with Kishida on topological semantics of first-order modal logic. Marcus talked about some interesting results in the mathematics of modal logic, especially general semantics for … Continue reading Modality Morning

Why the Faculty Scholarly Productivity Index doesn’t mean anything in philosophy

Ok. Brit posted about it. Apparently some people claim that the Faculty Scholarly Productivity Index (FSP) shows something about the rankings produced by the Philosophical Gourmet Report (PGR) (e.g., that they're off). But it doesn't. That is not because the PGR is actually the best possible way to measure program or even faculty quality. It … Continue reading Why the Faculty Scholarly Productivity Index doesn’t mean anything in philosophy

Kurt Gödel in the Stanford Encyclopedia

Juliette Kennedy's entry on Kurt Gödel has just been published in in the Stanford Encyclopedia.(It took a long time to get this done because of all the formulas that needed to be converted into HTML. If you find a mistake, please let Juliette or me know.)

Philosophy Genealogy

I just noticed that Josh Dever's Philosophy Family Tree now comes with a little Java applet that gives you a list of your philosophical ancestors (easier to use than the PDF list).Josh, any plans to make the tree capable of dealing with more than one advisor?

A complete first-order temporal logic of time with gaps

Source

Theoretical Computer Science 160 (1996) 241-270
(with Matthias Baaz and Alexander Leitsch)

Abstract

The first-order temporal logics with □ and ○ of time structures isomorphic to omega (discrete linear time) and trees of omega-segments (linear time with branching gaps) and some of its fragments are compared: The first is not recursively axiomatizable. For the second, a cut-free complete sequent calculus is given, and from this, a resolution system is derived by the method of Maslov.