A clausal resolution method for extended computation tree logic ECTL

A temporal clausal resolution method was originally developed for linear time temporal logic and further extended to the branching-time framework of Computation Tree Logic (CTL). In this paper, following our general idea to expand the applicability of this efficient method to more expressive formalisms useful in a variety of applications in computer science and AI requiring branching time logics, we define a clausal resolution technique for Extended Computation Tree Logic (ECTL). The branching-time temporal logic ECTL is strictly more expressive than CTL in allowing fairness operators. The key elements of the resolution method for ECTL, namely the clausal normal form, the concepts of step resolution and a temporal resolution, are introduced and justified with respect to this new framework. Although in developing these components we incorporate many of the techniques defined for CTL, we need novel mechanisms in order to capture fairness together with the limit closure property of the underlying tree models. We accompany our presentation of the relevant techniques by examples of the application of the temporal resolution method. Finally, we provide a correctness argument and consider future work discussing an extension of the method yet further, to the logic CTL^*, the most powerful logic of this class.     

Types of \mathsf{I} -Free Hereditary Right Maximal Terms

The implicational fragment of the relevance logic “ticket entailment” is closely related to the so-called hereditary right maximal terms. I prove that the terms that need to be considered as inhabitants of the types which are theorems of T_→ are in normal form and built in all but one case from and only. As a tool in the proof ordered term rewriting systems are introduced. Based on the main theorem I define FIT_→ – a Fitch-style calculus (related to FT_→) for the implicational fragment of ticket entailment.     

Plugging the Leaks in Neurath's Ship: A Defense of Naturalistic Epistemology

This paper examines the question whether foundational epistemology (“FE”) can be replaced by naturalized epistemology (“NE”). First, it argues that Quine's defense of NE is inadequate since it is only based on arguments showing the impossibility of the logical empiricist version of FE rather than on arguments for the impossibility of FE as such. Second, it proposes that a more promising argument for the impossibility of FE can be found in the Münchhausen-trilemma which aims at showing that ultimate foundations (and, hence, FE) are unattainable. However, Karl-Otto Apel has shown that this trilemma is unconclusive since it uncritically presupposes the premise that all argumentation is deductive in nature. Apel's argument implies that FE is possible if and only if it is possible to devise a non-deductive foundation (“NDF”). It is argued, however, that the possibility of NDF cannot be demonstrated. This leads to a situation called the Multatuli-dilemma: we cannot prove the possibility of ultimate foundations nor can we prove the impossibility of ultimate foundations. This dilemma shows that the discussion about the possibility of FE is pointless. Thus, it suggests that it is legitimate to replace FE by NE. Barry Stroud and Henri Lauener, however, argue that this replacement is not feasible since NE is not capable of refuting scepticism (Stroud) or justifying methodological rules (Lauener). But these objections are shown to be mistaken: First, epistemological scepticism is practically impossible and, hence, does not pose a serious threat to NE. Second, NE is capable of justifying methodological norms if and only if it makes use of so-called internal justifications. Thus, the final conclusion of this paper is that FE can be replaced by NE. This revised version was published online in August 2006 with corrections to the Cover Date.     

Kant and Kantian Themes in Recent Analytic Philosophy

This article notes six advances in recent analytic Kant research: (1) Strawson's interpretation, which, together with work by Bennett, Sellars, and others, brought renewed attention to Kant through its account of space, time, objects, and the Transcendental Deduction and its sharp criticisms of Kant on causality and idealism; (2) the subsequent investigations of Kantian topics ranging from cognitive science and philosophy of science to mathematics; (3) the detailed work, by a number of scholars, on the Transcendental Deduction; (4) the clearer understanding of transcendental idealism sparked by reactions to Allison's epistemic account; (5) the resulting need—prompted also by new studies of the thing in itself—to face up to the old question of the philosophical defensibility of such idealism; and (6) the active engagement with Kant's ethics and political philosophy that derives from Rawls's and others' work.     

Identical Twins,Deduction Theorems,and Pattern Functions: Exploring the Implicative BCSK Fragment of S5

We recapitulate (Section 1) some basic details of the system of implicative BCSK logic, which has two primitive binary implicational connectives, and which can be viewed as a certain fragment of the modal logic S5. From this modal perspective we review (Section 2) some results according to which the pure sublogic in either of these connectives (i.e., each considered without the other) is an exact replica of the material implication fragment of classical propositional logic. In Sections 3 and 5 we show that for the pure logic of one of these implicational connectives two – in general distinct – consequence relations (global and local) definable in the Kripke semantics for modal logic turn out to coincide, though this is not so for the pure logic of the other connective, and that there is an intimate relation between formulas constructed by means of the former connective and the local consequence relation. (Corollary 5.8. This, as we show in an Appendix, is connected to the fact that the ‘propositional operations’ associated with both of our implicational connectives are close to being what R. Quackenbush has called pattern functions.) Between these discussions Section 4 examines some of the replacement-of-equivalents properties of the two connectives, relative to these consequence relations, and Section 6 closes with some observations about the metaphor of identical twins as applied to such pairs of connectives.     

Using temporal logics of knowledge for specification and verification—a case study

Temporal logics of knowledge are useful for reasoning about situations where the knowledge of an agent or component is important, and where change in this knowledge may occur over time. Here we use temporal logics of knowledge to reason about the game Cluedo. We show how to specify Cluedo using temporal logics of knowledge and prove statements about the knowledge of the players using a clausal resolution calculus for this logic. We discuss the advantages and disadvantages of using this logic to specify and verify the game Cluedo and describe related implementations.