Torben Braüner defends his thesis ”Hybrid Logic and Its Proof-Theory” in fulfillment of the requirements for the degree doctor scientiarum (dr.scient.).
The defence takes place at Roskilde University in Biografen/The Cinema, Building 41, on Thursday April 23rd 2009, at 1.00 pm.
- Stig Andur Pedersen, Professor of philosophy, Roskilde University,
- Patrick Blackburn, Director of Research, INRIA, France’s national organisation for research in computer science,
- Melving Fitting, Professor of computer science, philosophy, and mathematics, City University of New York.
Abstract of the thesis:
Hybrid logics are obtained by adding further expressive power to ordinary modal and temporal logic. The history of hybrid logics goes back to the philosopher Arthur Prior's work on temporal logic in the 1960s. The extra expressive power of hybrid logics is often useful. For example, when reasoning about time one often wants to formulate a series of statements about what happens at specific times, and ordinary modal logic simply does not allow this. The addition of hybrid-logical machinery increases the expressive power, but often decidability is retained, which is important for computational applications. Now, proof-theory is the branch of logic dealing with the notion of proof and formal systems for representing proofs. There is little consensus about proof-theory for ordinary modal logic, and many modal-logical proof systems lack important proof-theoretic properties. By giving a spectrum of well-behaved proof systems (natural deduction, Gentzen, tableau, and axiom systems) for a spectrum of hybrid logics (propositional, first-order, intensional first-order, and intuitionistic), this thesis demonstrates that the deficiencies of ordinary modal logic are remedied when hybrid-logical machinery is added. Besides remedying these deficiencies, the hybrid-logical proof-systems have independent computational as well as philosophical and mathematical motivations.
Copies of the thesis are available from the author (torben [at] ruc . dk).