Similarity in formal argumentation has recently gained attention due to its significance in problems such as argument aggregation in semantics and enthymeme decoding. While prior work has focused on propositional logic arguments, we extend these approaches to First-Order Logic (FOL) arguments, enabling reasoning based on the similarity of arguments in more complex and realistic contexts. We present a comprehensive framework for FOL argument similarity, including: 1. An extended axiomatic foundation for similarity measures, 2. A parametric model decomposed into four levels to eficiently evaluate structured knowledge, 3. A Tversky-based family of measures to instantiate these concepts, 4. A set of constraints ensuring well-behaved models that satisfy axioms, and 5. We introduce and analyze non-symmetric similarity measures in formal argumentation for the first time.
An argumentation system typically consists of two main components: a representation component, which structures information as a graph with arguments as nodes and binary relations between them (either positive, called support, or negative, called attack), and a reasoning component, which determines the acceptability of arguments according to argumentation semantics.
Formal argumentation has become an important area within knowledge representation and reasoning,
with applications in domains such as decision-making [
Across these diverse applications, a common concern has emerged: the need to reason not only about the presence of arguments and relations, but also about the degree of similarity between arguments. This notion, initially introduced in [9] for propositional arguments, has been formalized within an axiomatic framework to ensure that similarity measures satisfy desirable rational properties. Subsequent work [10, 11] has shown the practical benefits of these measures, in particular for avoiding redundancy and improving argument aggregation in gradual semantics, where each argument receives a numerical degree of acceptability. An argument is defined as a pair ⟨Premises, Claim⟩, where the premises aim to justify the claim. For instance, consider two arguments 1 = ⟨{1, 1 → }, ⟩ and 2 = ⟨{2, 2 → }, ⟩, which support the same claim through diferent reasoning. These arguments can be considered having some similarity, as they both justify the same claim. Now suppose they both attack a third argument = ⟨{¬ ∧ ¬}, ¬ ∧ ¬⟩. In gradual semantics, the degree of acceptability of an argument is often influenced by the number and the degree of acceptability of its attackers. Assuming that 1, 2, and 3 = ⟨{3, 3 → }, ⟩ all have equal degree of acceptability, the combined impact of the “similar” arguments 1 and 2 on should be lower than the combined impact of two “dissimilar” arguments, such as 1 and 3. The similarity between 1 and 2 reflects a form of redundancy, which should reduce their aggregated influence when computing the acceptability of . In this setting, similarity scores between arguments provide a principled way to adjust aggregation in order to avoid overestimating the efect of repeated or equivalent information.
Furthermore, the role of similarity has recently been extended beyond argument aggregation. In the
context of enthymeme decoding, similarity serves as one of the evaluation criteria to assess the quality
of a decoding (i.e. a reconstructed argument). More specifically, it quantifies how faithful a decoding is
to the original enthymeme (i.e. an incomplete argument) [
Overall, similarity between arguments should be seen as a core structural feature of argumentation systems, just like attack and support relations. However, existing studies on logical argument similarity remain largely confined to the propositional level, which limits their applicability. Many real-world arguments involve quantifiers, relational structures, and variables that propositional logic cannot adequately express. In this work, we address this gap by introducing a general framework for evaluating similarity between arguments expressed in first-order logic (FOL). We extend existing principles analysis to the FOL setting, and propose a four-level parametric model that captures the internal structure of FOL arguments, from atomic literals to sets of formulae. The framework is instantiated using Tverskybased similarity functions, guided by formal constraints that ensure compliance with the principles. Additionally, we provide an analysis of non-symmetric similarity in formal argumentation, highlighting its potential role in capturing directional similarities between arguments.
This framework is illustrated through examples but remains application-independent, making it suitable for integration into various reasoning settings, including but not limited to gradual semantics and enthymeme reconstruction. By moving beyond propositional logic, we aim to provide a more expressive and realistic foundation for reasoning about argument similarity in complex domains.
This paper simplifies our previous approach based on Order-Sorted (OS) FOL [ 12] by adopting standard, unsorted FOL. OS-FOL is more expressive in theory, but it requires explicit sort declarations and type-consistent instantiations, which are impractical in real-world settings, especially for natural language arguments, where such type information is often implicit or unavailable. By removing these constraints, the new framework becomes easier to apply and enables a reformulation of the principles based directly on similarities between predicates and constants, resulting in more precise definitions. Moreover, we revise the definition of instantiated arguments to ensure valid arguments (e.g. when instantiating existential claims, only those instances actually supported by the premises are retained). We also provide a deeper analysis of both symmetric and non-symmetric similarity models, including a characterization of the conditions under which total similarity (i.e., value 1) is achieved (Theorem 3). Finally, we include a brief related work section on logical similarity measures to situate our contribution.
First Order Logic is a rich framework that develops information about the objects and can also express the relationships between them (using predicates). For instance, let the constants = _ , = _ , and the predicates () = (), () = _ (), and () = _(). Using these, we can form statements like, (): “The tropical forest is a forest” or ∀ () ∧ () → (): “Any forest that undergoes massive deforestation will lose biodiversity”.
Definition 1. A First Order Language FOL, is a set of formulae built up by induction from: a set C of constants (C = {1, . . . , }), a set V of variables (V = {, , , . . .}), a set P of predicates (P = {1, . . . , }), a function ar : P → N which gives the arity of predicates, the usual connectives (¬, ∨, ∧, →, ↔), Boolean constants ⊤ (true) and ⊥ (false) and quantifier symbols ( ∀, ∃). A grounded formula is a formula without any variable.
We use lowercase greek letters (e.g. , ) to denote formulae, and uppercase ones (e.g. Φ, Ψ) to denote sets of formulae. The set of all FOL formulae is denoted by FOL. We assume formulae to be prenex, i.e. written as 11, . . . , where is a quantifier (for each ∈ {1, . . . , }) and is a non-quantified formula. A formula is in negation normal form (NNF) if it does not contain implication or equivalence symbols, and every negation symbol occurs directly in front of an atom (i.e., a predicate with its parameters). Following [13], we slightly abuse words and denote by NNF() the formula in NNF obtained from by “pushing down” every occurrence of ¬ (using De Morgan’s law) and eliminating double negations. For instance, NNF(¬(( () → ()) ∨ ¬())) = () ∧ ¬() ∧ (). In that case, we call literal either an atom or the negation of an atom. The set of grounded atoms is denoted by A. We denote by Lit() the set of literals occurring in NNF(), hence Lit(¬(( () → ()) ∨ ¬())) = { (), ¬(), ()}. For a given set of predicates P, we define L = { (1, . . . , ), ¬ (1, . . . , ) | ∈ P, ar( ) = , ≥ 0} the set of literals. We say that a literal is negative when it starts with a negation, denoted by Pol() = − . Otherwise it is positive and is denoted by Pol() = +. Two literals and ′ have the same polarity if Pol() = Pol(′). Finally, given a grounded literal = ± ( 1, . . . , ) where ± ∈ {+, −} indicates the polarity of , Pred() = is the name of the predicate underlying , and Para() = ⟨1, . . . , ⟩. Consider ∈ FOL, is in conjunctive normal form (CNF) if it is a conjunction of clauses ⋀︀ where each clause is a disjunction of literals ⋁︀ . For instance () ∧ (() ∨ ()) is in CNF while ( () ∧ ()) ∨ () is not. Clauses can be represented as sets of literals, and CNF formulae as sets of clauses.
FOL formulae are evaluated via a notion of structure, i.e. a triplet St = (, , ) where is the (non-empty) domain, = {1, . . . , } are relations over the domain, and = {1, . . . , } are constants in the domain.
Definition 2. An interpretation ISt over a structure St assigns to elements of the FOL vocabulary some values in the structure St. Formally, ∙ I St( ) = , for ∈ {1, . . . , } (each predicate symbol is assigned to a relation), ∙ I St( ) = , for ∈ {1, . . . , } (each constant symbol is assigned to a constant value).
Then satisfaction of formulae is recursively defined by: ∙ I St |= (1, . . . , ) if ( 1, . . . , ) ∈ , ∙ I St |= ∃ if I St,← |= for some ∈ , ∙ I St |= ∀ if I St,← |= for each ∈ , ∙ conjunctions, disjunctions and negations are interpreted as usually in classical logic, where ISt,← is a modified version of ISt s.t. the variable is replaced by a value in the domain . Finally, if Φ is a set of formulae, then ISt |= Φ if I St |= for each ∈ Φ.
We say that Φ is consistent if there is at least one interpretation ISt s.t. ISt |= Φ.
We now define instantiations as grounded formulae compatible with a given FOL formula. Definition 3. Given Φ a set of FOL formulae and ISt an interpretation over a structure St, the set of instantiations of Φ is defined recursively by: ∙ Inst ISt (Φ) = {Φ} if Φ = {}, where is a grounded formula s.t. ISt |= , ∙ Inst ISt (Φ) = {InstISt ({← | ISt |= ← , ∈ })} if Φ = {∀}, ∙ Inst ISt (Φ) = {InstISt ({← | ISt |= ← , ∈ }) | ∅ ⊂ ⊆ } if Φ = {∃}, ∙ Inst ISt (Φ) = {1 ∪ 2 | 1 ∈ InstISt ({1}), 2 ∈ InstISt (Φ2), ISt |= 1 ∪ 2} if Φ = {1} ∪ Φ2 with 1 ̸∈ Φ2, where ← is the formula s.t. all the occurrences of the variable are replaced by the value .
The idea is that formulae with quantified variables may be instanciated in various ways. Assuming that for a predicate and an interpretation ISt, we have ISt |= { (), ()}; then InstISt (∃ ()) = {{ ()}, { ()}, { (), ()}} and InstISt (∀ ()) = {{ (), ()}}.
Moreover, an instantiation is consistent because of the constraint ISt |= 1 ∪ 2 in the last part of the definition. This constraint means that, if e.g., we consider the set of formulae {∃ (), ∃¬ ()}, then we keep only the instantiations where () is true and () is false, or the opposite. Example 1. Let Φ = {∃ () ∧ (), ∀ () ∧ () → ()} be a set of formulae with the interpretation ISt |= { () ∧ (), () ∧ ()}. We have InstISt (Φ) = { { () ∧ (), () ∧ () → (), () ∧ () → ()}, { () ∧ (), () ∧ () → (), () ∧ () → ()}, { () ∧ (), () ∧ (), () ∧ () → (), () ∧ () → ()}}.
From structure and interpretation, we define the consequence relation over FOL formulae. Definition 4. Let and be two FOL formulae. We say that is a consequence of , denoted by ⊢ , if for any structure St, and any interpretation ISt over St, ISt |= implies ISt |= . Two formulae , are equivalent (denoted ≡ ) if ⊢ and ⊢ .
A logic is a pair (, |∼) where is a set of formulae (i.e. a language) and |∼⊆ × is a consequence relation. An example of logic is (ℒ, ⊢) with ℒ an FOL language following Def. 1 and ⊢ the consequence relation from Def. 4. Logical arguments [14] are defined as follows: Definition 5. An argument built under a logic (, |∼) is a pair ⟨Φ, ⟩, where1 Φ ⊆ and ∈ , s.t. Φ is consistent, Φ|∼ , and ∄Φ′ ⊂ Φ s.t. Φ′ |∼ . An argument = ⟨Φ, ⟩ is trivial if Φ = ∅ and ≡ ⊤ . Φ is called the support (S() = Φ) and its claim (C() = ). The set of all arguments built under (, |∼) is denoted Arg().
Example 2. Let , ∈ Arg(ℒ) such that: = ⟨{∃ () ∧ (), ∀ () ∧ () → ()}, ∃ () ∧ ()⟩, = ⟨{ (), (), ∀ () ∧ () → ()}, () ∧ ()⟩.
In this paper, we assume an FOL language ℒ and focus on the arguments Arg(ℒ) built under the logic (ℒ, ⊢). Since logical arguments are mathematical objects satisfying some specific properties, instantiating them must be done with care, so we need to adapt the notion of instantiation of a set of formulae to take into account the particularities of arguments (for instance, the relation between the support and the claim or the minimality requirement).
Definition 6. Let = ⟨Φ, ⟩ be a logical argument and ISt an interpretation over a structure St, the set of instantiated arguments of is defined by:
InstISt () = {i = ⟨Γ, ⋀︁ Ψ⟩ | Γ ⊆ Δ ∈ Inst ISt (Φ), Ψ ∈ InstISt ({}), i ∈ Arg(ℒ)} We add the power “i” to an argument to indicate that we are considering its instantiated version. Example 3. From Example 1 the instantiations of the support of are: InstISt (S()) = { { () ∧ (), () ∧ () → (), () ∧ () → ()}, { () ∧ (), () ∧ () → (), () ∧ () → ()}, { () ∧ (), () ∧ (), () ∧ () → (), () ∧ () → ()}}.
Then for the claim: InstISt (C()) = {{ () ∧ ()}, { () ∧ ()}, { () ∧ (), () ∧ ()}}. Hence InstISt () = {i1 = ⟨{ () ∧ (), () ∧ () → ()}, () ∧ ()⟩, i2 = ⟨{ () ∧ (), () ∧ () → ()}, () ∧ ()⟩, i3 = ⟨{ ()∧(), ()∧() → (), ()∧(), ()∧() → ()}, ()∧()∧ ()∧()⟩}. Similarly, InstISt () = {1i = ⟨{ (), (), () ∧ () → ()}, () ∧ ()⟩}.
Two sets of formulae Φ, Ψ ⊆ ℒ are equivalent, i.e., Φ ∼= Ψ, if there is a bijection : Φ → Ψ s.t. ∀ ∈ Φ, ≡ () . We use this restricted equivalence notion to avoid equivalences that could be false due to incorrect information. For example the sets {(), () → ()} and {(), () → ()} should not be equivalent. However, we may want to consider that a set of formulae is equivalent with the conjunction of its elements (e.g. { (), ()} and { () ∧ ()} are equivalent). To make them equivalent, we borrow the method used in [15]. We transform every formula into a CNF, then we split it into a set containing its clauses. In our approach, we consider one CNF per formula. For that purpose, we use a finite sub-language ℱ of ℒ containing one formula per equivalent class and the formula should be in CNF. To ensure that ℱ is finite, we assume that the logical signature is also finite, meaning that the number of predicate symbols, constants, and function symbols is bounded. This assumption is not too restrictive in practice. In real-world applications, such as natural language processing (where textual input could be translated into FOL representations), the vocabulary used to express knowledge is typically finite. 1 ⊆ means is a finite subset of Definition 7. Let ℱ ⊂ ℒ s.t. ∀ ∈ ℒ, there is a unique ∈ ℱ s.t. ≡ , Lit() = Lit() and is a CNF formula. The transformation of formulae into the finite CNF language is written CNF() = .
Let ⊔(Φ) represent the compilation of Φ as a set of clauses. Intuitively, each formula can be viewed as a set of clauses with an associated sequence of quantifiers. A set of formulae is thus a set of clauses and a sequence of quantifiers, with variables renamed to prevent ambiguities. As an example, assume 1 = ∃ () ∧ () and 2 = ∃() ∨ (). We have ⊔({1, 2}) = ∃, ′{ (), (), (′) ∨ (′)}. Formally, for Φ = { | ∈ N} ⊆ ℱ , where is a non-quantified CNF formula (i.e., a set of clauses CNF() for some ∈ ℱ ), and is the sequence of quantifiers associated with , we define ⊔(Φ) = (*1 . . . * , ⋃︀ ⋃︀ * ), where a renaming is applied to each clause ( * ) and each sequence ∈Φ ∈ of quantifiers ( * ) in order to guarantee that no variable is shared between quantifiers * and * (with ̸= ) or between clauses coming from diferent formulae and (with ̸= ). We write ⊔() instead of ⊔({}), for ∈ ℱ .
Throughout the paper, we consider ⊔(Φ) as a set with a single formula, where the sequence of quantiifers is the concatenation of *1 . . . * and the non-quantified part is the CNF formula corresponding to the set of clauses ⋃︀ ⋃︀ * .
∈Φ ∈
For instance, ⊔({∀∃ (, ), ∀ 1() ∨ 2()}) = ⊔({∀1∃2 (1, 2) ∧ ∀3 1(3) ∨ 2(3)}) = {∀1∃2∀3 { (1, 2), 1(3) ∨ 2(3)}} .
Let us now introduce the notion of compiled argument.
Definition 8. The compiled argument of ∈ Arg(ℒ) is c = ⟨⊔(S()), C()⟩. The power “c” denotes the compiled version of an argument. The set of compiled instantiated arguments of is CI() = {ci = ⟨⊔(S(i)), C(i)⟩ : i ∈ InstISt ()}, where their compiled instantiated supports (resp. claims) are S() = {S(ci) : ci ∈ CI()} (resp. C() = {⊔(C(ci)) : ci ∈ CI()}). Example 4. From Example 3, the compilation of i3 and 1i are: c3i = ⟨{ (), (), ¬ ()∨¬()∨ (), (), (), ¬ () ∨ ¬() ∨ ()}, () ∧ () ∧ () ∧ ()⟩; 1ci = ⟨{ (), (), ¬ () ∨ ¬() ∨ ()}, () ∧ ()⟩. Moreover, consider ∈ Arg(ℒ) such that = ⟨{ ()∧()∧()}, ()∧()⟩, its compilation is: c = ⟨{ (), (), ()}, ()∧()⟩.
The compilation allows us to capture the similarity between () ∧ () and (), (). Moreover, we can see that the compilation c is not concise, as it includes irrelevant information (()) for its claim. As shown in [15], clausal arguments ensure conciseness.
Definition 9. Two arguments , ∈ Arg(ℒ) are equivalent, denoted by ≈ , if there is a bijection : S() → S() s.t. ∀Φ ∈ S(), Φ ∼= (Φ), and ′ : C() → C() s.t. ∀Ψ ∈ C(), Ψ ∼= ′(Ψ). Otherwise, ̸≈ (not equivalent).
: S() → S() s.t. ∀Φ ∈ S(), Φ ⊆ (Φ).
Let , ∈ Arg(ℒ), is a sub-argument of , denoted ⊑ , if there is a bijection
A similarity measure indicates whether two objects (e.g., predicates, or arguments) share some features.
Definition 11. For X a set of objects, a similarity measure on X is a function simX : X × X → [
In this section, we focus on similarity measures over arguments, i.e., X = Arg(ℒ), assuming the existence of simP (resp. simC), a similarity measures on predicates (resp. on constants). Intuitively, simArg(, ) is close to 0 if the diference between and is significant, and close to 1 if they are similar. Several principles that similarity measures should satisfy have been discussed in the literature [9, 16]. Some of the principles (Maximality, Symmetry, Substitution, and Syntax Independence) can be stated exactly as in [15], since they do not concern the internal structure of the arguments. Notice that some authors have argued against the fact that a similarity measures should absolutely satisfy symmetry [17, 18]. The others must be adapted to our FOL-based arguments.
Principle 1 states that arguments sharing no content should have a similarity of 0. While in propositional logic, identifying common atoms is enough, here we must consider predicates and constants. In the context of quantified predicates, we instantiate the variables to analyse the constants. The next three principles consider only compiled instantiated arguments with no irrelevant information (first condition), ensuring safe handling of their similarity. In Principle 1, the second condition excludes the case where both arguments have an empty support and so no intersection to compare. The third (resp. fourth) condition ensures that the arguments have no similarity between the predicates and constants appearing in their support (resp. claim).
Principle 1. Let ISt an interpretation over a structure St, a similarity measure simArg satisfies Minimality if ∀, ∈ Arg(ℒ), if ∀ ci ∈ CI(), ∀ci ∈ CI(): 1. ci, ci ∈ Arg(ℒ), 2. and are not trivial, 3. ∀ ∈ S(ci), ∀ ∈ Lit(), ∀ ∈ S( ci), ∀ ∈ Lit() , simP(, ) = 0, ∀ ∈ Para(), simC(, ) = 0, 4. ∀ ∈ ⊔(C(ci)), ∀ ∈ Lit(), ∀ ∈ ⊔(C( ci)), ∀ ∈ Lit(), simP( , ) = 0, ∀ ∈ Para(), ∀ ∈ Para(), simC( , ) = 0, then simArg(, ) = 0. ∀ ∈ Para(),
The second (resp. third) principle states that the more an argument shares formulae in its support (resp. claim) with an another one, the higher is their similarity.
The compound nature of arguments (support and claim) prevents guarantees when both are considered. Thus, the second condition neutralizes one part to focus on the other. For Principle 2 focusing on supports we ensure that we have identical or completely diferent claims. As for Principle 3, we ensure that the support are the same, otherwise with completely diferent support we will have also completely diferent claim. The third condition guarantees that supports (resp. claims) of and share more elements than those of and . The fourth condition indicates that the more distinct elements you have, the less similar you are. The fifth condition ensures the reliability of conditions 3 and 4 by guaranteeing that distinct elements of have no similarity with and .
Principle 2. Let ISt an interpretation over a structure St, a similarity measure simArg satisfies Monotony if ∀, , ∈ Arg(ℒ), if ∀ ci ∈ CI(), ∀ci ∈ CI(), ∀ci ∈ CI(): 1. ci, ci, ci ∈ Arg(ℒ), 2. ⊔(C(ci)) = ⊔(C(ci)) or ∀ ∈ ⊔(C(ci)), ∀ ∈ Lit(), ∀ ∈ ⊔(C( ci)), ∀ ∈ Lit(), simP( , ) = 0, ∀ ∈ Para(), ∀ ∈ Para(), simC( , ) = 0, 3. S(ci) ∩ S(ci) ⊆ S( ci) ∩ S(ci), 4. S(ci) ∖ S(ci) ⊆ S( ci) ∖ S(ci), and 5. for = S(ci) ∖ S(ci), ∀ ∈ , ∀ ∈ Lit(), ∀ ∈ S( ci) ∪ S(ci), ∀ ∈ Lit() , simP(, ) = 0, ∀ ∈ Para(), ∀ ∈ Para(), simC( , ) = 0, then simArg(, ) ≥ simArg(, ). ∙ (Strict Monotony) If the inclusion in condition 3. is strict or, S(ci) ∩ S(ci) ̸= ∅ and the inclusion in condition 4. is strict, then simArg(, ) > simArg(, ).
Dominance if ∀, , ∈ Arg(ℒ), if ∀ ci ∈ CI(), ∀ci ∈ CI(), ∀ci ∈ CI(): Principle 3. Let ISt an interpretation over a structure St, a similarity measure simArg satisfies 2. S(ci) = S(ci), 1. ci, ci, ci ∈ Arg(ℒ), 3. ⊔(C(ci)) ∩ ⊔(C(ci)) ⊆ ⊔(C( ci)) ∩ ⊔(C(ci)), 4. ⊔(C(ci)) ∖ ⊔(C(ci)) ⊆ ⊔(C( ci)) ∖ ⊔(C(ci)), and simC(, ) = 0, simP(, ) = 0, ∀ ∈ Para(), ∀ ∈ Para(), then simArg(, ) ≥ simArg(, ). inclusion in condition 4. is strict, then simArg(, ) > simArg(, ). ∙ (Strict Dominance) If the inclusion in condition 3. is strict or, ⊔(C(i)) ∩ ⊔(C(i)) ̸= ∅ and the
Defining similarity between arguments involves analyzing multiple levels of their CNF structure. At each level, we provide an abstract definition of similarity measure using the previous level, followed by a possible instantiation.
Level 1: Compare pairs of literals (Section 4.1).
Level 2: Aggregate the similarity of pairs of literals to compare grounded clauses (Section 4.2).
Level 3: Combine the similarity of pairs of grounded clauses to compare instantiated supports or claims
(Section 4.3).
tion 4.4).
and claims obtained from Level 4.
4.1. Similarity between literals
Level 4: Compute the similarity between sets of instantiations, for each instantiated argument
(SecThe overall similarity between two arguments is obtained by combining the similarities of their supports
Definition 12. A similarity measure between two literals is a function simL : L × L → [
We now instantiate this abstract definition by computing similarity between literals via atom comparison (ignoring polarity), then adjusting scores based on polarity. In this instance, atom similarity depends on two factors: constant vectors and predicate values, with the functions “c” applying simC on each pair of constants and “p” which is a direct application of simP on the pair of predicates. Both are then combined using an aggregation function “g”.
Let c : ⋃︀+∞ ,=1 C × C
→ [
be a similarity measure between a pair of predicates and g : [
︁)
simA⟨g,p,c⟩ : A × A → [
A possible p is the function returning 1 if the predicates are the same, 0 otherwise. Let , be two arbitrary objects. The equality function eq : X × X → {0, 1} eq(, ) = 0 otherwise. We propose an instance of c suited to vectors of constants. is defined by eq(, ) = 1 if = ; or measure between constants. The pointwise similarity between and is:
Let = ⟨1, . . . , ⟩, = ⟨1, . . . , ⟩ be vectors of constants, and simC a similarity pwssimC(, ) = {︃ 1 ∑︀m=in1(,) simC(,) max(,) = = ⟨⟩ In this paper, we only use pwseq, which we simplify as pws.
We use polarities as binary criteria to determine whether two atoms can be considered similar. similarity measure between atoms simA⟨g,p,c⟩ such that: simL⟨g,p,c⟩(1, 2) =
define
simL⟨g,p,c⟩ : L × L → [
Let avg the average function, we denote simL⟨avg,eq,pws⟩ (resp. simA⟨avg,eq,pws⟩) by sL (resp. sA). Example 5. sL( (), ¬ ()) = 0 as they have opposite polarities, while sL( (, ), (, )) = 34 : sA( (, ), (, )) = avg(eq(, ), pws(⟨, ⟩, ⟨, ⟩)) = avg(1, eq(,)+eq(,) ) = avg(1, 12 ) = 34 . 2
We could use more sophisticated measures between literals, e.g. assigning a similarity score of 1 to semantically opposite predicates with opposite polarity, e.g., ¬() and (). For this, simC and simP should consider semantics rather than just syntax. Concretely, the function eq (in this work simP = simC = eq), could be replaced by a semantic similarity, e.g., using NLP techniques, such as cosine similarity between word embeddings (like Word2Vec [19], GloVe [20], or BERT-based models [21]). 4.2. Similarity between grounded clauses From levels 2 to 4, we use membership functions to assess an object’s similarity to a set. defined by: ⊕simX(, ) = ⊕ ′∈ (simX(, ′)).
simX a similarity measure on X, the membership function of in , ⊕simX : X × 2 X
→ [
The classical set-membership can be captured by meaqx. Now we can evaluate how much a literal is similar to a clause, i.e. a set of literals. We define the function sL = simL ⟨g,p,c⟩.
Let ∈ L be a literal, ⊆ L
literal in a set of literals by the function savLg : L × 2 L → [
be a set of literals. We define the membership of a asvLg(, ) = avg′∈(simL⟨g,p,c⟩(, ′)).
To compare a literal with a set of literals in a clause, we choose to use average aggregation instead of the similarity between two grounded clauses is computed by simGsavLg . max, as unlike conjunction, disjunction does not guarantee that the max similarity is meaningful. Then,
A similarity measure between two grounded clauses is a function simGsavLg :
2L × 2 L → [
In Def. 18, we define the similarity between two grounded clauses using a similarity measure (as in Def. 11), based on the membership function asvLg to compare literals with sets of literals (i.e., grounded clauses). Def. 18 outlines the general concept of grounded clause similarity. In this paper, we use Tversky’s ratio model [17] as a concrete approach, though other methods meeting the requirements of Def. 18 and 11 could also be used. Tversky’s ratio model [17] is a general family of similarity measures that includes well-known measures like [22], [23], [24], [25], and [26]. We extend it by using our parametrizable membership function (see Def. 16) instead of standard set membership operators.
Symmetric Measures
Tve1,1,⊕simX(, ) = jac⊕simX(, ) Tve0.5,0.5,⊕simX(, ) = dic⊕simX(, ) Tve0.25,0.25,⊕simX(, ) = sor⊕simX(, ) Tve0.125,0.125,⊕simX(, ) = adb⊕simX(, )
Tve2,2,⊕simX(, ) = ss⊕simX(, )
Non-Symmetric Measures Tve1,0,⊕simX(, ) = ns-jac⊕simX(, ) Tve0.5,0,⊕simX(, ) = ns-dic⊕simX(, ) Tve0.25,0,⊕simX(, ) = ns-sor⊕simX(, ) Tve0.125,0,⊕simX(, ) = ns-adb⊕simX(, )
Tve2,0,⊕simX(, ) = ns-ss⊕simX(, ) aggregation function and simX a similarity measure on X. Let be the average of the total similarity between the elements of with respect to , and the elements of with respect to ; and (resp. ) be the total dissimilarities of the elements of (resp. ) with respect to (resp. ), defined as follows: Let , ⊆ X be arbitrary sets of objects, ⊕simX be a membership function with ⊕ an • = avg︁( ∑︀ ∈ ⊕simX(, ), ∑︀ ∈ ⊕simX(, ) , ︁) • = ∑︀ • = ∑︀ ∈ (1 − ⊕simX(, )), ∈ (1 − ⊕simX(, )).
Let two coeficients , ∈ [0, +∞), the extended Tversky measure between and is: Tve,, ⊕simX (, ) = ︂{ 1
+(×)+(×) if = otherwise Classical similarity measures (see Table 1 in [9] for definitions) can be derived with = = 2 − , using classical set-membership. Specifically, the Jaccard measure ( jac) corresponds to = 0, Dice (dic) to = 1, Sorensen (sor) to = 2, Anderberg (adb) to = 3, and Sneath and Sokal (ss) to = −1. Moreover, when = the Tversky measure is symmetric. ⊕simX, we have Tve,, ⊕simX (, ) = Tve,,
⊕simX (, ).
Proposition 1. For any sets of objects , ⊆ X , any ∈ [0, +∞) , and any membership function including Jaccard, Dice, Sorensen, Anderberg, and Sokal and Sneath. are identical; in the non-symmetric case, if one is included in the other.
These measures satisfy intuitive properties: in the symmetric case, sets are maximally similar if they X, simX(, ) = 1. ∙ If = , then Tve ,, ∙ If ⊆ , then Tve max simX (, ) = 1 (symmetric case).
,0, msaixmX (, ) = 1 (non-symmetric).
Proposition 2. Let ∈ [0, +∞) , , ⊆ X , and simX respects the maximality property: ∀ ∈ avg Example 6. Let 1 = (, ), 2 = (, ), = (, ). = avg(saLvg(1, {2, }), saLvg(2, {1}) + saLvg(, {1})) Let sG = jacsL , then sG(Lit(1), Lit(2 ∨ )) = ++ ≈ 0.23 where: = avg(avg( 3 , 0), 34 + 0) = 0.5625;
4 = 1 − savLg(1, {2, }) = 1 − avg( = (1 − saLvg(2, {1})) + (1 − saLvg(, {1})) = 1.25.
34 , 0) = 0.625;
4.3. Similarity between sets of grounded clauses
Let G be the set of all grounded clauses in FOL. We define the function sG = simG savLg .
Definition 20. Let ∈ G and Δ ⊆ G . We define the membership of a grounded clause in a set of
grounded clauses by the function msaGx : G × 2 G → [
msaGx(, Δ) = max ′∈Δ(sG(, ′)).
is a function simIsmaGx : 2G × 2 G → [
We revisit Example 6, but we consider a conjunction instead of the disjunction of 2 and . Example 7. Let sG = jacsaLvg and sI = jacsmaGx , then sI({1}, {2, }) = ++ = 13 where: = avg(msaGx(1, {2, }), msaGx(2, {1}) + msaGx(, {1})) = avg(max( 3 , 0), 34 + 0) = 0.75;
4 = 1 − msaGx(1, {2, }) = 1 − max( 34 , 0) = 0.25; = (1 − msaGx(2, {1})) + (1 − msaGx(, {1})) = 1.25. 4.4. Similarity between instantiations Let I be the set of all instantiations in FOL which are sets of sets of grounded clauses, i.e., I = 22G , and sI = simIsmaGx .
Definition 22. Let Φ ∈ I and ⊆ I . We define the membership of an instantiation in a set of
instantiations by the function msIax : I × 2 I → [
msIax(Φ, ) = maxΦ′∈ (sI(Φ, Φ′)).
Definition 23. A similarity measure between two sets of instantiations is a function sS =
simSsmIax : 2I × 2 I → [
We call a similarity model (SM) any tuple M = ⟨sL, sG, sI, sS⟩ defining the 4 levels of similarity.
Reexamine arguments and , focusing on their compiled claim instantiations from Example 3. Example 8. Let the set of compiled instantiations of claim of and , C() = {Φ1 = { (), ()}, Φ2 = { (), ()}, Φ3 = { (), (), (), ()}} and C() = {Ψ = { (), ()}}. Let the Jaccard similarity model Mjac = ⟨sL, sG, sI, sS = jacsmaIx ⟩. sS(C(), C()) = ++ = 1.625+0.75+0 = 12..632755 ≈ 0.684, where:
1.625 = avg(︀ sI(Φ1, Ψ) + sI(Φ2, Ψ) + sI(Φ3, Ψ), max(sI(Ψ, Φ1), sI(Ψ, Φ2), sI(Ψ, Φ3)))︀ = avg(1 + 0.5 + 0.75, 1) = avg(2.25, 1) = 2.25+1 = 1.625
2 = (1 − sI(Φ 1, Ψ)) + (1 − sI(Φ 2, Ψ)) + (1 − sI(Φ 3, Ψ))
= (1 − 1) + (1 − 0.5) + (1 − 0.75) = 0 + 0.5 + 0.25 = 0.75 = 1 − max(sI(Ψ, Φ 1), sI(Ψ, Φ2), sI(Ψ, Φ3)) = 1 − 1 = 0
Using similarity models, we extend the work of [9] to assess the similarity between two FOL arguments.
Definition 24. Let a coeficient 0 < < 1 , a similarity model M = ⟨sL, sG, sI, sS⟩ and ISt an
interpretation over a structure St. Let , ∈ Arg(ℒ), we define the similarity between FOL
M, (, ) =
arguments from Arg(ℒ) × Arg(ℒ) to [
S(), S()) + (1 − ) × sS(
C(), C()).
simArgM simArgMns− Maximality Symmetry Substitution Syntax Independence Minimality Monotony Strict Monotony Dominance Strict Dominance Example 9. We conclude the example of and . Let Mjac = ⟨sL, sG, sI, sS⟩. CI() = {c1i = ⟨{ (), (), ¬ () ∨ ¬() ∨ ()}, () ∧ ()⟩, c2i = ⟨{ (), (), ¬ () ∨ ¬() ∨ ()}, () ∧ ()⟩, c3i = ⟨{ (), (), ¬ () ∨ ¬() ∨ (), (), (), ¬ () ∨ ¬() ∨ ()}, () ∧ () ∧ () ∧ ()⟩}; CI() = {1ci = ⟨{ (), (), ¬ () ∨ ¬() ∨ ()}, () ∧ ()⟩}.
As computed in Example 8, sS(S(), S()) = 12..63817255 ≈ 0.730, hence: simArgIMStjac, 12 (, ) = 21 × 21..36182755 + 12 × 21..367255 =
We present the notion of well-behaved similarity model where sL = simL⟨g,p,c⟩, linking the lower-level properties of measures (e.g., Tversky measures) to the higher-level properties of argument similarity. Definition 25. A similarity model M = ⟨sL = simL ⟨g,p,c⟩, sG, sI, sS⟩ is well-behaved if: 1. a) i. g(1, 1) = 1,
ii. g(0, 0) = 0, b) p(, ) = 1, c) i. c(⟨1, . . . , ⟩, ⟨1, . . . , ⟩) = 1, ii. let 1, . . . , , 1, . . . , ∈ C s.t. > 0, and > 0, if ∀ ∈ {1, . . . , }, ∀ ∈ {1, . . . , }, simC(, ) = 0, then c(⟨1, . . . , ⟩, ⟨1, . . . , ⟩) = 0, 2. Given X a set of objects, a) simX⊕s (, ) = 1 for any set of objects ⊆ X, b) if ∀ ∈ , ∀′ ∈ ′, s(, ′) = 0 then simX⊕s (, ′) = 0, c) let 0, 1, 2 ⊆ X s.t. 1 ⊂ 2 and 2 ∖ 1 = {2}. If ∃0 ∈ 0 s.t. s(0, 2) = s(2, 0) = 1 then simX⊕s (0, 2) ≥ simX ⊕s (0, 1), d) let 0, 1, 2 ⊆ X s.t. 1 ⊂ 2 and 2 ∖ 1 = {2}. If ∀0 ∈ 0, s(0, 2) = s(2, 0) = 0 then simX⊕s (0, 1) ≥ simX ⊕s (0, 2).
Where simC is the similarity between constants in c from sL. In the item 2. X may denote literals (L), grounded clauses (G), instantiations (I) or set of instantiations (S).
Theorem 1. For any similarity model M, if M is well-behaved then simArgIMSt, satisfies the following principles: Maximality, Minimality, Monotony and Dominance.
Theorem 2. Let a well-behaved similarity model M.
M, satisfies Symmetry (resp. Syntax Independence) if sL, sG, sI, sS are symmetric (resp. ∙ simArg ISt syntax independent). ∙ simArg IMSt, satisfies Strict Monotony and Strict Dominance if it satisfies 2.(c’) and 2.(d’), where 2.(c’) (resp. 2.(d’)) extends 2.(c) (resp. 2.(d)) by adding the condition simX⊕s (0, 1) < 1 (resp. simX⊕s (0, 1) > 0) to deduce their conclusion strictly (i.e., > instead of ≥).
Interestingly, some results from the propositional framework in [9] change in FOL: 1. The characterization linking the satisfaction of axioms to a similarity of 1 if arguments are equivalent is lost. 2. Argument compilation makes equivalent arguments identical, giving them a similarity of 1 solely via Maximality. 3. Logically non-equivalent arguments (e.g., with ¬() and ()) can also have a similarity of 1 if deemed similar by a similarity measure. 4. Substitution is no longer implied by other axioms, as the characterization of similarity of 1 for equivalent arguments no longer holds.
The functions g, p and c of this paper are well-behaved.
Lemma 1. For g ∈ {min, avg}, p = eq and c = pwseq, ⟨g, p, c⟩ satisfies item 1. of Def. 25. avg
Similar results hold for the Tversky measures used to define simGsL , simIsmaGx , and simSsmIax , as detailed in Table 1.
Lemma 2. If in Tve,, smiamxX , simX is either simL⟨g,p,c⟩ s.t. ⟨g, p, c⟩ satisfies item 1. of Def. 25, or a similarity measure satisfying item 2. of Def. 25, then Tve,, msaixmX satisfies item 2. of Def. 25. Proposition 3. Let simArgIMSt, with ∈ (0, 1) , ∈ {jac, dic, sor, adb, ss, ns-jac, avg ns-dic, ns-sor, ns-adb, ns-ss} and M = ⟨sL, sG = sL , sI = smaGx , sS = smaIx ⟩. All principles are compatible according to Table 2.
The symmetric extended Tversky measures returns a similarity of 1 if the arguments are equivalent. While non-symmetric measures also show full similarity in another specific case of sub-arguments. Theorem 3. Let , ∈ Arg(ℒ) and a similarity model M (resp. Mns − ) from Table 2. For any ∈ (0, 1) , we have: simArgIMSt, (, ) = 1 if ≈ ; and simArgIMStns−, (, ) = 1 if ⊑ and ⊔(C()) ⊆ ⊔(C()).
Asymmetric measures violate Strict principles and Substitution by scoring 1 for sub-arguments, preventing similarity increases for equivalent arguments and allowing difering argument structures to share a similarity of 1.
Several works have investigated similarity in logic-based or structured representation systems, but they difer significantly from our work w.r.t. expressivity, the nature of similarity, and intended applications.
Ramon and Bruynooghe [27] define a distance between first-order logic objects, focusing on the structural comparison of clauses and terms. Their approach operates within the syntax of FOL, without addressing quantified formulas explicitly, and relies on clause-level comparisons in normalized form. Similarly, Horváth et al. [28] define recursive similarity functions over first-order terms for instancebased learning, focusing on term structure rather than complete formulae. Their approach does not handle quantifiers or logical connectives. In contrast, our framework operates on FOL formulae with quantifiers and connectives, and supports similarity computation over structured arguments.
In contrast to syntactic or clause-based distances, Williamson [29] introduces a formal logic of comparative similarity using a ternary predicate (, , ), interpreted as “ is more similar to than to ”. While formally elegant, this qualitative approach lacks numerical scores and aggregation.
Similarity in ontology-based or object-oriented systems was studied in [30, 31]. Bisson [30] studies similarity based on hierarchies and attributes in object-oriented representations, but without a logical foundation. Ehrig et al. [31] propose a flexible multi-dimensional framework for ontology matching, but without schema-level comparisons, nor extension to FOL formulae or structured argumentation.
In the description logic (DL) community, several works attempt to define similarity between concepts. Borgida et al. [32] and Janowicz [33] propose semantically grounded measures for DLs, typically based on model-theoretic subsumption or concept overlap. However, DLs are restricted fragments of FOL: they do not support general quantification, nested terms, or logical connectives. In contrast, our framework is designed to operate on first-order logic, enabling a more expressive and flexible similarity computation.
González-Calero et al. [34] explore the use of description logics in case-based reasoning by representing cases as DL concepts and retrieving them via subsumption. While semantically grounded, their approach is limited to concept-level similarity and does not support the composition of similarity measures across multiple structural levels.
In summary, prior work relies either on syntactic distances over terms or clauses, qualitative reasoning frameworks without quantitative evaluation, or semantic similarity restricted to limited fragments such as description logics. In contrast, our contribution defines similarity directly over full first-order logic, supporting quantification and nested connectives, and provides a parametric multi-level model that evaluates similarity both at diferent structural levels within FOL formulae and within argument structures.
This paper introduces parametric similarity models, defining families of similarity measures for FOL arguments, including generalized versions of existing measures (i.e., Tversky) and, for the first time in logical argumentation, non-symmetric measures. Three extended principles are proposed, with wellbehaved properties ensuring the satisfaction of some principles. Symmetric Tversky-based measures satisfy all principles, while non-symmetric ones satisfy a subset.
This work opens new research avenues, as exploring additional measures (e.g., semantic similarity with BERT-based models [21]) and principles (e.g., independent distribution [35]) to improve similarity accuracy. Future work will focus on real-world applications, implementing similarity models, and analyzing their complexity.
This work was supported by the Agence Nationale de la Recherche (ANR) under the projects AGGREEY ANR-22-CE23-0005, AIDAL ANR-22-CPJ1-0061-01, and the Plan d’Investissement France 2030, as part of the Initiative d’Excellence d’Université Côte d’Azur under the reference ANR-15-IDEX-01.
The author(s) have not employed any Generative AI tools. [8] V. David, A. Hunter, A logic-based framework for decoding enthymemes in argument maps involving implicitness in premises and claims, in: IJCAI’25, 2025.
[9] L. Amgoud, V. David, Measuring similarity between logical arguments, in: KR’18, 2018, pp. 98–107. [10] L. Amgoud, V. David, An adjustment function for dealing with similarities, in: COMMA’20, 2020, pp. 79–90. [11] L. Amgoud, V. David, A General Setting for Gradual Semantics Dealing with Similarity, in:
AAAI’21, 2021. [12] V. David, J. Delobelle, J.-G. Mailly, Similarity measures between order-sorted logical arguments, in: Journées d’Intelligence Artificielle Fondamentale, 2023. [13] J. Lang, P. Liberatore, P. Marquis, Propositional independence-formula-variable independence and forgetting, J. Artif. Intell. Res. 18 (2003) 391–443. [14] P. Besnard, A. Hunter, A logic-based theory of deductive arguments, Artificial Intelligence 128 (2001) 203–235. [15] L. Amgoud, V. David, Similarity measures based on compiled arguments, in: ECSQARU’21, 2021, pp. 32–44. [16] L. Amgoud, V. David, D. Doder, Similarity measures between arguments revisited, in: ECSQARU’19, 2019, pp. 3–13. [17] A. Tversky, Features of similarity, Psychological Review 84 (1977) 327–352. [18] K. P. Jantke, Nonstandard concepts of similarity in case-based reasoning, in: Information Systems in Data Analysis: Prospects – Foundations – Applications, 1994, pp. 28–43. [19] K. W. Church, Word2vec, Natural Language Engineering 23 (2017) 155–162. [20] J. Pennington, R. Socher, C. D. Manning, Glove: Global vectors for word representation, in:
EMNLP’14, 2014, pp. 1532–1543. [21] N. Reimers, Sentence-bert: Sentence embeddings using siamese bert-networks, arXiv preprint arXiv:1908.10084 (2019). [22] P. Jaccard, Nouvelles recherches sur la distributions florale, Bulletin de la societe Vaudoise des sciences naturelles 37 (1901) 223–270. [23] L. Dice, Measures of the amount of ecologic association between species, Ecology 26 (1945) 297–302. [24] T. Sørensen, A method of establishing groups of equal amplitude in plant sociology based on similarity of species and its application to analyses of the vegetation on danish commons, Biol.
Skr. 5 (1948) 1–34. [25] M. Anderberg, Cluster analysis for applications. monographs and textbooks on probability and mathematical statistics, 1973. [26] P. Sneath, R. Sokal, Numerical taxonomy. The principles and practice of numerical classification., 1973. [27] J. Ramon, M. Bruynooghe, A framework for defining distances between first-order logic objects, in: ILP’98, 1998, pp. 271–280. [28] T. Horváth, S. Wrobel, U. Bohnebeck, Relational instance-based learning with lists and terms,
Machine Learning 43 (2001) 53–80. [29] T. Williamson, First-order logics for comparative similarity, Notre Dame J. Formal Log. 29 (1988). [30] G. Bisson, Why and how to define a similarity measure for object based representation systems,
Towards Very Large Knowledge Bases (1995) 236–246. [31] M. Ehrig, P. Haase, M. Hefke, N. Stojanovic, Similarity for ontologies-a comprehensive framework (2005). [32] A. Borgida, T. Walsh, H. Hirsh, et al., Towards measuring similarity in description logics., Description Logics 147 (2005) 1–8. [33] K. Janowicz, Sim-dl: Towards a semantic similarity measurement theory for the description logic alcnr in geographic information retrieval, in: OTM 2019 Conferences, 2006, pp. 1681–1692. [34] P. González-Calero, B. Díaz-Agudo, M. Gómez-Albarrán, et al., Applying dls for retrieval in case-based reasoning, in: DL’99, 1999. [35] V. David, Dealing with Similarity in Argumentation, Ph.D. thesis, Univ. Toulouse III, 2021.