Xixi Logic Seminars #70

Speaker: Ryuta Arisaka (National Institute of Informatics, Japan)
Date & Time: 14-16 June 2017
Place: Seminar Room #259, Main teaching building, Xixi campus, Zhejiang University

BI Proof theory (14 June 2017, 10:00-11:30 AM)

BI is a combined logic. It is a basis of Separation Logic which is widely known in programming community for its local reasoning. While classical negation is allowed in Separation Logic, BI is intuitionistic. It combines intuitionistic logic and multiplicative intuitionistic linear logic. Despite many years since its appearance, development of its proof theory has been slow. In particular, while decidability of BI was stated in one paper, still no decision procedures are known for BI. To address this shortage in the literature, a reasonable approach is to start with sequent calculus which is a formalism suitable for automated reasoning. As far as BI sequent calculus is concerned, decidability will follow if we show (1) elimination of structural rules that introduce copies of conclusion structures into premises (explicit elimination) and (2) elimination of any logical rules that introduce copies of conclusion formulas into premises ((3) and cut elimination). We present a BI sequent calculus that satisfies (1), to make a progress in this research problem.

Coordination of Dynamics and Statics in Abstract Argumentation: Coalition Formation (15 June 2017, 10:00-11:30 AM)

Static aspects of abstract argumentation have been studied extensively. AGM-like dynamic changes of argumentation frameworks are being studied relatively well, too. In comparison, coordination of dynamics and statics of argumentation is not so widely studied. It is becoming more and more important, however, to reason about evolving argumentation frameworks. It is useful (1) for better analysis of users sentiments and effective sales approaches and better marketing in business, or (2) for argumentation among teams, and so on. We consider a particular type of (2). In particular, we use vehicles of abstract argumentation (arguments and attacks among them) for developing semantics for coalition formation. The sort of coalition formation we have in mind is political alliance of political parties, which has interesting characteristics. For instance, normally, a political party is not free of internal conflicts. For another instance, the role of a politician in a political party varies, at times as an individual having political agendas, and at times as the political party’s member acting for the party. We represent a politician as an argument, a political party as a set of arguments, and contention in political perspectives as an attack. To model internal conflicts within a political party, we relax the Dung conflict-freeness into conflict-eliminability, allowing conflicts in a set of arguments so long as no arguments are defeated completely. In the characterisation of conflict-eliminability, we require numerical quantification of attack strengths as well as of argument strengths. To model the multiple roles of an argument, we consider coordination of static and dynamic argumentation. Based on certain argumentation-theoretic criteria such as defendedness, the number of attackers and the size of a set of arguments, we will first define semantics of coalition profitability of a given conflict-eliminable set forming a coalition with another conflict-eliminable set, and will show theoretical properties around coalition profitability. We will then provide 4 coalition formability semantics, each of which formalises certain utility postulate(s) taking the coalition profitability into account. Compared to the standard acceptability semantics, these semantics are more local, in that they are relativised to local sets of arguments.

Coordination of Dynamics and Statics in Abstract Argumentation: Persuasion (16 June 2017, 9:00-10:20 AM)

The act of persuasion is a key component in rhetoric argumentation. A persuasion act often entails alteration of an agent’s arguments into other arguments. So from one perspective it is a dynamics modifier. Whereas persuasion as a dialogue game is popularly being studied in the literature, an argumentation framework equipped with persuasion as a dynamic modifier is not. As day-to-day rhetoric argumentation particularly in social forums is not – contrary to the presumption in a dialogue game – necessarily turn-based between one group of proponent(s) and one group of opponent(s), there is a good incentive in studying an argumentation framework which could also treat concurrently running multiple persuasion dialogues. For that, instead of the standard turn-based mechanism, we extend Dung’s argumentation frameworks with persuasion relations. They function nearly the same way as dynamic operators in dynamic epistemic logic or assignments in programming languages. We define interactions between persuasion and attack in the dynamic argumentation framework, detail the notion of transitions, set forth properties related to arguments’ admissibility, and define a basic notion of admissibility. We show a way of enriching the basic admissibility through CTL (computation tree logic) encoding for useful inferences. Potential applications of the framework are in development of effective sales approaches and better marketing in business.

Discussion (16 June 2017, 10:30-11:30 AM)