De Finettian Logics of Indicative Conditionals Part II: Proof Theory and Algebraic Semantics

In Part I of this paper, we identified and compared various schemes for trivalent truth conditions for indicative conditionals, most notably the proposals by de Finetti (1936) and Reichenbach (1935, 1944) on the one hand, and by Cooper (Inquiry, 11, 295–320, 1968) and Cantwell (Notre Dame Journal of Formal Logic, 49, 245–260, 2008) on the other. Here we provide the proof theory for the resulting logics and , using tableau calculi and sequent calculi, and proving soundness and completeness results. Then we turn to the algebraic semantics, where both logics have substantive limitations: allows for algebraic completeness, but not for the construction of a canonical model, while fails the construction of a Lindenbaum-Tarski algebra. With these results in mind, we draw up the balance and sketch future research projects.

Non-Analytic Tableaux for Chellas's Conditional Logic CK and Lewis's Logic of Counterfactuals VC

Priest has provided a simple tableau calculus for Chellas's conditional logic Ck. We provide rules which, when added to Priest's system, result in tableau calculi for Chellas's CK and Lewis's VC. Completeness of these tableaux, however, relies on the cut rule.

Building an Efficient OWL 2 DL Reasoner

The Ontology Web Language (OWL) has received considerable traction recently and is used in a number of industrial and practical applications. While decidable, all basic reasoning tasks for OWL are intractable (most of them are N2ExpTime-complete). Thus, in order to obtain a system capable of solving practically-relevant nontrivial problems, a number of theoretical and practical issues need to be resolved. In my talk I will present an overview of the techniques employed in HermiT, a state-of-the-art OWL reasoner developed at Oxford University. I will present the main ideas behind the hypertableau calculus and contrast them with the tableau calculi used in similar systems. Furthermore, I will discuss optimization techniques used in HermiT such as the blocking cache, individual reuse, and core blocking. Finally, I will discuss certain higher-level optimizations implemented on top of the basic calculus, such as the recently-developed optimized classification algorithm.

Synthesising and Implementing Tableau Calculi for Interrogative Epistemic Logics

This paper presents two tableau provers for deciding interrogative-epistemic logics. They are both based on a tableau calculus generated using a recently introduced tableau synthesis framework. We have implemented the calculus using two approaches, namely Mettel2 and Qtab Here, we describe and compare these different approaches of implementing a tableau procedure.