Although logical inferences are interpretable, actually explaining them to a user is still a challenging task. While sometimes it may be enough to point out the axioms from the ontology that lead to the consequence of interest, more complex inferences require proofs with intermediate steps that the user can follow. Our main hypothesis is that different users need different representations of proofs for optimal understanding. To this end, we undertook some user experiments related to logical proofs. We explored how a user's cognitive abilities influence the performance in and preference for certain proof representations. In particular, we compared tree-shaped representations with linear, textbased ones, and for each we offered an interactive and a static version. After each proof, participants had to solve some tasks measuring their level of understanding and rated each proof according to the perceived comprehensibility. At the end of the questionnaire, subjects ranked the proofs by comprehensibility. We found no differences between the general performance or the subjective ratings of the proof representations. However, in the final ranking participants preferred the conditions with tree-shaped proofs over the textual ones, with significant differences in the rankings of the higher cognitive ability group and across both groups but not in the low cognitive ability group.
Research on explaining description logic inferences has mostly focused on
computing justifications [
Logical (abstract) reasoning is the ability to solve novel problems without
taskspecific knowledge and a core mechanism of human learning [
Our main goal in this paper is to find out whether a user’s logical ability
influences which of these four proof representations are preferred and lead to better
performance. A study from last year [
In a first experiment, we verified that the score on the standardized
International Cognitive Ability Resource (ICAR) test1 strongly correlates with the
ability to draw logical inferences and understand logical proofs. Based on this
insight, we used the ICAR in our second experiment to measure the user’s ability
levels and compare the different proof representations. To open our experiments
to a larger population, we decided not to use the formal DL syntax, but rather
hand-crafted textual representations of axioms, similar to the ones used in [
There are various fluid intelligence tests assessing logical ability, e.g. The Stanford
Binet Intelligence Scale, Fifth Edition (SB:V) [
In parallel, several approaches for converting description logic axioms and proofs into textual representations have been developed and evaluated [1, 6, 29, 33,
A v ⊥
O = { A v ∃r.>,
C u B v ⊥,
A v ∀r.(B u C) }
34]. For example, generation of verbalized explanations for non-trivial derivations
in a real world domain was tested on computer scientists in [
Concerning the representation of logical statements, we take the following
studies into the account. First, in [
We assume a basic familiarity with DLs, in particular ALCQ [
It is important that proofs are neither too detailed nor too short. In fact, a
justification can itself be seen as a one-step proof of an unintended entailment α,
but if each element of the justifications seems reasonable to the user, then it
can be hard to track down the precise interaction between these axioms that
causes the problem. Recall that axioms may still not behave as the user expects,
e.g. “every A has only rs” does not imply “every A has an r”. On the other
hand, by assumptions also made in [
A textual representation of a proof is necessarily a linearization, where the inference steps are explained in a sequence, for example in a top-down left-right order. A text corresponding to the formal proof in Figure 1 could be the following: Since every A has an r and every A has only rs that are Bs and Cs, every A has an r which is a B and a C. Since every A has an r which is a B and a C and there is no object which is a C and a B at the same time, there is no object in A.
Other aspects in which a text differs from a proof tree are that conjunctions (e.g. “since”, “and”) are used to illustrate proof steps and that statements may be repeated if they are reused later. For our second experiment, we used a flexible visualization of trees in which arrows are used instead of horizontal lines (see Figure 2 on page 9).
As described in the introduction, we do not use the formal DL syntax for
the experiments, i.e., also in the proof tree representation, A v ∃r.> would be
shown as “Every A has an r.” Moreover, we use nonsense names that vaguely
look and sound English to enable more natural-sounding sentences, e.g. “Every
woal is munted only with luxis that are kakes” instead of “Every A has only rs
that are Bs and Cs” (A v ∀r.(B u C)). We already faced a problem concerning
prior knowledge about the example domains in [
We first conducted an experiment that shows a connection between participants’ understanding of logical proofs and their general cognitive abilities. A printable version of the survey is available online.2 4.1
Description of the experiment Introduction and Goals. In our main experiment (Section 5), we want to distinguish user preferences based on their baseline level of ability to solve logical reasoning tasks. To this end, we want to employ a standardized measure that allows us to predict the performance on such tasks. Here, we first tested whether the ICAR16 questionnaire can be used for this purpose.
Design. We used LimeSurvey3 for hosting our fully online survey. Since we did not pre-screen (i.e., impose eligibility criteria on) our participants for experience with logic or proofs, we inserted a short introduction explaining the structure of proof trees. In order to exclude the effect of tiredness, the order of the ICAR16 questions and the proof tasks was randomized.
Participants. The sample consisted of 101 participants (45 female, 56 male) with a mean age of M = 24.52 (SD = 6.81). The age range spread between 18 and 48 years. Participants were recruited using Prolific4 and were paid 6€ for their participation. Apart from being at least 18 years old, there were no exclusion criteria. 28 participants who did not complete the survey were excluded (and not paid).
ICAR16. To assess the participants’ cognitive abilities, the abbreviated form
of the International Cognitive Ability Resource (ICAR16) [
Further Information. As further information, demographic data were collected (age, gender) as well as experience with propositional logic, from 1 (“no knowledge at all/no experience”) to 5 (“expert/a lot of experience”). After each proof task, the participants were asked to rate its difficulty on a scale from 1 (“very easy”) to 5 (“very difficult”).
Hypothesis. The ICAR16 score is an independent variable that, according to our hypothesis, predicts the performance in the logical proofs.
Results
Descriptive Results. The mean of the ICAR16 scores was M = .55 (SD = .24) with the participants’ performance being spread in a normal distribution. The maximal achieved score was 1, the minimum was 0. The mean of the score for both logical reasoning tasks was M = 15.99 (SD = 3.3), with the maximum score being 23 and the minimum 6. The performance in these tasks was also normally distributed across the participants. Moreover, the difficulty of the first task was rated with a mean of M = 3.64 (SD = .89). The difficulty of the second task was rated as M = 3.55 (SD = 1.14).
Regression analysis. A multiple regression analysis was carried out using the
performance in the logical reasoning tasks as the dependent and the ICAR16
performance as the independent variable. The ICAR16 score significantly predicted
the performance in the logical tasks (F (1, 99) = 43.15, p < .001). The ICAR16
explained 30% of the variation in the score of the logical tasks (R2 = .3, p <
.001), which can be interpreted as large effect size/high explained variance [
Given that ICAR16 scores are highly correlated with performance on logical reasoning tasks, we used it in our main experiment to distinguish participants by their logical ability level. A printable version of the survey is available online.5 5.1
Description of the experiment Introduction and Goals. With this experiment, we attempt to find out which proof representation is most understandable for different users. The goal is to find a difference in the (subjective) preferences and (objective) performance on each proof representation, depending on the user’s level of logical reasoning ability. Conditions. We used two different conditions (factors) with two levels each. One condition was the representational form of the proof, which was either tree-shaped or (linear) textual. The other condition was the interactivity of the proof representation, which was either static or interactive. Thus, there were the four following condition combinations: (ir) interactive tree, (sr) static tree, (ix) interactive text, and (sx) static text (see Table 1). We used a 2 × 2 within-subjects design, which means that each participant saw all four combinations. The independent variable in the main study is the ICAR16 score. Objective (the number of correct answers) and subjective (comprehensibility rating) performances on proofs as well as proof rankings are dependent variables. We conducted the experiment in English via LimeSurvey, with embedded links to the interactive proof representations that were hosted on our own server.
Design. The survey was again implemented using LimeSurvey. As in the first experiment, the order of the ICAR16 and the proof question groups was randomized. Moreover, each participant was randomly assigned to one of the four groups in Table 1. Before the proof tasks, we added a short explanation of the proof representation and a small training example on which the participants could explore both interactive formats.
Participants. The final sample consisted of 173 participants (41% female, 59% male) with a mean age of M = 24.8 (SD = 8.21) and an age range from 18 to 65 years. The mean of the participants’ experience with propositional logic was M = 1.76 (SD = 1). Furthermore, 60.7% of the participants indicated that they never worked with propositional logic. The participants were recruited using Prolific4 and were paid 10.20€ for their participation. Apart from being at least 18 years old, there were no exclusion criteria. 83 participants who did not complete the survey were excluded also by the platform. Due to technical errors, the proofs were not displayed for 3 participants, which were also excluded. Additionally, four attention checks were implemented in the study. 13 participants with more than 2 incorrectly answered attention checks were excluded as well.
ICAR16. Again, we used the ICAR16 questionnaire to assess the participants’ cognitive abilities (see page 5).
Proofs. We developed four artificial proofs of roughly the same difficulty level. The statements of each proof were given in textual form (also for the tree-shaped representations), with concept and role names replaced by nonsense words (see Section 3). For each of the four proofs, the proofs in both representation formats were created manually, not automatically. For the linear textual format, the individual statements were connected by additional words and statements were repeated if they were last mentioned more than 2 lines above. In Figures 2 and 2, we depict the textual and tree-shaped representations of Proof 1. Green color indicates the assumptions, intermediate deductions are marked in blue, and the final conclusion is colored orange.
The interactive version of the tree representation6 started with only the
final conclusion visible, and participants could interact with each node by using
three buttons. A button labeled “<” revealed the immediate predecessors of
the current node in the proof. The second button labeled “↑” could reveal the
whole subtree above the current node, and the last button labeled “↓” allowed
to collapse the subtree back to a single node. The interactive text7 worked
in a different way. At the beginning, participants saw only the first sentence,
i.e., the first assumption. Using two buttons labeled “>” and “<” they could
reveal the next sentence or hide the most recently revealed sentence. Additionally,
clicking on a sentence highlighted the premises that were used to infer the selected
statement (corresponding to the predecessors of a node in the tree representation).
Moreover, both interactive representations could be freely zoomed and panned.
The interactive proofs were provided by a prototypical web application for
explaining DL entailments called Evonne [
For each proof, there were three pages of questions. For the interactive conditions, the proofs on the first page were collapsed (to the root node or the first sentence), but on subsequent pages they started fully expanded since they had already been explored. Each question page contained a single question with 6 answer options (plus “none of these” and “I don’t know”). Questions were of the
form “Which of the following would be a correct replacement for the deduction ‘XYZ’ in the proof?” or “Which parts of the following summary/reformulation of the proof are incorrect?” The former questions require to choose a statement, which is not necessary equivalent to a given axiom but which aligns smoothly to the rest of the proof. In the end, a score was calculated based on the number of correct answers. Thus, the highest possible score for a user performance was 12. Further Information. As further information, demographic data were collected (age, gender, nationality), as well as experience with propositional logic, from 1 (“no knowledge at all/no experience”) to 5 (“expert/a lot of experience”). Participants also indicated how frequently they use propositional logic with 1 being “Never” and 5 being “All the time”. After each proof, the participants were asked to rate its comprehensibility on a scale from 1 (“not at all”) to 5 (“very much”). At the end of the survey, the participants were asked to additionally rank all the proofs they had seen according to their relative comprehensibility. Hypotheses. We stated two hypotheses concerning the preferences and performance differences between the proof representations.
Hypothesis 1 : It is easier to understand interactive proofs than static proofs. This will be shown by an increase in performance and by a higher comprehensibility rating for the interactive conditions.
Hypothesis 2 : The relative level of comprehensibility of a tree-shaped vs. textual proof depends on the cognitive abilities. This will be shown by a difference in performance and difficulty rating between the condition combinations and in the final comprehensibility ranking, in dependence of the ICAR16 scores. 5.2
Results
For the analyses, IBM SPSS Statistics (Version 26) predictive analytics software
for Windows [
A median split (mdn = .44) was carried out to divide the participants into those who achieved high scores in the ICAR16 and thus presumably also have higher cognitive abilities and those who scored lower.
For ICAR16 the mean was M = .46, while it was M = 2.36 for the proof performance. The group containing those participants who scored low in the ICAR16 achieved M = 1.9 across all proofs. In contrast, the group of participants with high ICAR16 scores showed an overall proof performance of M = 2.87. Performance and Comprehensibility Ratings. To compare the performance in the proof tasks and the subjective comprehensibility ratings after n Most interactive text interactive tree 15 15 static text 30 30 45 45 60 60 0 0 15 15 static tree 30 30 45 45 60 60 each proof, we ran a multivariate analysis of variance (MANOVA). All the assumptions were considered as tenable. We found no significant overall difference between the conditions across the two ICAR groups, Pillai’s Trace = .01, F (6, 1376) = 1.41, p = .206. Also when looking at the groups separately, we could not find any significant differences between the representations, neither in the low-ICAR group (Pillai’s Trace =1.03, F (6, 712) = 1.90, p = .078) nor in the group with high scores (Pillai’s Trace = .01, F (6, 656) = .53, p = .788). Thus, we could not detect differences in the comprehensibility ratings as well as the performance between the various representations in each cognitive ability group and across the two groups.
Ranking. To evaluate the ranking of the four representations (1 = most comprehensible, 4 = least comprehensible), we ran a Friedman’s test revealing a significant difference across both ICAR groups, χ2(3) = 17.16, p = .001, n = 173 (see Figure 3, light bars). Post-hoc pairwise comparisons were Bonferronicorrected and showed three significant comparisons. The interactive tree was significantly more often ranked higher than the interactive text (z = .40, p = .024, Cohen’s effect size r = .03) and also higher than static text (z = -.50, p = .002, Cohen’s effect size r = .04). The static tree representation was also ranked significantly higher than static text, z = .39, p = .032, Cohen’s effect size r = .03 (see Figure 3).
A Friedman’s test in the group with high ICAR performance showed a significant difference in the ranking of representations, χ2(3) = 12.73, p = .005, n = 83 (see Figure 3, dark bars). Bonferroni-corrected post-hoc pairwise comparisons revealed two significant comparisons. There is a significant difference between static tree and static text (z = .59, p = .019, Cohen’s effect size r = .06) with static tree being ranked higher than static text. Interactive tree was also preferred before static text, (z = -.54, p = .041, Cohen’s effect size r = .06).
The low-ICAR-performers showed no significant difference in the ranking of representations, χ2(3) = 6.70, p = .082, n = 90.
Neither of our two hypotheses could be conclusively confirmed. We did not find a significant advantage of using some proof representations over others, even when distinguishing groups by their levels of cognitive abilities. The analysis of the final ranking of the proof representations indicates a subjective preference of the conditions with tree-shaped proofs over their textual counterparts, but this did not seem to impact the objective performance measure nor the subjective ratings the participants gave after each proof. These preferences are largely driven by the group with higher ICAR performance (cf. Figure 3).
Limitations. According to the aims of our study, we did not pre-select
participants according to their experience with logic or field of studies. 55.5% of the
participants had no experience with propositional logic and 60.7% had never
worked with it. For many participants, even the ones with higher ICAR scores,
the proof tasks were very challenging, resulting in a mean score of M =2.36 out
of a total of 12. 15 people commented about the high difficulty level in the end,
and only 3 said the proofs were easy to understand. This resulted in many data
points being clustered on the lower end of the scale and differences being more
difficult to detect. For similar future studies, it is important to calibrate the
difficulty of the tasks well; they should be neither too hard nor too easy.
Conclusion. In addition to previous observations that shorter proofs are
better [
Acknowledgements This work was supported by the DFG grant 389792660 as part of TRR 248 (https://perspicuous-computing.science), and QuantLA, GRK 1763 (https://lat.inf.tu-dresden.de/quantla).