Discussion Graph Semantics of First-Order Logic with Equality for Reasoning about Discussion and Argumentation

There are several well-known models of discussion and argumentation. Some (such as Toulmin’s model [13], issue-based information systems [10] and argumentation schemes [14]) serve as a guideline for having a high-quality discussion, while others in the tradition of Dung’s argumentation model [5, 6, 3] offer logical reasoning capabilities through a set of logical principles. Most of these models are a graph structure (and even if they are a network, they can be normally reduced into a graph structure).

Each of the discussion models has been implemented and used in relevant fields: AI and Law [2], Education [8], Pragmatics/Rhetorics [9, 1], to name but a few. However, when it comes to formal reasoning, it is predominantly the second group of discussion models (in Dung’s tradition) to which much of the effort has been dedicated. There are many variations and extensions to Dung’s argumentation model defining the semantics of acceptability of arguments in argumentation.

However, most of the semantics of acceptability are intractable unless P = NP, and is therefore difficult to scale up to large graph structures such as may be obtained from a discussion forum on the Internet. Besides, there can be other reasoning tasks we may be interested in carrying out. Even the seemingly a lot simpler reasoning task of detecting a particular discussion structure pattern (that is, when the pattern is simple enough) can still come in handy. For example, we may be interested in learning about whether a discussion contains the structure pattern of Toulmins’ model, issue-based information systems or argumentation schemes. If the discussion does not contain the pattern, we may then be able to prompt discussion participants to supply missing components. The pattern detection albeit its simplicity (again, when the pattern is simple enough) is therefore useful.

The foregoing discussion points us to the direction of reasoning about discussion graphs in some formal language, accommodating the desired flexibility of stating any property that we may like to reason about about a discussion structure. However, currently, there is a conspicuous lack of a formal framework to reason about general discussion graphs. While a few proposals were advanced previously [12, 4], they are rather specific to handling Dung’s argumentation model for reasoning about the above-stated semantics of acceptability. They are constructed bottom-up, have in syntax syntactic components specific to Dung’s argumentation model, and are largely propositional. It is not immediate how they may be extended to reasoning about more general discussion graphs. The presence of special syntax makes it harder to identify connection to more standard formal logic.

Seeing the technical gaps, in this paper we develop a reasoning framework for discussion and argumentation in a top-down manner. For ensuring compatibility with existing formal logic, we do not invent a new logic. We use the syntax of first-order logic with equality. What we newly formulate is its discussion graph semantics in order to directly work with discussion and argumentation graph structures through it. Technically, we define the semantics of first-order logic formulas when the domain of discourse, i.e. an object-level semantic structure, is a discussion graph structure with annotations on nodes and edges. The key research question around our technical development is as follows:

Q In first-order logic dealing with sentences, a sentence (of potentially an arbitrary finite length) is a basic building block. If we take an analogy, in first-order logic dealing with discussion graph structures, a discussion graph (of potentially an arbitrary finite size) should be a basic building block, but how do we formulate this intuition into the semantics of first-order logic (with equality) so that the above-described pattern detection tasks and other reasoning tasks can be intuitively tackled with it?

We answer this question by allowing any predicate symbol to denote a graph structure with annotations. After formulating the discussion graph semantics of first-order logic (with equality), we show concrete examples illustrating how it is used for reasoning about: the aforementioned pattern detection of any annotated object-level graph structures; as well as some logical properties of them as in Dung’s argumentation model.

We introduce the syntax of first-order logic with equality succinctly.

A logical connective is any member of the set $\{\top,\bot,\forall,\exists,\neg,\wedge,\vee,\supset\}$. $\top$ and $\bot$ have the arity of 0; $\forall$, $\exists$ and $\neg$ have the arity of 1; and $\wedge$, $\vee$ and $\supset$ have the arity of 2. A variable is any member of an uncountable set $\boldsymbol{Vars}$. A logical symbol is one of the following: a logical connective, a variable, a parenthesis/bracket symbol (e.g. ‘(’, ‘[’, ‘)’, ‘]’), a punctuation symbol (e.g. ‘.’, ‘,’) or an equality symbol =.

A function symbol is any member of an uncountable set $\boldsymbol{Funcs}$ and each function symbol has an arity of some non-negative integer. It is assumed that there are infinitely many function symbols for each arity in $\boldsymbol{Funcs}$. A constant is a function symbol with the arity of 0. A predicate symbol is any member of an uncountable $\boldsymbol{Preds}$ and each predicate symbol has an arity of some non-negative integer. It is again assumed that there are infinitely many predicate symbols for each arity in $\boldsymbol{Preds}$. A propositional variable is a predicate symbol with the arity of 0. A non-logical symbol is one of the following: a function symbol (including a constant) or a predicate symbol (including a propositional variable).

The language for first-order logic, FOL, comprises all the logical and non-logical symbols. For convenience, any variable is denoted by $x$, any predicate symbol by $p$ and any function symbol by $f$. By $t$, we shall denote a term and by $\overrightarrow{t}$ we shall denote a tuple of $n\geq 0$ terms $(t_{1},\ldots,t_{n})$. The exact definition of a term is as follows. (1) Any variable is a term. (2) Any $f(\overrightarrow{t})$ for some function symbol $f$ of arity $n\geq 0$ and some tuple of $n$ terms $\overrightarrow{t}$ is a term. (3) Any term is recognised by (1) and (2) alone.

A formula $F$ is any of the following. (1) $p(\overrightarrow{t})$ for some predicate symbol $p$ of arity $n\geq 0$ and some tuple of $n$ terms $\overrightarrow{t}$. (2) $\top$ or $\bot$. (3) $\neg F_{1}$ for some formula $F_{1}$. (4) $\forall x.F_{1}$ or $\exists x.F_{1}$ for some variable $x$ and some formula $F_{1}$. (5) $F_{1}\wedge F_{2}$, $F_{1}\vee F_{2}$ or $F_{1}\supset F_{2}$ for some formulas $F_{1}$ and $F_{2}$. (6) $(F_{1})$ or $[F_{1}]$ for some formula $F_{1}$. (7) $t_{1}=t_{2}$ for some terms $t_{1}$ and $t_{2}$. A formula $F$ is well-formed iff there is no variable occurring free in $F$. As for the binding order of the logical connectives, $\neg$ binds strongest, $\wedge$ and $\vee$ bind the second strongest, $\forall$ and $\exists$ the third strongest, while $\supset$ binds the weakest.

When discussion models are extracted from natural language texts through mining [7, 11], they are often a graph structure with annotations on its nodes and edges. As such, it is only natural that we consider a graph structure with annotations as the domain of discourse of our semantic structure. We shall call the pair of: a graph structure; and a function assigning annotations (as strings) to the graph nodes and the graph edges an annotated graph. Fig. 1 shows at the top an example of annotated graph denoting a Toulmin’s model. This figure is actually a compact form of a graph (shown at the bottom left) and a function to assign annotations (partially shown at the bottom right). All the graphical representation of an annotated graph in the rest of this paper will be in the compact form.

To explain this annotated graph a little more in detail, $txt_{i}$ denotes some natural language text (as a string) and the empty annotation $\{\}$ (as an empty string) is used to signify a ‘whatever’ annotation. Now, Toulmin’s model is not originally a graph: an arrow from $txt_{2}$ actually goes to an arrow. In order to represent it in graph, we have converted the network into the annotated graph by inserting an auxiliary annotated node $txt_{5}:\{\}$ in the middle of the arrow from $txt_{4}:\{qualifier\}$ to $txt_{6}:\{claim\}$.

For other discussion models, Fig. 2 shows one example of Dung’s model and that of issue-based information systems. In the original Dung’s model, they do not care about annotations on texts/statements, so every text/statement is given $\{\}$ as its annotation. On the other hand, every edge is given $attacks$ annotation. In issue-based information systems, text/statement is given an annotation from $\{issue,position,argument\}$. Any $position$-annotated text/statement can have an edge only to $issue$-annotated texts/statements. Any $argument$-annotated text/statement on the other hand can have an edge only to $position$-annotated texts/statements. An $issue$-annotated text/statement can have an edge to any $issue$/$position$/$argument$-annotated text/statement. Each edge is given an annotation reflecting from which annotated text/statement to which annotated text/statement it goes.

In practice, we may not be obtaining from natural language text an annotated graph that perfectly matches one of these discussion models structure-wise. Fig. 3 shows one example which is almost a Dung’s model but with $questions$ annotation on one of the edges and with various annotations on texts/statements.

Consequently, it is necessary to recognise every annotated graph. The following definition formally characterises our domain of discoure. Here and elsewhere, $\mathfrak{p}(\ldots)$ denotes the power set of $...$

To be able to tell whether one object-level annotated graph is smaller than another, we define the following order relation $\unlhd$.

We formulated the discussion graph semantics of FOL and showed how it can be used to reason about object-level annotated graphs. The formulation is top-down, covering any object-level annotated graph. Moreover, it is predicate logic, meaning it is now possible to reason about object-level annotated graphs with variables and quantifications, in much the same way as we reason about object-level sentences. In the literature of argumentation, there are a couple of proposals [12, 4, 15] for using a formal logic for argumentation. However, they are constructed bottom-up, specific to Dung’s model [12, 4], lack variables and quantifiers [4], introduce new logical connectives for $attack$ and others [12], and include meta-properties of an object-level graph as propositional variables of the logic [4, 15]. As such, they are not readily extensible to reasoning about other discussion models. The embedding of meta-properties makes it harder to understand the syntactic-semantic correspondence, and a lack of quantifications results in a very long formal description. We have addressed these issues. There are a plenty of solvers and other implemented tools available for FOL. By staying within the realm of FOL, the benefit that we can receive from the vast literature of available formal techniques is immense.

To mention future work, this work should be a good foundation for an interesting interdisciplinary research of formal discussion/argumentation and program analysis/verification. We now have the FOL-based specification language for reasoning about general discussion graphs. Study into integrability of formal methods that exist in program analysis/verification into reasoning about discussion should naturally follow.

This work was supported by JSPS KAKENHI Grant Number 21K12028.