Although logical entailments are often considered “explainable”, experience with justifications in DLs has shown that explaining why a logical consequence holds still requires some effort. However, a full formal proof of a DL entailment may be considered too long-winded, and a textual representation of a proof may be preferred. It may also depend on the user's experience and individual preferences which representation of a proof constitutes a good explanation for them. Building on previous work on explaining DL consequences to users, we ran an experiment to compare 4 different forms of proofs: formal proofs and textual proofs, which are either very detailed or condensed. A multiple linear regression with contrast coding revealed that the participants rated short proofs as being easier than long proofs, independent of their representation. On the other hand, we could not verify any influence of prior experience with logic on how easy or difficult the different kinds of proofs were considered.
Explanations of automated decisions are currently an important topic of research.
However, apart from the popular discussion about how “explainable” different
AI methods are, the main task of explanations is understanding, i.e., that the
information transmitted is actually received by the human user, and hence is a
topic for social science research [
In the DL community, research on explanations first focused on proofs for
explaining entailments [
In an effort to understand which of these approaches are most promising
for improving explainability, our experiment continues in this line of research.
We investigated which representations of DL proofs are preferred by users (who
had some prior experience in logic). The main formats we used are full formal
proofs in a tree-shaped representation, e.g. based on consequence-based reasoning
procedures [
Our main finding is that shorter proofs were rated as being easier than ones that contained detailed reasoning chains. In particular, the long textual proof representation was often considered to be too long-winded and repetitive. However, the experience level of our participants did not seem to influence their preferences. Nevertheless, there clearly are differences in how different individuals were working with the different proof representations. 2
We assume a basic familiarity with DLs, in particular ALC [
O = { A v ∃r.>,
C u B v ⊥, A v ∀r.(B u C) }
Since the only requirement is soundness of each proof step, adjacent steps can be merged to obtain shorter proofs, e.g. for the proof in Fig. 1 we could merge the two steps:
A v ∃r.>
A v ∀r.(B u C)
A v ⊥
C u B v ⊥ This directly corresponds to the justification J = O. Thus, a justification can also be seen as a very short proof. However, it can be useful to highlight intermediate inference steps, for example to pinpoint the precise cause of an unintended entailment α: even if all axioms from the ontology seem reasonable to the user, at some point in the proof they will start to have unintuitive consequences, which can be used to track down the problem.
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 Fig. 1 could be the following: Since every A has an r-successor and every A has only r-successors that are B and C, every A has an r-successor that is B and C. Since every A has an r-successor that is B and C and there is no object which is C and B at the same time, there is no A. 3
We conducted an experiment where we assessed participants’ understanding of these different proof representations. The full details of the experiment are available online1. 3.1
Introduction and Goals. With the current experiment, we attempt to find which proof representation is most understandable, also considering experience with logic. The objective is to find a difference in the difficulty rating of longer or shorter proofs with either textual or a formal representation. 1 https://cloud.perspicuous-computing.science/s/Wmtmyp8JQNaF2AD Participants. 16 participants (four female) were assessed with a mean age of 23 (standard deviation = 1.71). Our international participants were recruited from undergraduate and graduate university students with basic knowledge of logic, which was required to understand the proofs. Participants were recruited via advertisements on mailing lists. Screening criteria were familiarity with first-order logic (e.g. through a lecture), a stable Internet connection, installing a video conference app with video access (on their mobile device or computer) and the permission to record their handwriting and voice during the experiment.
In Table 1, the descriptive statistics of the participants’ self-rated experience
with logic can be found.
Conditions and Design. We used two different conditions (factors) with two
levels each. One condition was the representational form of the proof, which
was either textual or formal. The other condition was the length of the proof,
which was either short or long. Thus, there were the four following condition
combinations: Long Text, Short Text, Long Formal, and Short Formal (see Table 2).
We used a 2 × 2 within-subjects design, which means that each participant saw
all four combinations.
Material. The proofs were chosen such that they represent an unintuitive
consequence, e.g. the unsatisfiability of a concept name, or that any amputation
of a finger is also an amputation of the whole hand [
In Figure 2, we depict a short formal and a short textual representation for one of the examples; the longer variants can be found in the appendix. Each proof was shown below a list of the involved ontology axioms on the left (Cell v Compound etc.), a textual translation of these axioms on the right (e.g. “Every cell is a compound.”), as well as a short statement of the entailment (“The ontology above implies that there is no cell culture.”).
Procedure and Tasks. Due to the Corona pandemic, we could not conduct the experiment in person as planned. Instead we used video conferences with Zoom2 and GoToMeeting3 to communicate with our participants.
The experiment was conducted in English. Every participant got an individual appointment. They were asked via e-mail whether they had a printer. If this was not the case, then the experiment sheets were send to them via post. If they had a printer, then they received the sheets as a PDF via e-mail with specific instructions on how to print them. One day before their appointment, the participants received an e-mail with a reminder and the link to the video conference meeting. To start the experiment, the participant was welcomed by the experimenter. The purpose and the procedure of the experiment was explained. They were then instructed to put the printed or sent papers in front of them and a link to the questionnaire and a participant number were sent to them. They went through the first six pages of the questionnaire asking them about their demographic data and experience with logic. To refresh participant’s memory and to make sure everyone started with at least the same basic knowledge about 2 https://zoom.us 3 https://www.gotomeeting.com
At u C v ⊥ At u Cmp v ⊥
Since every cell culture is a material object and every material object contains an atom, every cell culture contains an atom. From the facts that every cell culture contains an atom and that every cell culture contains a cell and contains only cells, it follows that every cell culture contains something which is both an atom and a cell. Every cell is a compound. Thus, any object which is an atom and a cell at the same time is also an atom and a compound. There is no object which is an atom and a compound at the same time. Therefore, there is no object which is both an atom and a cell.
Furthermore, since every cell culture contains something which is both an atom and a cell and there is no object which is both an atom and a cell, there is no cell culture. description logics, they were shown a 10-minute video with a crash course on description logics.
Afterwards, they were asked to arrange the camera setup in such a way that the papers in front of them and their hands were visible. Then the experimenter started recording the participant. To demonstrate both proof representations (textual and formal), a training phase was conducted. The participant saw a textual proof and a formal proof consecutively. The experimenter explained that they would see an ontology which implies an unintuitive statement. We used the think-aloud technique, in which the participant was asked to read the ontology and the proof carefully and simultaneously summarize the proof out loud. They were encouraged to take notes on the paper, point or draw connections between the axioms and the proof and to explain their line of reasoning. After each proof they were asked to answer the following two questions and to mark their answers on the sheets: “Which part of the proof was the most difficult to understand and why?” and “Which axioms in the ontology do you think are most responsible for the unintuitive consequence and why?” During the training phase the participant was allowed to ask questions. After the two training examples, the experiment phase began. One after another, they saw four ontologies, each of which implied an unintuitive statement. The instructions were the same as in the training phase except that no questions from the participant were answered by the experimenter. They were reminded to think aloud while working through the proofs. To minimize the impact of the order in which they saw the different proof representations, we used a Latin square, so every combination of the two conditions was seen first by one fourth of the participants (see Table 2).
After each proof, the participant filled out one question in the questionnaire about the perceived difficulty of the proof and received the same two questions as in the training phase. Subsequently, the final question in the questionnaire asked the participant to rank the proofs based on their comprehensibility (first rank = very easy, fourth rank = very difficult). It was possible to give several proofs the same rank. They were asked to comment on the ranking, what they liked and disliked about the proofs and afterwards also if they noticed any differences or similarities between the proofs. They were then told that there were two different representational forms of proofs and asked which they preferred and why.
Finally, the experimenter made sure that the participant submitted the questionnaire, stopped the recording and told them to fill in their participant number on each sheet, scan it or take a photo and send us the final sheets.
To assure a stable video conference connection, the experimenter’s video was off the whole time. To match the video and the questionnaire after the experiment, each participant was given the participant number, i.e., an individual code which they had to use in the questionnaire and on the sheets and under which we saved the video. Overall the experiment lasted around one and a half hours. After receiving all six pages (two for the training and four for the experiment phase), we sent them a code for an Amazon voucher worth 20 e.
To make sure the participants really understood the proofs a logic expert reviewed the video of each participant after each session. Due to the thinkaloud technique the expert was able to follow the participant’s thought and rated the video based on the participant’s understanding on a scale from 1 (no understanding) to 3 (complete understanding).
Independent and Dependent Variables. To assess participants’ logic experience we asked them how they would rate their experience with propositional, description, first order logic on a Likert-like rating scale from 1 (no knowledge) to 5 (expert). We further evaluated how they rated the difficulty of each proof on a Likert-like rating scale from 1 (very easy) to 5 (very difficult). To compare the different proof representations, we asked the participants to rank the proofs at the end of the experiment based on their comprehensibility.
Hypotheses. We stated three hypotheses concerning the participants’ self-rating of the difficulty of the proofs.
Hypothesis 1 : It is easier to understand a short, concise explanation than a longer version (in the same representation format). This will be shown by a lower difficulty rating for the short proofs than for the long proofs.
Hypothesis 2 : Users with less experience in logic can understand the longer text better than a short formal proof. This will be shown by a lower difficulty rating of the long textual proof.
Hypothesis 3 : Users with more experience in logic can understand a long formal proof better than a long text. This will be shown by a lower difficulty rating of the long formal proof. Problems and Limitations. Originally, this experiment was planned as inperson: all the technical equipment as well as a suitable room would have been arranged by us to minimize possible distractions. However, due to the Corona pandemic, we had to re-design the experiment to an online setting. As immediate drawbacks of a less controlled environment, we encountered i) technical problems with the video conference due to unstable Internet connections, ii) poor quality of video and audio recordings, e.g. a low-resolution phone camera, iii) compatibility issues with different browsers, e.g. for video playback, iv) concerns about privacy for receiving and storing the video and audio recordings of participants and their homes, v) various interruptions related to the environment, i.e., family members or domestic animals.
Additionally, there was a more conceptual problem concerning prior knowledge about the example domains. For example, if a participant sees a (for them) contradictory axiom in the ontology (e.g. “every vegetarian is a person,” because they would consider herbivorous animals to also be vegetarians; or “every artist is a professional,” since there exist also amateur artists),4 they would not focus anymore on the actual task of understanding why this ontology implies the goal axiom. 3.2
Quantitative Results. To compute the quantitative analyses IBM SPSS
Statistics (Version 26) predictive analytics software for Windows [
For Hypothesis 1, a multiple linear regression with contrast coding (K1, K2, K3) was conducted. K1 contrasted the textual representation against the formal one. K2 contrasted the short vs. long proofs and K3 the interaction between the two general conditions. The three contrasts explained 14.2% of variance in the rating after each proof, R2 = .14, F(3, 60) = 3.30, p < .05. Only K2 was found to be a significant predictor in the linear regression, β = −.29, t(60) = −2.42, p < .05. This means that the participants rated the shorter proofs as being easier than the longer ones, which was independent of the presentation format. Thus, Hypothesis 1 could be supported by our data.
For Hypotheses 2 and 3, we want to assess if the strength of the relationship between the independent variables (condition combinations) and the dependent variable (rating after each proof) changes with the third variable (experience), i.e., whether there is an interaction between the conditions and the experience. We computed moderator analyses with the two condition combinations as a predictor, the experience as a moderator variable and the rating after each proof as the criterion. To put the conditions into the moderator analysis for Hypothesis 2, the Long Text was coded with +1 and Short Formal with -1 (and similarly for Hypothesis 3 with Long Text and Long Formal). For each self-rated measure of experience (propositional logic, first-order logic, description logic), one moderation analysis was computed. 4 These occurred in the training examples.
For Hypothesis 2, the moderation analyses for the self-rated experience with propositional and first-order logic revealed a significant model, R2 = .25, F(3, 28) = 3.07, p < .05 and R2 = .31, F(3, 28) = 4.21, p < .05, respectively, but only the two main effects were shown to be significant and not the interaction (see Table 3). Thus, there was no significant moderation. The main effect of the condition combinations showed that the Short Formal representation was rated as being easier than the Long Text. The main effect of experience means that, the more experience the participants had, the easier they rated the proof. However, the two main effects were independent from each other and showed no interaction, which means that neither the experience with propositional logic nor the experience with first-order logic influenced the relationship between the condition and the rating. For the self-rated experience with description logic, the moderation model was not found to be significant. Thus, Hypothesis 2 could not be supported by our data. Experience with logic did not make a difference on the understanding of the different proof representations.
For Hypothesis 3, from the three moderation models, only the model with the self-rated experience with propositional logic turned out to be significant, R2 = .25, F(3, 28) = 3.07, p < .05. Only the main effect of experience was significant here, β = −.43, t(28) = −2.10, p < .05. Thus, also Hypothesis 3 could not be supported by our data. Experience with logic did not make a difference on the understanding of the different long conditions.
Additionally to the three hypotheses, we used Friedman’s ANOVA for comparing the comprehensibility ranking of the proof representations at the end of the experiment (first rank = very easy, fourth rank = very difficult). It revealed a significant difference in the ranking of the condition combinations, χ2(3) = 15.29, p < .01 with a moderate effect size (Kendall’s W = .32). For the post-hoc pairwise comparisons Bonferroni correction was used which resulted in a p-threshold of 0.008, resulting in only two significant comparisons.
The participants’ ranking of condition combinations is shown in Figure 3. The combination Short Text was preferred over Long Text, Z = 1.53, p < .008. The median ranking for Short Text and Long Text was 2 and 3.5, respectively. Additionally, Short Formal was preferred over Long Text, Z = 1.50, p < .008. 8 ts7 n6 a p ic5 itr fp4 a o r3 e b m2 u N 1 0 8 ts7 itrcapn6 i5 a fsep4 o r3 b 2 m u N 1 0 8 ts7 n6 a p ic5 itr fp4 a o r3 e b m2 u N 1 0 8 ts7 itrcapn6 i5 a fsep4 o r3 b 2 m u N 1 0 1.Rank 2.Rank 3.Rank
Chosen rank Long Formal 4.Rank 1.Rank 2.Rank 3.Rank
4.Rank
Chosen rank Short Formal Short Formal had the lowest median ranking with 1.50. Both comparisons showed moderate effect sizes, r = 0.38 for both. Median ranking for Long Formal was 2.
Only one participant chose Long Text on the first rank. Their statement can be found in the next subsection. However, nobody put Long Text on the second rank, but 15 chose the third or fourth rank for it. Thus, most participants ranked it as (very) difficult. Short Text was never assigned the fourth rank, but by 13 participants it was considered very easy or easy.
Long Text Short Text 1.Rank 2.Rank 3.Rank
Chosen rank 4.Rank 1.Rank 2.Rank 3.Rank
4.Rank Chosen rank Qualitative Results. For the qualitative evaluation, we transcribed the audio recordings into text and arranged the texts according to the condition or condition combination. Then, we compared the participants’ statements on each condition based on similarity and differences according to the hypotheses and grouped them contentwise.
In general, the participants’ statements also supported the view that the formal proofs were preferred over the textual proofs. Participants described the formal proofs as “easier to understand” and also as “clearer”. One participant mentioned that for them it was “easier to find certain parts” of the proof. Another one that that their “orientation is better” within the proof, in order to go through it step-by-step, and that it is “easy to follow the proof”. The textual proofs were often characterized as inconvenient, “less understandable” or “hard to understand” or even “annoying”.
On the other hand, one participant stated that “for short proofs text is ok.” Only one participant said that they “preferred a proof explained through words rather than through a schema.” The participant commented on it as follows: “Texts add more redundancy and this redundancy helps with connecting. My intuition for language can spot inconsistencies better. So, if a domain is abstract or unknown and a proof is complex (like in Mathematics) and requires to put together several pieces and arguing about them, wording might help a lot.”
Many participants were struggling with inferences involving both ∀- and
∃quantifiers in formal proofs. However, its textual equivalent or a second encounter
of ∀+∃ were perceived much better (this combination appeared already in the
training examples). Several participants mentioned that a graphical presentation
is better when there are parallel threads: “I could clearly see what and where
they come from. And then forget about what I just learned so I could go to
another part. And once I again need this part, I know exactly where it came
from later.” Also, some participants found it very difficult to deal with longer
domain-specific terms, since it requires more time to understand and to keep
track of them. These opinions confirm the motivation behind [
Short proofs were rated as being easier than long proofs, independent of the
presentation format. Thus, future experiments and theoretical approaches should
focus on shortening proofs. With our data, Hypotheses 2 and 3 could not be
supported. However, the rankings and discussions clearly showed individual user
preferences between formal and textual representations. For further research in
this direction, the questions from [
On the other hand, the ultimate goal is to explain logical conclusions to
domain experts who are not familiar with logic. Here, an interesting direction
of study is to generate (concise) textual explanations [
From a procedural point of view, it would be preferable to use a
betweensubjects design (different people test each condition) instead of within-subjects
(when the same person tests all the conditions), to minimize learning effects, which
however requires more participants. Of course we would also like to compare other
proof representations, e.g. pure justifications, linear vs. non-linear formats, mixed
formal/textual presentations as mentioned above, incorporating annotations such
as axiom numbering or coloring, and most importantly interactive approaches
such as the proof plugin for the Protégé ontology editor [
As was demonstrated by the participants’ different opinions and preferences
about proof representations, it makes sense to incorporate the user as an active
element in the design of a suitable presentation. User modeling [
Another take-away message we learned from our experiment is that preparing such experiments to take place online from the beginning also has an upside since then they are more resilient against unforeseen events.
Acknowledgements This work was partially supported by DFG grant 389792660 as part of TRR 248 (https://perspicuous-computing.science). We are also grateful to our colleagues who forwarded the advertisement for the experiment to their students, and of course to the participants.
On the following two pages we depict the long versions of the proofs in Figure 2: Every cell culture contains a cell and contains only cells. Thus, every cell culture contains only cells. Since every cell culture is a material object and every material object contains an atom, every cell culture contains an atom. From the facts that every cell culture contains an atom and that every cell culture contains only cells, it follows that every cell culture contains something which is both an atom and a cell. Trivially, every object which is both an atom and a cell is an atom and a cell. Thus, every object which is both an atom and a cell is a cell. Every cell is a compound. Therefore, every object which is both an atom and a cell is a compound. Trivially, every object which is both an atom and a cell is an atom and a cell. Thus, every object which is both an atom and a cell is an atom. From the facts that every object which is both an atom and a cell is an atom and that every object which is both an atom and a cell is a compound, it follows that every object which is both an atom and a cell is both an atom and a compound. There is no object which is both a compound and an atom at the same time. Therefore, there is no object which is both an atom and a cell.
v oC lle lle llv Cu C e
l C m ule
u nd to vC ll e u C m
m uto o
t m A A o t
v A ll e
C ll u e m C o
m t uo A
t m A o t A lv
l ve ll C e u C
m uo
t m A o t A ⊥ M m o v t