CLAR 2021: THE FOURTH INTERNATIONAL CONFERENCE ON LOGIC AND ARGUMENTATION
PROGRAM FOR FRIDAY, OCTOBER 22ND
Days:
previous day
all days

View: session overviewtalk overview

09:00-10:35 Session 7
09:00
On the Need of Knowledge for Computational Argument Analysis and Generation
10:00
Integrating Individual Preferences into Collective Argumentation
PRESENTER: Chonghui Li

ABSTRACT. In the field of collective argumentation, multiple agents may have distinct knowledge representations and individual preferences. In order to obtain reasonable collective outcome for the group, either individual frameworks should be merged or individual preference should be aggregated. However, framework merging and preference aggregation are different procedures, leading to disagreements on collective outcome. In this paper, we figure out a solution to combine framework merging, argumentative reasoning and incomplete preference aggregation together. Furthermore, a couple of rational postulates are proposed to be the criteria for the reasonability of collective outcome obtained based on our approach.

10:20
A Henkin-style completeness proof for the modal logic S5

ABSTRACT. This paper presents a recent formalization of a Henkin-style completeness proof for the propositional modal logic S5 using the Lean theorem prover. The proof formalized is close to that of Hughes and Cresswell [10], except that it is given for a system based on a different choice of axioms. Here the proof is based on a Hilbert-style presentation better described as a Mendelson system augmented with axiom schemes for K, T, S4, and B, and the necessitation rule as a rule of inference. The language has the false and implication as the only primitive logical connectives and necessity as the only primitive modal operator. The full source code is available online and has been typechecked with Lean 3.4.2.

10:35-10:50Coffee Break
10:50-12:05 Session 8
10:50
Tableau-Based Decision Procedure for Logic of Knowing-How

ABSTRACT. Recently, there has been an increasing interest in studying logic of knowing-how based on the idea of planning. In literature, it shows that the knowing-how logic based on 10 different types of plans is the same. In this paper, we present a tableau system for this knowing-how logic, and we show that there is an algorithm that runs in polynomial space for deciding whether a formula of the knowing-how logic is satisfiable. Since the knowing-how logic is an extension of epistemic logic which is Pspace-hard, it follows that the knowing-how logic is Pspace-complete.

11:10
A Logic for Binary Classifiers and their Explanation
PRESENTER: Xinghan Liu

ABSTRACT. Recent years have witnessed a renewed interest in Boolean function in explaining binary classifiers in the field of explainable AI (XAI). The standard approach of Boolean function is propositional logic. We present a modal language of a ceteris paribus nature which supports reasoning about binary classifiers and their properties. We study a family of classifier models, axiomatize it and show completeness of our axiomatics. Moreover, we prove that the variant of our modal language with finite propositional atoms interpreted over these models is NP-complete.We leverage the language to formalize counterfactual conditional as well as a bunch of notions of explanation such as abductive, contrastive and counterfactual explanations, and biases. Finally, we present two extensions of our language: a dynamic extension by the notion of assignment enabling classifier change and an epistemic extension in which the classifier’s uncertainty about the actual input can be represented.

11:30
Relevant Epistemic Logic with Public Announcements and Common Knowledge
PRESENTER: Igor Sedlar

ABSTRACT. Building on our previous work in non-classical dynamic epistemic logic, we add common knowledge operators to a version of public announcement logic based on the relevant logic R. We prove a completeness result with respect to a relational semantics, and we show that an alternative semantics based on information states is dual to the relational one. We add a question-forming inquisitive disjunction operator to the language and prove a completeness result with respect to the information semantics. It is argued that relevant public announcements are particularly suitable for modelling public argumentation.

11:50
The placeholder view of assumptions and the Curry–Howard correspondence

ABSTRACT. Proofs from assumptions are amongst the most fundamental reasoning techniques. Yet the precise nature of assumptions is still an open topic. One of the most prominent conceptions is the placeholder view of assumptions generally associated with natural deduction for intuitionistic propositional logic. It views assumptions essentially as holes in proofs (either to be filled with closed proofs of the corresponding propositions via substitution or withdrawn as a side effect of some rule), thus in effect making them an auxiliary notion subservient to proper propositions. The Curry-Howard correspondence is typically viewed as a formal counterpart of this conception. In this talk, based on my paper of the same name (Synthese, 2020), I will argue against this position and show that even though the Curry-Howard correspondence typically accommodates the placeholder view of assumptions, it is rather a matter of choice, not a necessity, and that another more assumption-friendly view can be adopted.

12:05-13:30Lunch/Coffee Break
13:30-15:15 Session 9
13:30
Towards a sound and complete dialogue system for handling enthymemes
PRESENTER: Andreas Xydis

ABSTRACT. A common assumption for argumentation-based dialogues is that any argument exchanged is complete, in the sense that its premises entail its claim. However, in real world dialogues, agents commonly exchange enthymemes --- arguments with incomplete logical structure. This paper formalises the dialogical exchange of enthymemes that are missing some constituent elements, such that it is not possible to directly entail the claim of the intended argument from the premises of the enthymeme exchanged. This can lead to misunderstandings between agents; we provide a rich set of locutions for identifying and resolving such misunderstandings, and a protocol that governs the use of these. We show that, under certain conditions, the status of moves made during a dialogue conforming to our system corresponds with the status of arguments in the Dung argument framework instantiated by the contents of the moves made at that stage in the dialogue. This is significant since it ensures that the use of enthyememes does not prevent the agents from reaching the appropriate decision according to the information they have shared.

13:50
How Can You Resolve a Trilemma? - A Topological Approach -
PRESENTER: Kazuko Takahashi

ABSTRACT. This paper discusses how to escape a state in which argumentation can reach no conclusion by offering a new argument. We formalize our approach based on Dung's abstract argumentation framework (AF). When an AF has no stable extension, we have no meaningful conclusion. We address the problem of whether it is possible to revise this situation by adding an argument which attacks an existing one. If possible, how many solutions can we generate and at what position should it be added? We discuss this problem using an AF consisting of a trilemma and show conditions depending on the topology of the AF. We also address the point that a specific argument can be accepted or not by this action. We extend the discussion towards two possible directions: a general N-lemma case and a set of AFs each of which consists of several trilemmas. It follows that when a large size of argumentation becomes stuck in practical situation, the position to which a counter-argument should be added can be detected by a check of the topology of the AF.

14:10
A variant with the variable-sharing property of Brady's 4-valued implicative expansion BN4 of Anderson and Belnap's logic FDE

ABSTRACT. A logic L has the "variable-sharing property"(VSP) if in all L-theorems of conditional form antecedent and consequent share at least a propositional variable. Anderson and Belnap consider the VSP as a necessary property any relevance logic has to fulfil. Now, among relevance logicians, Brady's logic BN4 is widely viewed as the adequate implicative 4-valued logic. But BN4 does not have the VSP. The aim of this paper is to define a variant of BN4 having, in addition to the VSP, some properties that do not support its consideration as a mere artificial construct.

14:30
Paranegations and The Square of Opposition
PRESENTER: Mariusz Urbanski

ABSTRACT. In this paper, a description of semantics for non-classical negations of paralogics CLuN and CLaN is presented in terms of the square of opposition. An outline of a synthetic tableaux method for these and some other paralogics is given as well.

14:45
Entailments with sentential predicates

ABSTRACT. A model accounting for entailments between sentential predicates formed from verbs of propositional attitude is proposed. In his model no reference o propositions is made. Sentential predicates denote set of sentences of a given natural language. This approach avoids the problem of intensionality and permits to use various tools from the generalise quantifier theory.

15:00
Validity under Assumptions

ABSTRACT. Slightly altering and extending McGee's semantics for conditionals, we define a ternary notion of validity for natural language arguments, which can be regarded as a unification of two kinds of validity in the literature. By the new notion of validity, an inference is not just valid or invalid, but valid or invalid under a set of assumptions. Based on this notion, we give a unified solution to some typical puzzles concerning conditionals and epistemic modals, including the (in)validity of modus ponens, modus tollens, Import-Export, conditional excluded middle, Or-to-If, and fatalism arguments, as well as the puzzle of Moore sentences and the scope ambiguity problem in modal conditionals.