Asian Workshop on Philosophical Logic

In this talk, I propose a kind of TW-models for epistemic logic (of knowledge and belief) which is constructed on the basis of Timothy Williamson’s knowledge first epistemology. I show that based on TW-models, Williamson’s knowledge account of assertion—‘One must: assert p only if one knows that p’—can be well-justified by stipulating the required semantic rule for the modal operator A (for ‘asserting’) in terms of the semantic rule for the modal operator K (for ‘knowing). And more importantly, on TW-models, the knowledge account of assertion would no longer suffer from the problem of logical omniscience, a problem which can be found in normal modal systems in general.

extended abstract (pdf)

Model checking is an algorithmic technique for verifying temporal properties of reactive and concurrent systems, and finite model checking has successful stories for finding fatal bugs in hardware and telecommunication protocols. Software, that is inherently infinite (such as integers, recursive procedure calls, threads, etc.), imposes new challenges on model checking techniques over infinite state space. This talk is dedicated to infinite model checking on pushdown systems and their practical applications to program analysis and verification.

extended abstract (pdf)

An agent may have incorrect perception or observations to the visible parts of the environment and the agent's knowledge is directly from her correct observations or is derived by her correct observations with her knowledge about the system. To catch the above idea, we present a model, called the interpreted perception system one. A logic of knowledge and certainty, called KC logic, is established based on this model. The interpreted perception system model may offer a computationally grounded model, in terms of the states of computer processes, to those epistemic logics other than S5.

In this paper we porpose Hoare style proof systems called PR⁰_D and PRKW⁰_D for plan generation and plan verification under 0-approximation semantics of the action language A_K. In PR⁰_D (resp. PRKW⁰_D), a Hoare triple of the form {X}c{Y }(resp. {X}c{KWp}) means that all literals in Y become true (resp. p becomes known) after executing plan c in a state satisfying all literals in X. The proof systems are shown to be sound and complete, more importantly, they provide a way to efficiently generate and verify longer plans from existing verified shorter plans by applying so-called composition rule, provided that enough number of shorter plans have been properly stored. The idea is essentially a tradeoff between space and time, we refer it to off-line planning and argue that it could be applied to real world domains.

abstract (pdf)

In this talk, I shall discuss my recent studies on relevant modal logics. Relevant modal logics are modal logics over relevant logics. The objective of relevant log ics is to avoid the paradoxes of classical logic, i.e., paradoxes of relevance and consistency. In general, modal logics are formalized by adding modal operators, f or example, necessity and possibility, to classical logic. Modal logics based on n on-classical logics, including intuitionistic modal logics and relevant modal logi cs, have attracted considerable interest from the viewpoint of human thought and applications to computer science.

extended abstract (pdf)

We first present a short introduction illustrating how argumentation could be viewed as an universal mechanism humans use in their practical reasoning where by practical reasoning we mean both commonsense reasoning and reasoning by experts as well as their integration. We then present logic-based argumentation employing implicit or explicit assumptions. Logic alone is not enough for practical reasoning as it can not deal with quantitative uncertainties. We explain how probabilities could be integrated with argumentation to provide an integrated framework for jury-based (or collective multiagent) dispute resolution.

In this talk, we discuss the unification problems in normal modal logics without weak transitivity, in particular, with the axiom of symmetry (p-> Box Dia p). We will see some particular logics that play the role of boundary of the classification of unification type in the lattice of normal modal logics over some logics with B-axiom. This is another part of the joint work with Prof. Wojciech Dzik in last autumn.

Solutions to the semantic paradoxes abound in literature, but not many of them have the merit of maintaining the soundness of Tarski’s T-schema. In this regard, dialetheist solutions are of special interest. Dialetheism is the view that some contradictions (sentences of the form "A /\ ¬A") are true, or, equivalently, the view that some sentences, those that are called "glut sentences", are both true and false. Liar sentences are typically regarded as examples of glut sentences. H. Field (2008) distinguishes two types of dialetheism: classical glut theories and paraconsistent dialetheism. Classical glut theories stick to classical logic with the unavoidable result that they all reject T-schema, so they will be excluded from further considerations in this talk. Paraconsistent dialetheism, on the other hand, takes the correct logic to be a certain version of paraconsistent logic in which the classical explosion rule fails, so that accepting both T-schema and true contradictions will not lead a dialetheist to the embarrassing conclusion that everything is true. Following G. Priest (1987, 2006), one may further distinguish two types of paraconsistent dialetheism: classical (paraconsistent) dialetheism and intuitionist (paraconsistent) dialetheism; the former accepts the law of excluded middle (LEM) and the principle of bivalence (BIV) while the latter rejects both. Most well-known paraconsistent dialetheists, such as Priest and Jc Beall, are classical dialetheists. They hold the common view that truths and falsities are jointly exhaustive but not mutually exclusive, or, to say the same thing in different words, that every sentence is either true or false (where "x is false" is defined as "the negation of x is true"). The direct target of the present talk is classical dialetheism and I will argue that a paraconsistent dialetheist had better be an intuitionist.

extended abstract (pdf)

The duality of validity and unsatisfiability in classical logic generated a focus on questions of validity in nonclassical logics. For many applications, (un)satisfiability is the more relevant concept. The failure of the duality mentioned leads to many open problems related to properties of (un)satisfiability. We use Gödel logics as prime examples.

Hybrid logic is an extended modal logic with nominals i (a syntactic name of a state) and satisfaction operators @i φ (φ is true at the named state by i). In this talk, I will propose how to combine two hybrid logics, i.e., a way of dealing with two dimensions (e.g. any two domains from time, space, possible worlds, and individuals) at the same time in one setting. My way of combining hybrid logics can be regarded as an expansion of product of modal logics.

extended abstract (pdf)

In this talk, I will present the main results of my book Reasoning about Preference Dynamics (Springer, 2011). The book proposes a uniform logical theory of preference, drawing together ideas from several areas: Modal logics of betterness relations, dynamic epistemic logics of information change, and priority-based systems of representing structured preference relations. It developed a two-level view of preference that fits very well with realistic architectures of agency, closer to cognitive reality. I will focus on the logical study of acts and events that change information, and that may even change our evaluation of the world, changing our preferences. I will also discuss the entanglement of preference, knowledge and belief, illustrating the crucial interplay of information and evaluation dynamics in successful rational agency. The result can be applied in analyzing preferences in a wide variety of fields. I will show some case studies on deontic reasoning and on games.