# Position-Aware Parameter Efficient Fine-Tuning Approach for Reducing
Positional Bias in LLMs

Zheng Zhang†, Fan Yang∗, Ziyan Jiang∗, Zheng Chen∗, Zhengyang Zhao∗, Chengyuan
Ma∗, Liang Zhao†, Yang Liu Amazon, views here are the authors’s and not those
of Amazon. †Emory University<EMAIL_ADDRESS>.

###### Abstract

Recent advances in large language models (LLMs) have enhanced their ability to
process long input contexts. This development is particularly crucial for
tasks that involve retrieving knowledge from an external datastore, which can
result in long inputs. However, recent studies show a positional bias in LLMs,
demonstrating varying performance depending on the location of useful
information within the input sequence. In this study, we conduct extensive
experiments to investigate the root causes of positional bias. Our findings
indicate that the primary contributor to LLM positional bias stems from the
inherent positional preferences of different models. We demonstrate that
merely employing prompt-based solutions is inadequate for overcoming the
positional preferences. To address this positional bias issue of a pre-trained
LLM, we developed a Position-Aware Parameter Efficient Fine-Tuning (PAPEFT)
approach which is composed of a data augmentation technique and a parameter
efficient adapter, enhancing a uniform attention distribution across the input
context. Our experiments demonstrate that the proposed approach effectively
reduces positional bias, improving LLMs’ effectiveness in handling long
context sequences for various tasks that require externally retrieved
knowledge.

##  1 Introduction

Recent advancements in developing Large Language Models (LLMs) significantly
enhance the proficiency of language models in harnessing and utilizing
extensive input context. This advancement plays a crucial role in improving
the performance of applications in areas like recommendation (Naumov et al.,
2019) and question answering (Roberts et al., 2020; Yasunaga et al., 2021).
Especially, LLMs have shown remarkable advancements in retrieval-augmented
generation tasks, significantly enhancing text information retrieval (Guu et
al., 2020a; Borgeaud et al., 2022), exhibiting strong performance in sifting
through vast amounts of data to find relevant information.

Figure 1: Illustration of Positional Preferences in LLMs: The figure
demonstrates how the Vicuna-13b-v1.5-16k model’s performance on a
recommendation task changes with the correct answer’s position in the input
context window. Given a list of potential candidates, we intentionally
position the ground truth candidate at various locations within the list to
assess how the predicted position distribution by the LLM shifts. From the
figure we can observe the probability peaks near the correct position of
relevant information, demonstrating a degree of capacity for identifying
pertinent information. There is a notable preference for the first position,
indicating significant positional preference.

Although LLMs have made significant progress in processing retrieval-based
tasks, their application encounters a key challenge due to a positional bias
issue. In many retrieval scenarios, a list of potential candidates is
presented. The order of these candidates is often interchangeable and not
intended to influence the outcome. However, the inherent input structure of
LLMs necessitates flattening this list, thereby imposing an artificial
“ordering” over the candidates. Recent studies (Liu et al., 2023a; Ravaut et
al., 2023) have revealed that the performance of LLMs is notably affected by
the position of relevant information within the input context, especially in
cases of extended input lengths. Specifically, previous study (Liu et al.,
2023a) claimed that LLMs often perform better when relevant information is at
the beginning or end of a sequence, while their performance decreases when key
details are in the middle. The uneven performance across text segments is
described as “lost-in-the-middle” phenomenon.

While preliminary research (Liu et al., 2023a; Ravaut et al., 2023; Zheng et
al., 2023) has highlighted this positional bias as a significant limitation in
LLMs, there is a notable gap in understanding the underlying causes of this
issue. In our study, we have conducted comprehensive experiments to assess how
the position of genuinely relevant information influences the probability
distribution of the retrieved information’s location. Our findings indicate
that rather than the “lost-in-the-middle” phenomenon, it is more accurate to
state that each LLM exhibits a unique “positional preference” within the
context window. For example, as shown in Figure 1, the Vicuna-13b-v1.5-16k
model exhibits a clear “positional preference” for selecting the initial
position within the input context as the predicted position, regardless of the
actual location of the relevant information.

Moreover, a general while efficient solution to mitigate this positional bias
issue remains under-explored. Addressing this challenge is crucial for the
advancement and accuracy of LLM applications, especially in contexts where the
order of information should not affect the understanding ability of LLMs.
Initially, we execute a series of experiments demonstrating that merely
employing prompt-based strategies, such as presenting few-shot examples or
instructing LLMs to organize candidates hierarchically, can not overcome the
issue. To counter this, we introduce a data augmentation strategy that
involves permuting the position order within documents to mitigate the
positional preference issue inherent in the source data. Additionally, we
propose a parameter-efficient fine-tuning technique named Position-Aware
Parameter Efficient Fine-Tuning (PAPEFT), designed to make pre-trained LLMs
aware of and adjust for positional bias by explicitly considering document
positions within the context window. Experimental results across various
applications, including recommendation and link prediction, show an over 56%
reduction in performance variance across different positions of relevant
information, demonstrating a more consistent and reliable understanding
abilities of proposed method within the input context window.

The remainder of this work is organized as follows: We begin by discussing
existing relevant studies in the Section 2. This is followed by a formal
problem definition and an introduction to the datasets in the Section 3.
Subsequently, in the Section 4, we investigate the underlying cause of LLMs’
positional bias through a series of empirical studies and shows that simply
adopting prompt-based solution can not address the bias. In Section 5, we
delve into the motivation behind our approach and discuss the specific
techniques employed. We conclude with comprehensive experimental results,
assessing aspects such as effectiveness and efficiency in Section 6.

##  2 Related Works

Positional Bias in LLMs. While LLMs have gained prominence, the exploration of
positional bias within these models is still in its infancy and has only
recently started to attract attention. The body of existing research, though
growing, remains limited. A handful of early studies have started to shed
light on the implications of positional bias in LLMs. For instance, Liu et al.
(Liu et al., 2023a) provided benchmarks indicating that positional bias is a
widespread concern, particularly in question answering and key-value pair
retrieval tasks. Ravaut et al. (Ravaut et al., 2023) expanded on this by
exploring positional bias in text summarization tasks. Zheng et al. (Zheng et
al., 2023) made an early attempt to correct this bias by adjusting LLM outputs
based on a prior probability reflecting the model’s option preferences.
Nevertheless, their approach is confined to multiple-choice contexts and lacks
generalizability for broader applications. This limitation stems from the
challenges in calculating the prior probability and the significant increase
in computational demands that such a method entails.

Retrieval-Augmented Generation. Retrieval-Augmented Generation combines
generative capabilities of language models with external knowledge retrieval,
enhancing accuracy and relevance in responses. Early foundational work in
transformers set the stage for RAG systems (Vaswani et al., 2017). Subsequent
developments like R-Transformer (Lewis et al., 2020) and RAG models (Guu et
al., 2020b) integrated retrieval mechanisms with large language models,
improving performance in knowledge-intensive tasks. Recent advancements (Liu
et al., 2023b; Chowdhery et al., 2023) focus on optimizing retrieval
efficiency and accuracy, addressing challenges in coherence, factual
correctness, and bias management.

Parameter Efficient Fine-Tuning for LLMs. Parameter-efficient fine-tuning has
emerged as a crucial technique for enhancing model performance without the
substantial computational and memory costs associated with full model
training. This approach, as discussed in recent literature, involves adjusting
a small subset of the model’s parameters while keeping the majority of the
model’s weights fixed, thereby enabling the model to adapt to new tasks or
data with minimal resource expenditure. Techniques such as adapter layers
(Houlsby et al., 2019; Dettmers et al., 2024), prompt tuning (Li & Liang,
2021), and sparse updates (Liu et al., 2023c) have been highlighted as
effective means for achieving this efficiency. Such methods not only conserve
resources but also mitigate the risk of overfitting by limiting the degree of
freedom during the training process. Existing research primarily concentrates
on enhancing the efficiency of the fine-tuning stage for LLMs, whereas our
work is distinctly focused on debiasing a pre-trained LLM using an efficient
fine-tuning module.

##  3 Preliminaries

##### Problem Formulation.

This paper focuses on the exploration and analysis of tasks which leverage
Retrieval-Augmented Generation (RAG) framework in the context of Large
Language Models (LLMs). The central scenario of our study is an input context
with a set of $K$ retrieved documents. Among these documents, only one
contains the correct or relevant information. The input context to LLM is a
composite of all $K$ potential documents alongside additional textual cues.
Formally, the input context is structured as
$[\mathbf{P}_{s},\mathbf{X}_{1},\mathbf{X}_{2},\dots,\mathbf{X}_{K}]$, where
$\mathbf{P}_{s}$ represents the additional textual prompts that describe the
task for LLMs. The desired outcome from the LLM in response to this input
should correctly identify and select the correct relevant document from the
set of $K$ candidates. Formally, if the correct relevant document is denoted
as $\hat{\mathbf{X}}_{c}$, where $c$ ranges from 1 to $K$, the likelihood that
the LLM identifies the $i$-th position as the true relevant location is
expressed as $P(\mathbf{X}_{i}|\hat{\mathbf{X}}_{c})$. The fluctuation in the
accuracy of predictions for the correct positions, as these positions vary, is
measured by the standard deviation divided by the mean of the set of
probabilities for all correctly predicted positions. This set is represented
as $\\{P(\mathbf{X}_{c}|\hat{\mathbf{X}}_{c})|c\in[1,K]\\}$, where
$P(\mathbf{X}_{c}|\hat{\mathbf{X}}_{c})$ denotes the probability of the
correct position $\mathbf{X}_{c}$ given the predicted position
$\hat{\mathbf{X}}_{c}$, for each position $c$ within the range of 1 to $K$.

##### Datasets.

Our research investigates positional bias in Language Learning Models (LLMs)
across Recommendation (REC), and Link Prediction (LP) domains. We employed
specialized datasets—Amazon M2 (Jin et al., 2023) for REC, and Arxiv (Wang et
al., 2020) for LP—to evaluate LLMs’ ability to identify key information in
varying contextual placements. The critical information’s position within each
dataset was systematically varied to test LLM adaptability and accuracy with
shifting contexts. The details of used datasets are as follows:

Recommendation (REC): We utilized the Amazon M2 dataset (Jin et al., 2023),
which is a rich source of user-product interaction data. Each session within
the dataset consists of a sequence of products previously purchased by a user,
and their next following purchase. The dataset provides extensive metadata for
each product, including descriptions and brand information. We present a set
of $K$ possible products per session, among which only one is the actual
product that the user purchased and the others are negative samples. We alter
the position of “ground truth” product within the list to examine the LLMs’
proficiency in pinpointing the relevant information depending on its
contextual placement.

Link-Prediction (LP): We leverage the comprehensive citation network benchmark
dataset Arxiv (Kwiatkowski et al., 2019). This dataset describes a large
citation graph where each node is a research paper and the connections between
nodes indicate their citation behavior. To assess the ability of LLMs against
varied positions of relevant information, we include an evaluation of their
ability to accurately identify and present correct cited paper. We manipulate
the location of the ground truth cited paper among a list of randomly sampled
papers. Specifically, for each given paper, we present a list of papers while
only one of them is truly cited by the given one. Then we vary the position of
the ‘ground truth’ paper to evaluate how the position of the paper impacts the
LLMs’ prediction ability.

##### Choice of LLMs.

To assess the robustness of LLMs against positional bias in scenarios
involving extensive context sizes, we have compiled a list of widely
recognized open-source LLMs specifically tailored for managing long input
contexts. This compilation features models frequently employed in academic
research, such as Vicuna-13b-v1.5-16k (Chiang et al., 2023) and
Longchat-13b-16k (Li et al., 2023). These selections enable us to examine a
model’s efficacy in processing extended dialogues and its capability to handle
positional information within conversational settings.

##### Evaluation Metrics.

We adopt “accuracy” to evaluate the generated answer quality by LLMs, judging
whether the correct relevant document is selected to generate the final
answer. Additionally, we employ “fluctuation” as a metric to assess the
variance in performance across different positions, which is defined as the
ratio of the standard deviation to the average value.

##  4 Empirical Studies

Figure 2: The Longchat-13b-16k model’s performance on a recommendation task
changes with the correct answer’s position in the input context window.
Comparing with the Vicuna-13b-v1.5-16k model’s trend in Figure 1, we can
observe that these two models have different preferred positions. The
Longchat-13b-16k model has preferred location around position eleven, while
Vicuna-13b-v1.5-16k prefers the first position.

###  4.1 Investigating the Underlying Causes of Positional Bias in LLMs

To uncover the reasons underlying positional bias in LLMs, we initiate our
investigation by conducting empirical experiments. These experiments are
designed to evaluate how the placement of the ground truth answer influences
the probability distribution of the positions predicted by LLMs. In Figure 1
and Figure 2, we illustrate the predicted probability distributions for all
potential positions across various ground truth locations, using the
Vicuna-13b-v1.5-16k and Longchat-13b-16k models, respectively. From these
figures, it is evident that both models exhibit a “preferred position” for the
predicted answer, regardless of the actual ground truth positions. Notably,
the models demonstrate distinct positional preferences, where Longchat-13b-16k
shows a preference for the eleventh position and Vicuna-13b-v1.5-16k tends to
favor the first position. Therefore, instead of the “lost-in-the-middle”
phenomenon suggested by earlier research (Liu et al., 2023a), we arguably
propose that the issue of positional bias is primarily due to the model’s
“preferred position”.

###  4.2 Prompt-Engineering Based Method Performance

Model # of Few-shot 1 5 9 13 17 20 Longchat-13b-16k 0 0.426 0.125 0.105 0.142
0.127 0.261 Longchat-13b-16k 1 0.620 0.223 0.167 0.161 0.150 0.338
Longchat-13b-16k 3 0.594 0.169 0.130 0.142 0.123 0.269 Longchat-13b-16k 5
0.669 0.175 0.114 0.108 0.100 0.228 Vicuna-13b-v1.5-16k 0 0.931 0.207 0.076
0.057 0.019 0.069 Vicuna-13b-v1.5-16k 1 0.832 0.014 0.005 0.003 0.000 0.001
Vicuna-13b-v1.5-16k 3 0.872 0.002 0.001 0.002 0.005 0.011 Vicuna-13b-v1.5-16k
5 0.903 0.003 0.001 0.003 0.002 0.004

Table 1: Few-shot performance on recommendation task with 1, 3, and 5 few-shot
examples. Here “0” few-shot examples denotes the performance of zero-shot
situation.

Considering the identified “preferred position” bias, a natural question
arises: can we devise an effective method to mitigate this bias issue? With
recent advancements demonstrating that LLMs possess a significant in-context
learning capability (Min et al., 2021), enabling them to learn and reason
based on the text prompts provided, it naturally leads to the question whether
specially crafted prompts could be employed to address or alleviate the impact
of positional bias. To answer this question, we have crafted a variety of
input prompts, aiming to provide insights on addressing the positional bias
issue. The description of prompts is as below and the example of prompts can
be found in Appendix Table 7.

(1) Zero-shot learning: LLMs are tasked with generating responses without any
prior examples. This setting is essential to observe the natural inclinations
of LLMs and their raw handling of positional information, providing a baseline
for their performance.

(2) Few-shot learning: We provide the LLMs with a handful of selected examples
within the prompt. The goal is to determine if a limited number of
illustrative examples can provide sufficient knowledge to the models, thereby
guiding them towards more accurate interpretations of information, regardless
of its positional context.

(3) Hierarchical inference: A potential cause of the positional bias issue
could be attributed to the extensive context size and the large number of
possible choices. To tackle this challenge, we suggest employing a prompt that
encourages the LLM to make prediction in a bottom-up manner. Initially, the
model is instructed to categorize all candidates into a few smaller groups,
followed by identifying the most likely answer within each group.
Subsequently, from the chosen answers for each group, the model is tasked with
making the final prediction. Thus, the overall prediction process is
structured in a hierarchical fashion, aiming to mitigate the effects of
positional bias.

####  4.2.1 Few-shot Learning

In Table 1, we present the impact of utilizing a varying number of few-shot
examples on the performance in a recommendation task. The findings indicate
that while few-shot examples can generally enhance the model’s accuracy, they
do not mitigate the issue of positional bias along the sequence. The
fluctuation in performance across different positions continues to exhibit
high variance, even as the quantity of few-shot examples is increased.

####  4.2.2 Hierarchical Inference

The outcomes of employing hierarchical inference are detailed in Table 2. It
is observed that this approach not only fails to mitigate the positional bias
issue but also leads to a notable decrease in performance. A possible
explanation for this result could be that LLMs might not effectively process
the complex instructions presented within a single input prompt.

In conclusion, the empirical studies showcased here demonstrate that prompt-
based solutions alone are insufficient to resolve the positional bias issue.
Given the observation of a distinct “preferred location” for each pre-trained
LLM, it is arguably possible that positional biases are inherently introduced
during the pre-training phase or the instruction fine-tuning phase through the
training data.

Model Hierarchical 1 5 9 13 17 20 Longchat-13b-16k No 0.426 0.125 0.105 0.142
0.127 0.261 Longchat-13b-16k Yes 0.131 0.032 0.022 0.028 0.069 0.149
Vicuna-13b-v1.5-16k No 0.931 0.207 0.076 0.057 0.019 0.069 Vicuna-13b-v1.5-16k
Yes 0.179 0.012 0.041 0.280 0.212 0.268 GPT-3.5-turbo-16k No 0.440 0.507 0.495
0.354 0.315 0.288 GPT-3.5-turbo-16k Yes 0.245 0.147 0.133 0.092 0.095 0.138

Table 2: Hierarchical inference performance on recommendation task with
varying positions.

##  5 Methodology

In order to design an effective and efficient method for mitigating the
inherent positional bias of pre-trained LLMs, we introduce a strategy named
Position Aware Parameter Efficient Fine Tuning (PAPEFT). It combines a
position-aware parameter efficient adapter module with data augmentation
techniques. Specifically, to remove the model’s intrinsic location preference
bias, which is typically introduced by the pre-training phase data, we employ
a data augmentation technique (Section 5.1) that involves random permutation
of the ordering in candidate lists. This requires LLMs to distribute their
attention uniformly across different positions within the input context.
Furthermore, to efficiently debias the original parameters of LLMs, we
introduce an new adapter module that explicitly incorporates the positional
context of each candidate as learnable soft prompts (Section 5.2). This
integration aims to adjust the LLM’s attention to various positions more
equitably without modifying the original pre-trained parameters.

###  5.1 Ordering Permutation with Data Augmentation

As discussed in Section 4, existing pre-trained LLMs exhibit a specific
location preference over the input contextual length. This tendency results in
an uneven distribution of attention across the entire context, and thus leads
to fluctuating performance. A potential explanation for the distinct location
preferences observed in various LLMs could stem from positional biases present
in the original pre-training data, e.g. key information is often placed at the
start of text.

In order to provide an appropriate way to mitigate this issue in the data
perspective, we adopt a strategic data augmentation process designed to evenly
distribute LLM attention across various positions within the input context.
Specifically, this approach creates multiple permutations for each set of
potential document candidates within a given input context. These permutations
serve as augmented fine-tuning datasets. Mathematically, given a list of
candidates
$[\mathbf{P}_{s},\mathbf{X}_{1},\mathbf{X}_{2},\dots,\mathbf{X}_{K}]$, we
create multiple permutations of this list, ensuring that each candidate
$\mathbf{X}_{i}$ occupies every possible position across different versions.
This generates a series of new training instances
$[\mathbf{P}_{s},\mathbf{X}_{\pi(1)},\mathbf{X}_{\pi(2)},\dots,\mathbf{X}_{\pi(K)}]$,
where $\pi$ denotes a permutation function that rearranges the indices
$1,2,\dots,K$.

Figure 3: The overall framework of location encoding soft prompt adapter
module. The relative locations of potential documents are initially computed
and subsequently fed into a soft prompt adapter. The soft location tokens are
concatenated with textual tokens to form a combined input for the attention
layers in LLMs.

###  5.2 Explicitly Incorporating Positions Location through Location Encoding
Adapter

Given the generated augmented data, a key question is the design of the fine-
tuning module for the pre-trained LLM. Directly optimizing the LLM parameters
is a straightforward approach but proves inefficient due to the vast number of
parameters involved. Although various parameter-efficient fine-tuning methods
like LoRA (Hu et al., 2021), QLoRA (Dettmers et al., 2023), and prompt tuning
(Lester et al., 2021) are available, they do not adequately consider the
location of documents within the input context, thus these approaches are not
fully optimized in addressing positional bias.

In order to let LLMs be aware of the position of all potential documents for a
debias-oriented optimization process, we further propose a novel adapter
module to explicitly incorporate the relative locations of documents as
additional input prompts, which is named as Location Encoding (LE) adapter.
Specifically, each document’s relative location is computed and included in
the input prompts. Then a trainable adapter module transforms the dimensions
of these locational prompts into the token embedding space, aligning the
semantic meaning of the transformed locational tokens with the textual tokens.

Mathematically, as illustrated in Figure 3, the process begins by computing
the relative locations of all potential documents within the context length,
denoted as $\mathbf{S}\in\mathbb{R}^{K}$. A learnable adapter module
$f_{\theta}$, where $\theta$ denotes the learnable parameters, is then applied
to these locational prompts. This module aligns the semantic essence of these
spatial tokens with the trained textual token space of the LLM. The formal
transformation process is represented as follows:

$f_{\theta}(\mathbf{S}_{i})=\mathbf{A}_{i},\quad\forall
i\in[1,K],\quad\mathbf{A}_{i}\in\mathbb{R}^{d},$ (1)

where $d$ represents the dimension of the token embedding space utilized by
the LLM.

Upon completion of this mapping process, the adapter model generates
additional transformed tokens $\mathbf{A}$. These tokens are subsequently
concatenated with the original textual tokens, forming a new, enriched input
sequence
$I=[\mathbf{A},\mathbf{P}_{s},\mathbf{X}_{1},\mathbf{X}_{2},\dots,\mathbf{X}_{K}]$
for the LLMs. This concatenated sequence encourages that each document is
presented and guided by a contextual positional cue, thereby providing the LLM
with a dual awareness of content and contextual positioning.

##  6 Experiments

Task Base Model Fine Tune Strategy 1 5 9 13 17 20 Mean Fluctuation (%) REC
Longchat-13b-16k Original 0.329 0.249 0.211 0.205 0.171 0.341 0.251 27.78
PAPEFT-PT 0.832 0.714 0.708 0.723 0.715 0.736 0.733 6.38 PAPEFT-LE 0.854 0.731
0.748 0.745 0.767 0.752 0.766 5.82 PAPEFT-LoRA 0.864 0.816 0.808 0.823 0.815
0.836 0.827 2.47 Vicuna-13b-v1.5-16k Original 0.855 0.083 0.211 0.205 0.171
0.341 0.311 89.76 PAPEFT-PT 0.881 0.698 0.701 0.745 0.767 0.741 0.756 8.88
PAPEFT-LE 0.883 0.746 0.738 0.798 0.807 0.765 0.790 6.77 PAPEFT-LoRA 0.855
0.836 0.818 0.833 0.825 0.855 0.837 1.83 LP Longchat-13b-16k Original 0.016
0.112 0.147 0.168 0.051 0.022 0.086 75.97 PAPEFT-PT 0.698 0.708 0.742 0.760
0.718 0.742 0.728 3.26 PAPEFT-LE 0.755 0.754 0.763 0.781 0.773 0.763 0.765
1.37 PAPEFT-LoRA 0.829 0.810 0.815 0.809 0.816 0.825 0.817 0.99
Vicuna-13b-v1.5-16k Original 0.257 0.208 0.119 0.166 0.096 0.104 0.158 40.58
PAPEFT-PT 0.757 0.721 0.709 0.741 0.761 0.771 0.743 3.27 PAPEFT-LE 0.744 0.774
0.773 0.769 0.760 0.783 0.767 1.77 PAPEFT-LoRA 0.824 0.824 0.823 0.841 0.843
0.853 0.835 1.52

Table 3: Accuracy score and performance fluctuation with varying position of
relevant document. We present the results of the original model, and the
proposed PAPEFT framework equiped with three different parameter efficient
fine-tuning techniques (PT for prompt tuning, LE for location encoding, and
LoRA) on recommendation (REC) and link prediction (LP) tasks, with
Longchat-13b-16k and Vicuna-13b-v1.5-16k as the base model.

###  6.1 Experimental Settings

Our introduced PAPEFT framework is composed of two main components: the data
ordering permutation augmentation technique, and the parameter-efficient fine-
tuning (PEFT) module. For an in-depth evaluation of the PEFT module, we have
chosen three different choices. This choice is designed to cover a broad
spectrum of tunable parameters and to evaluate the effectiveness of our
specially designed location encoding soft prompt adapter. To differentiate
between these configurations, we designate the variant equipped with the
location encoding soft prompt adapter as PAPEFT-LE. The variant employing a
straightforward prompt tuning adapter (Lester et al., 2021), which shares the
same architectural framework as the location encoding soft prompt adapter but
removes the input of relative document locations, is termed PAPEFT-PT. Lastly,
the variant incorporating a LoRA (Hu et al., 2021) adapter is referred to as
PAPEFT-LoRA. Table 4 displays the tunable parameters of the three adapters.

##### Augmented Datasets Details.

During data augmentation phase, we generated five permutations of each
document set for REC, and three for LP tasks according to the size of
datasets. We select Longchat-13b-16k (Li et al., 2023) and Vicuna-13b-v1.5-16k
(Chiang et al., 2023) as the base model for their proficiency in handling long
context windows. Statistics information about the datasets size can be found
in Appendix A Table 5 and Table 6.

##### Implementation Details.

For efficient fine-tuning, we enabled 4-bit loading of model. The training was
conducted with a sequence length of 16,384 tokens, padding enabled to match
this length. The soft prompt adapter is featured with a two-layer MLP encoder
of 1024 hidden size. For optimization, we employed the paged AdamW 32-bit
optimizer with a cosine learning rate scheduler, setting the initial learning
rate at $2e^{-4}$. The model underwent four epochs of training with mixed
precision of BFloat16 and Float32. Flash attention 2 (Dao et al., 2022) is
used for further acceleration. For LoRA adapter, we use $r=16$ as the setting.
We use standard next-token prediction as our training objective. All
experiments were done using eight NVIDIA A100-40GB GPUs. Code can be found in
https://anonymous.4open.science/r/llm_long_context-E9CF.

###  6.2 Effectiveness Results

Our key findings on accuracy results of REC and LP tasks, as shown in Figure
3, our proposed PAPEFT framework and original models are summarized as
follows:

Positional Bias in Original Models: The performance of both Longchat-13b-16k
and Vicuna-13b-v1.5-16k models demonstrated significantly noticeable
fluctuations, with each model exhibiting distinct patterns of variability
across different tasks. These fluctuations are indicative of prevalent
positional bias within the original models.

Reduction in Positional Fluctuations: The PAPEFT framework achieves a
substantial reduction in positional bias, with an average decrease in
performance variance of 54.19% for recommendation tasks and 58.72% for link
prediction tasks. This improvement signifies that the integrated approach of
data augmentation and position-aware fine tuning effectively guides the LLM to
treat all candidates within the input context more evenly, thus mitigating
positional bias.

Enhancement in Model Performance: The PAPEFT framework yielded substantial
improvements in model performance with an average increase of 57.3% for the
recommendation task and 64.4% for the link prediction task compared to the
original model. These improvements demonstrate PAPEFT’s ability to not only
reduce performance bias but also to enhance the model’s task-specific
effectiveness.

Efficacy in Location Encoding Soft Prompt Module: Furthermore, when comparing
PAPEFT-LE to the prompt tuning method—which lacks location encoding but has an
equivalent number of tunable parameters—PAPEFT-LE achieves an additional
average reduction in performance fluctuations of 1.54% and achieves an average
performance improvement of 3.1% over the prompt tuning method. This highlights
the benefits of integrating explicit document locations via the soft prompt
tuning module, underscoring its effectiveness.

Parameter Efficiency of Location Encoding Soft Prompt Module: As highlighted
in Table 4, PAPEFT-LE utilizes 23.87 times fewer parameters compared to the
PAPEFT-LoRA method. Despite this, the results demonstrate that PAPEFT-LE
almost achieves comparable performance improvement and variance deduction to
the PAPEFT-LoRA method, which highlighting the parameter efficiency of
location encoding soft prompt adapter.

Task # Para Ratio (%) to original model PAPEFT-LoRA 125,173,760 0.95 PAPEFT-LE
5,250,048 0.04 PAPEFT-PT 5,250,048 0.04

Table 4: Number of tunable parameters comparison.

##  7 Conclusion

In this work, we conducted a comprehensive investigation into the phenomenon
of positional bias in large language models across diverse tasks that require
retrieving relevant knowledge. Through empirical results, we demonstrated that
current LLMs exhibit a noticeable positional preference over the candidate
lists. We showed that merely adopting prompt-based solution is insufficient to
address the positional bias issue. In order to address the positional bias
issue of LLMs, we introduced a data augmentation technique to permute the
ordering of candidates within the textual context, and a position aware fine
tuning module, which explicitly integrates the locational context of each
document into the LLMs’ input through a trainable adapter module. Our
extensive experiments in recommendation and link prediction tasks demonstrate
that the proposed module can substantially mitigate positional bias with
limited tunable parameters.

## References

  * Borgeaud et al. (2022) Sebastian Borgeaud, Arthur Mensch, Jordan Hoffmann, Trevor Cai, Eliza Rutherford, Katie Millican, George Bm Van Den Driessche, Jean-Baptiste Lespiau, Bogdan Damoc, Aidan Clark, et al.  Improving language models by retrieving from trillions of tokens.  In _International conference on machine learning_ , pp. 2206–2240. PMLR, 2022.
  * Chiang et al. (2023) Wei-Lin Chiang, Zhuohan Li, Zi Lin, Ying Sheng, Zhanghao Wu, Hao Zhang, Lianmin Zheng, Siyuan Zhuang, Yonghao Zhuang, Joseph E. Gonzalez, Ion Stoica, and Eric P. Xing.  Vicuna: An open-source chatbot impressing gpt-4 with 90%* chatgpt quality, March 2023.  URL https://lmsys.org/blog/2023-03-30-vicuna/.
  * Chowdhery et al. (2023) Aakanksha Chowdhery, Sharan Narang, Jacob Devlin, Maarten Bosma, Gaurav Mishra, Adam Roberts, Paul Barham, Hyung Won Chung, Charles Sutton, Sebastian Gehrmann, et al.  Palm: Scaling language modeling with pathways.  _Journal of Machine Learning Research_ , 24(240):1–113, 2023.
  * Dao et al. (2022) Tri Dao, Dan Fu, Stefano Ermon, Atri Rudra, and Christopher Ré.  Flashattention: Fast and memory-efficient exact attention with io-awareness.  _Advances in Neural Information Processing Systems_ , 35:16344–16359, 2022.
  * Dettmers et al. (2023) Tim Dettmers, Artidoro Pagnoni, Ari Holtzman, and Luke Zettlemoyer.  Qlora: Efficient finetuning of quantized llms.  _arXiv preprint arXiv:2305.14314_ , 2023.
  * Dettmers et al. (2024) Tim Dettmers, Artidoro Pagnoni, Ari Holtzman, and Luke Zettlemoyer.  Qlora: Efficient finetuning of quantized llms.  _Advances in Neural Information Processing Systems_ , 36, 2024.
  * Guu et al. (2020a) Kelvin Guu, Kenton Lee, Zora Tung, Panupong Pasupat, and Mingwei Chang.  Retrieval augmented language model pre-training.  In _International conference on machine learning_ , pp. 3929–3938. PMLR, 2020a.
  * Guu et al. (2020b) Kelvin Guu et al.  Realm: Retrieval-augmented language model pre-training.  In _Proceedings of ICML_ , 2020b.
  * Houlsby et al. (2019) Neil Houlsby, Andrei Giurgiu, Stanislaw Jastrzebski, Bruna Morrone, Quentin De Laroussilhe, Andrea Gesmundo, Mona Attariyan, and Sylvain Gelly.  Parameter-efficient transfer learning for nlp.  In _International conference on machine learning_ , pp. 2790–2799. PMLR, 2019.
  * Hu et al. (2021) Edward J Hu, Yelong Shen, Phillip Wallis, Zeyuan Allen-Zhu, Yuanzhi Li, Shean Wang, Lu Wang, and Weizhu Chen.  Lora: Low-rank adaptation of large language models.  _arXiv preprint arXiv:2106.09685_ , 2021.
  * Jin et al. (2023) Wei Jin, Haitao Mao, Zheng Li, Haoming Jiang, Chen Luo, Hongzhi Wen, Haoyu Han, Hanqing Lu, Zhengyang Wang, Ruirui Li, et al.  Amazon-m2: A multilingual multi-locale shopping session dataset for recommendation and text generation.  _arXiv preprint arXiv:2307.09688_ , 2023.
  * Kwiatkowski et al. (2019) Tom Kwiatkowski, Jennimaria Palomaki, Olivia Redfield, Michael Collins, Ankur Parikh, Chris Alberti, Danielle Epstein, Illia Polosukhin, Jacob Devlin, Kenton Lee, et al.  Natural questions: a benchmark for question answering research.  _Transactions of the Association for Computational Linguistics_ , 7:453–466, 2019.
  * Lester et al. (2021) Brian Lester, Rami Al-Rfou, and Noah Constant.  The power of scale for parameter-efficient prompt tuning.  _arXiv preprint arXiv:2104.08691_ , 2021.
  * Lewis et al. (2020) Patrick Lewis et al.  Retrieval-augmented generation for knowledge-intensive nlp tasks.  In _Proceedings of NeurIPS_ , 2020.
  * Li et al. (2023) Dacheng Li, Rulin Shao, Anze Xie, Ying Sheng, Lianmin Zheng, Joseph E. Gonzalez, Ion Stoica, Xuezhe Ma, and Hao Zhang.  How long can open-source llms truly promise on context length?, June 2023.  URL https://lmsys.org/blog/2023-06-29-longchat.
  * Li & Liang (2021) Xiang Lisa Li and Percy Liang.  Prefix-tuning: Optimizing continuous prompts for generation.  _arXiv preprint arXiv:2101.00190_ , 2021.
  * Liu et al. (2023a) Nelson F Liu, Kevin Lin, John Hewitt, Ashwin Paranjape, Michele Bevilacqua, Fabio Petroni, and Percy Liang.  Lost in the middle: How language models use long contexts.  _arXiv preprint arXiv:2307.03172_ , 2023a.
  * Liu et al. (2023b) Pengfei Liu, Weizhe Yuan, Jinlan Fu, Zhengbao Jiang, Hiroaki Hayashi, and Graham Neubig.  Pre-train, prompt, and predict: A systematic survey of prompting methods in natural language processing.  _ACM Computing Surveys_ , 55(9):1–35, 2023b.
  * Liu et al. (2023c) Zichang Liu, Jue Wang, Tri Dao, Tianyi Zhou, Binhang Yuan, Zhao Song, Anshumali Shrivastava, Ce Zhang, Yuandong Tian, Christopher Re, et al.  Deja vu: Contextual sparsity for efficient llms at inference time.  In _International Conference on Machine Learning_ , pp. 22137–22176. PMLR, 2023c.
  * Min et al. (2021) Sewon Min, Mike Lewis, Luke Zettlemoyer, and Hannaneh Hajishirzi.  Metaicl: Learning to learn in context.  _arXiv preprint arXiv:2110.15943_ , 2021.
  * Naumov et al. (2019) Maxim Naumov, Dheevatsa Mudigere, Hao-Jun Michael Shi, Jianyu Huang, Narayanan Sundaraman, Jongsoo Park, Xiaodong Wang, Udit Gupta, Carole-Jean Wu, Alisson G Azzolini, et al.  Deep learning recommendation model for personalization and recommendation systems.  _arXiv preprint arXiv:1906.00091_ , 2019.
  * Ravaut et al. (2023) Mathieu Ravaut, Shafiq Joty, Aixin Sun, and Nancy F Chen.  On position bias in summarization with large language models.  _arXiv preprint arXiv:2310.10570_ , 2023.
  * Roberts et al. (2020) Adam Roberts, Colin Raffel, and Noam Shazeer.  How much knowledge can you pack into the parameters of a language model?  _arXiv preprint arXiv:2002.08910_ , 2020.
  * Vaswani et al. (2017) Ashish Vaswani et al.  Attention is all you need.  _Advances in neural information processing systems_ , 30, 2017.
  * Wang et al. (2020) Kuansan Wang, Zhihong Shen, Chiyuan Huang, Chieh-Han Wu, Yuxiao Dong, and Anshul Kanakia.  Microsoft academic graph: When experts are not enough.  _Quantitative Science Studies_ , 1(1):396–413, 2020.
  * Yasunaga et al. (2021) Michihiro Yasunaga, Hongyu Ren, Antoine Bosselut, Percy Liang, and Jure Leskovec.  Qa-gnn: Reasoning with language models and knowledge graphs for question answering.  _arXiv preprint arXiv:2104.06378_ , 2021.
  * Zheng et al. (2023) Chujie Zheng, Hao Zhou, Fandong Meng, Jie Zhou, and Minlie Huang.  On large language models’ selection bias in multi-choice questions.  _arXiv preprint arXiv:2309.03882_ , 2023.

##  Appendix A Appendix

In Table 5, we show the basic statistic information about the datasets used in
experiments. In Table 6, we show the statistic information about the training
and test datasets used in fine tune phase.

Task | $K$ | Average # of Words
---|---|---
REC | 20 | 4.2k
LP | 20 | 6.2k
Table 5: Data statistics for test inference. Here $K$ denotes the number of potential items to select. Task | # Train | # Test
---|---|---
REC | 2,000 | 1,000
LP | 10,000 | 3,000
Table 6:  Fine-tune data train test splits statistics.  Table 7: Examples of
zero-shot prompts used in different domains. Task
setting |  Prompt to LLM
---|---
Rec |  Task: Using a user’s historical purchase data from Amazon.com, identify one product from a distinct list of potential products that you predict the user will most likely purchase next.

Belows are 2 historical purchased products:
Bought Product [1](Title: New brothread Wash Away)
Bought Product [2](Title: Crafter’s Companion Spray & Shine, Varnish)

Belows are 20 potential products to consider:
Potential Product [1](Title: Clarins Eau Dynamisante Shower Gel 150ml)
Potential Product [2](Title: My Living World LW105 Window Bird Feeder)
…
Potential Product [20](Title: BGS Do it yourself— Cutting Box with Fine Saw)
Question: Now you need to predict ONLY one product from the potential products
that the user will most likely purchase next. What is your prediction:
LP |  Task: Based on the title and abstract of a research paper, determine one paper from a list of potential papers that the original paper is most likely to cite.

Below is the provided research paper along with its title and abstract: style
aggregated network for facial landmark detection (Abstract: …)
The following are 20 potential papers for consideration: Potential Paper
[1](decafa deep convolutional cascade for face alignment in the wild)
(Abstract: …) Potential Paper [2](do altmetrics work for assessing research
quality ) (Abstract: …) … Potential Paper [20](ai based pilgrim detection
using convolutional neural networks ) (Abstract: …) Question: Predict ONE
paper from the given potential papers that the original document would most
probably cite. Please provide the predicted paper and a brief description of
why you think it is the most likely choice:
Table 8: Prompt engineering examples, few-shot learning and hierarachical
settings. Prompt
strategy |  Prompt to LLM
---|---
FEW-shot |  Task: [Task Description]

Belows are 3 examples:
Example [1] [Exampel 1]
Example [2] [Exampel 2]
Example [3] [Exampel 3]

Belows are 2 historical purchased products:
Bought Product [1][Historical Bought Product 1]
Bought Product [2][Historical Bought Product 2]

Belows are 20 potential products to consider:
Potential Product [1] [Potential Product 1]
Potential Product [2] [Potential Product 2]
…
Potential Product [20] [Potential Product 20]
Question: Now you need to predict ONLY one product from the potential products
that the user will most likely purchase next. What is your prediction:
Hierar-chical |  Task: [Task Description]

Given the inherent challenge of selecting the prime candidate directly from a
broad list, approach this assignment hierarchically: Start by segmenting the
products into 5 equal groups. For each segmented group, determine the product
with the highest purchase likelihood. For instance, select the most likely one
from group ([1]-[4]), followed by the top pick from group ([5]-[8]), and so
on. After narrowing down to the top products from each group, decide which
among them stands the best chance of being the user’s next purchase.

Belows are 2 historical purchased products:
Bought Product [1][Historical Bought Product 1]
Bought Product [2][Historical Bought Product 2]

Belows are 20 potential products to consider:
Potential Product [1] [Potential Product 1]
Potential Product [2] [Potential Product 2]
…
Potential Product [20] [Potential Product 20]
Question: Now you need to predict ONLY one product from the potential products
that the user will most likely purchase next. What is your prediction:


# ANITA: Analytic Tableau Proof Assistant

Davi Romero Vasconcelos UFC
Quixadá, BrazilSchool of Computer Science
Federal University of Ceará
Quixadá, Brazil<EMAIL_ADDRESS>
###### Abstract

This work presents the system ANITA (Analytic Tableau Proof Assistant)
developed for teaching analytic tableaux to computer science students. The
tool is written in Python and can be used as a desktop application, or in a
web platform. This paper describes the logical system of the tool, explains
how the tool is used and compares it to several similar tools. ANITA has
already been used in logic courses and an evaluation of the tool is presented.

##  1 Introduction

Logic in Computer Science course is part of most Information and Communication
Technology curricula, such as the curricula of the Information Systems,
Software Engineering, Computer Science, and Computer Engineering of the
Federal University of Ceará at Quixadá as mandatory components. The course has
a high failure rate. For better assimilation of the contents, it is essential
that the students exercise and that they get feedback on the correctness of
their proofs.

Many deductive systems are used for teaching the formal reasoning of proofs,
such as Axiomatic Systems (a la Hilbert), Natural Deduction System [8, 9], and
Analytic Tableaux [13, 3].

The Analytic Tableau system is widely used for teaching proofs and appears in
many Logic textbooks such as [13, 12, 14, 5]. This work presents a proof
assistant, ANITA (Analytic Tableau Proof Assistant), in order to assist in the
teaching-learning of undergraduate and graduate students. For the purpose of
teaching deduction systems, we take into account in ANITA the following
features: the students should write their proofs as similar as possible to
what is available in the textbooks and to what the students would usually
write on paper; the tool should be easy-to-use and reduce the number of clicks
since mouse-clicking can be tedious; the tool should allow the student to make
mistakes and point out errors on the proofs.

The rest of the paper is organized as follows. We provide a concise definition
of Analytic Tableau system in Section 2; We propose to write proofs in
Analytic Tableaux in Fitch-style in Section 3. Section 4 describes ANITA.
Section 5 compares ANITA to other proof assistants. The evaluation of ANITA is
presented in Section 6. And, we conclude this work in Section 7.

##  2 Analytic Tableaux

We now describe Analytic Tableaux for propositional logic which we will
subsequently extend to first-order logic.

Analytic Tableaux is an inference method based on _refutation_ : to prove
$\Gamma\vdash\varphi$, we assert that each formula of $\Gamma$ is _true_ and
$\varphi$ is _false_ , in order to derive a _contradiction_. On the other
hand, if no contradiction is obtained, then we construct a _countermodel_ ,
that is, a valuation111A valuation function $v$ is a mapping from the atoms to
the set $\\{T,F\\}$. that satisfies $\Gamma$ and does not satisfy $\varphi$.

In the method of analytic tableaux, we define $T~{}\varphi$ and $F~{}\varphi$
as signed formulas to stand that $\varphi$ is true and $\varphi$ is false. The
first step to constructing a tableau is to label all formulas in $\Gamma$ with
$T$ and the formula $\varphi$ with $F$. Starting from the initial tableau,
tableau expansion rules can be used to: add new formulas to the end of a
branch ($\alpha$-type rules); or split a branch into two branches
($\beta$-type rules). The rules for the construction of tableaux are as
follows:

$\alpha$ rule |  [. $T~{}\varphi\wedge\psi$ [. $T~{}\varphi$ |  |  |  |
---|---|---|---|---|---
$T~{}\psi$ ] ] |  [. $F~{}\varphi\vee\psi$ [. $F~{}\varphi$ |  |  |  |
$F~{}\psi$ ] ] |  [. $F~{}\varphi\rightarrow\psi$ [. $T~{}\varphi$ |  |  |  |
$F~{}\psi$ ] ] |  [. $T~{}\lnot\varphi$ [. $F~{}\varphi$ ] ] |  [. $F~{}\lnot\varphi$ [. $T~{}\varphi$ ] ] |  |  |
$\beta$ rule |  [. $F~{}\varphi\wedge\psi$ [. $F~{}\varphi$ ] [. $F~{}\psi$ ] ] |  [. $T~{}\varphi\vee\psi$ [. $T~{}\varphi$ ] [. $T~{}\psi$ ] ] |  [. $T~{}\varphi\rightarrow\psi$ [. $F~{}\varphi$ ] [. $T~{}\psi$ ] ] |  |

In each branch, a formula can only be expanded once. A branch that has no more
formulas to expand is said to be saturated. A branch that has a pair of
formulas $T~{}\varphi$ and $F~{}\varphi$ is said to be closed. A closed branch
no longer needs to be expanded. A tableau is said to be closed whether it has
all its branches closed, i.e., $\Gamma\vdash\varphi$. A saturated and unclosed
branch provides a _countermodel_ , i.e., $\Gamma\not\vdash\varphi$. Figure
1(a) shows that $A\rightarrow B,B\rightarrow C,A$ entails $C$ as an analytic
tableau proof. We use $\times$ as a symbol to close a branch by the signed
formulas in the blue nodes. Figure 1(b) shows a proof, in which we have one of
the branches (red nodes) that is saturated. So, we can extract a countermodel
from the truth values of the atoms in the branch.

[.$T~{}A\rightarrow B$
$T~{}B\rightarrow C$
$T~{}A$
$F~{}C$ [.$F~{}A$ [.$\times$ ] ] [.$T~{}B$ [.$F~{}B$ [.$\times$ ] ] [.$T~{}C$
[.$\times$ ] ] ] ]

(a) $A\rightarrow B,B\rightarrow C,A\vdash C$

[.$T~{}A$
$T~{}(A\land B)\rightarrow C$
$F~{}C$ [.$F~{}A\land B$ [.$F~{}A$ [.$\times$ ] ] [.$F~{}B$ ] ] [.$T~{}C$
[.$\times$ ] ] ]
Countermodel:
$v(A)=T$ and $v(B)=v(C)=F$

(b) $A,A\wedge B\rightarrow C\not\vdash C$

Figure 1: Examples of proofs in Analytic Tableau

We extend the analytic tableau system in order to include proofs of first-
order logic, in which we have all the rules of propositional logic and add the
following rules:

$\gamma$ rule |  [. $T~{}\forall x\varphi$ [. $T~{}\varphi^{x}_{t}$ ] ] |  [. $F~{}\exists x\varphi$ [. $F~{}\varphi^{x}_{t}$ ] ]
---|---|---
|  $t$ is substitutable for $x$ in $\varphi$ |  $t$ is substitutable for $x$ in $\varphi$
$\delta$ rule |  [. $F~{}\forall x\varphi$ [. $F~{}\varphi^{x}_{a}$ ] ] |  [. $T~{}\exists x\varphi$ [. $T~{}\varphi^{x}_{a}$ ] ]
| a is a new variable | a is a new variable

Here $\varphi^{x}_{t}$ is the expression obtained from the formula $\varphi$
by replacing the variable $x$, whenever it occurs free in $\varphi$, by the
term $t$. For instance, $(H(x)\rightarrow\forall
xM(x))^{x}_{y}=(H(y)\rightarrow\forall xM(x))$. We can say that a term $t$ is
substitutable for $x$ in $\varphi$ if there is no variable $y$ in $t$ that is
captured by a $\forall y$ (or $\exists y$) quantifier of $\varphi^{x}_{t}$.
For example, term $z$ is substitutable for $y$ in $\forall xP(x,y)$. On the
other hand, term $x$ is not substitutable for $y$ in $\forall xP(x,y)$.

The above rules can occur more than once in each branch, as we can make
arbitrary substitutions of variables. Thus, in the general case, we will not
be able to generate a countermodel. Figure 2 shows examples of proofs in
Analytic Tableaux.

[.$T~{}\forall x(H(x)\rightarrow M(x))$
$T~{}\forall xH(x)$
$F~{}\forall xM(x)$ [.$F~{}M(a)$ [.$T~{}H(a)\rightarrow M(a)$ [.$T~{}H(a)$
[.$F~{}H(a)$ [.$\times$ ] ] [.$T~{}M(a)$ [.$\times$ ] ] ] ] ] ]

(a) $\forall x(H(x)\rightarrow M(x)),\forall xH(x)\vdash\forall xM(x)$

[.$T~{}\forall x(H(x)\rightarrow M(x))$
$T~{}\exists xH(x)$
$F~{}\exists xM(x)$ [.$T~{}H(a)$ [.$F~{}M(a)$ [.$T~{}H(a)\rightarrow M(a)$
[.$F~{}H(a)$ [.$\times$ ] ] [.$T~{}M(a)$ [.$\times$ ] ] ] ] ] ]

(b) $\forall x(H(x)\rightarrow M(x)),\exists xH(x)\vdash\exists xM(x)$

Figure 2: Examples of Proofs in Analytic Tableaux

##  3 Analytic Tableaux in Fitch-Style

A (signed) tableau is a certain kind of binary, labeled ordered tree where
each node is labeled by a signed formula. However, we can present a version of
the analytic tableaux in Fitch-style. The proof is written in a linear and
sequential order, in which we number all the lines, and write a statement
(signed formula) with its justification which can be a premise, the conclusion
of the proof, or the application of one of the inference rules. Each split of
a branch is delimited by $\\{$ and $\\}$. A formula can only be used in a
proof at a given point if that formula happened previously and within that
branch. In the sequel, we will present all the rules in Fitch-style.

#### Initial Tableau Rule:

A proof of $\varphi_{1},\varphi_{2},\ldots,\varphi_{n}\vdash\psi$ starts with
initial tableau as shown in Figure 3(a), where:

  * •

The premises $\varphi_{1},\varphi_{2},\ldots,\varphi_{n}$ are represented in
one line each, following a sequential numbering, labeled as $T$ (True) and as
justification “Premise”.

  * •

The conclusion $\psi$ is defined on the line after the last premise, labeled
by $F$ (False) and with the justification “Conclusion”.

1. | $~{}T~{}\varphi_{1}$ | Premise
---|---|---
2. | $~{}T~{}\varphi_{2}$ | Premise
$\vdots$ | $\vdots$ | $\vdots$
n. | $~{}T~{}\varphi_{n}$ | Premise
n+1. | $~{}F~{}\psi$ | Conclusion
$\vdots$ | $\vdots$ | $\vdots$
(a) Initial Tableau

2 T A & Premise
F A Conclusion
⋮ ⋮

(b) Sample $A\vdash A$

Figure 3: Initial Tableau Rule

#### Closed Branch Rule:

We say that a branch is closed (contains a contradiction $\bot$) in line $p$
if a formula $\varphi$ is labeled in one line $m$ with $T$ and in another line
$n$ with $F$ (both before $p$). A closed branch can no longer be expanded.
Figure 4(a) presents the scheme of this rule. Figure 4(b) shows the proof of
$A\vdash A$, in which we close the (single) branch in line $3$ from the
formula $A$ referenced in lines $1$ and $2$ as $T$ and $F$, respectively.

⋮ | ⋮ | ⋮
---|---|---
$m$. | $~{}T~{}\varphi$ |
⋮ | ⋮ | ⋮
$n$. | $~{}F~{}\varphi$ |
⋮ | ⋮ | ⋮
$p$. | $\bot$ |  $m$,$n$
(a) Closed Branch

2 T A & Premise
F A Conclusion
⊥ 1,2

(b) $A\vdash A$

Figure 4: Closed Branch Rule

The negation-true rule ($\lnot T$) is shown in Figure 5(a), where the signed
formula $F~{}\varphi$ can be obtained in line $n$ by the signed formula
$T~{}\lnot\varphi$ in line $m$. In a similar way, the negation-false rule
($\lnot F$), see Figure 5(b), can be used to show $T~{}\varphi$ in line $n$ by
$F~{}\lnot\varphi$ in line $m$. As we can see, in Figure 5(c), we conclude
$T~{}\lnot A$ in line $3$ by the negation-false rule in line $2$. So, we apply
$\lnot T$ rule and get $F~{}A$ in line $4$. Thus, we close the branch in line
$5$ (a contradiction), because we have $T~{}A$ in line $1$ and $F~{}A$ in line
$4$.

⋮ | ⋮ | ⋮
---|---|---
m. | $~{}T~{}\lnot\varphi$ |
⋮ | ⋮ | ⋮
n. | $~{}F~{}\varphi$ | $m$
(a) Negation-True ($\lnot T$)

⋮ | ⋮ | ⋮
---|---|---
m. | $~{}F~{}\lnot\varphi$ |
⋮ | ⋮ | ⋮
n. | $~{}T~{}\varphi$ | $m$
(b) Negation-False ($\lnot F$)

2 T A & Premise
F ¬¬A Conclusion
T ¬A 2
F A 3
⊥ 1,4

(c) $A\vdash\lnot\lnot A$

Figure 5: Negation Rules

The and-true rule ($\land T$) is shown in Figure 6(a), in which the signed
formulas $T~{}\varphi$ and $T~{}\psi$ in lines $n$ and $n+1$, respectively,
are obtained by the signed formula $T~{}\varphi\land\psi$ in line $m$. For
example, in Figure 6(b), we apply rule $\land T$ to $T~{}A\land B$ in line $1$
and derive $T~{}A$ and $T~{}B$, in lines $3$ and $4$.

⋮ | ⋮ | ⋮
---|---|---
m. | $~{}T~{}\varphi\land\psi$ |
⋮ | ⋮ | ⋮
n. | $~{}T~{}\varphi$ | $m$
n+1. | $~{}T~{}\psi$ | $m$
(a) And-True ($\land T$)

2 T A∧B & Premise
F A Conclusion
T A 1
T B 1
⊥ 2,3

(b) $A\land B\vdash A$

Figure 6: And-True Rule

The and-false rule ($\land F$) is shown in Figure 7(a). This rule is applied
to $F~{}\varphi\land\psi$ in line $m$ and splits this branch into two: one
that starts in line $n$ with $F~{}\varphi$; and the other in line $p$ with
$F~{}\psi$. To delimit the respective branches, we use the symbols $\\{$ and
$\\}$. For instance, in Figure 7(b), we apply $\land F$ rule to $F~{}A\wedge
B$ in line $3$ and split this branch:

  1. 1.

In the branch starting in line $4$ with $F~{}A$ which is used with $T~{}A$
from line $1$ to close this branch in line $5$.

  2. 2.

In the branch starting in line $6$ with $F~{}B$ which is used with $T~{}B$
from line $2$ to close this branch in line $7$.

It is worth noting that we can only reference the formulas in the same branch.
So, for example, the formula $F~{}A$ in line $4$ could not be referenced in
the branch starting in line $6$.

⋮ | ⋮ | ⋮
---|---|---
m. | $~{}F~{}\varphi\land\psi$ |
⋮ | ⋮ | ⋮
n. | { $F~{}\varphi$ | $m$
⋮ |  ⋮ | ⋮
| } |
p. | { $F~{}\psi$ | $m$
⋮ |  ⋮ | ⋮
| } |
(a) And-False ($\land F$)

2 T A & Premise
T B Premise
F A∧B Conclusion
{ F A 3
⊥ 1,4$~{}~{}\\}$
{ F B 3
⊥ 2,6$~{}~{}\\}$

(b) $A,B\vdash A\land B$

Figure 7: And-False Rule

The or-true rule ($\lor T$) is presented in Figure 8(a). We apply this rule to
$T~{}\varphi\lor\psi$ in line $m$ and we split this branch into two new
branches: one that starts in line $n$ with $T~{}\varphi$; and the other in
line $p$ with $T~{}\psi$. For example, in Figure 8(b), the rule $\lor T$ is
applied to $T~{}A\lor B$ in line $1$ and we split this branch:

  1. 1.

In the branch that starts in line $5$ with $T~{}A$ which is used with $F~{}A$
in line $3$ to close this branch in line $6$.

  2. 2.

In the branch starting in line $7$ with $T~{}B$ which is used with $F~{}B$ in
line $4$ to close this branch in line $8$.

⋮ | ⋮ | ⋮
---|---|---
m. | $~{}T~{}\varphi\lor\psi$ |
⋮ | ⋮ | ⋮
n. | { $T~{}\varphi$ | $m$
⋮ |  ⋮ | ⋮
| } |
p. | { $T~{}\psi$ | $m$
⋮ |  ⋮ | ⋮
| } |
(a) Or-True ($\lor T$)

2 T A∨B & Premise
T ¬B Premise
F A Conclusion
F B 2
{ T A 1
⊥ 3,5$~{}~{}\\}$
{ T B 1
⊥ 4,7$~{}~{}\\}$

(b) $A\lor B,\lnot B\vdash A$

Figure 8: Or-True Rule

The or-false rule ($\lor F$) is shown in Figure 9(a), in which the signed
formulas $F~{}\varphi$ and $F~{}\psi$ in lines $n$ and $n+1$, respectively,
are obtained by the signed formula $F~{}\varphi\lor\psi$. For example, in
Figure 9(b), we apply rule $\lor F$ to $F~{}A\lor B$ in line $2$ and derive
$F~{}A$ and $F~{}B$, in lines $3$ and $4$.

⋮ | ⋮ | ⋮
---|---|---
m. | $~{}F~{}\varphi\lor\psi$ |
⋮ | ⋮ | ⋮
n. | $~{}F~{}\varphi$ | $m$
n+1. | $~{}F~{}\psi$ | $m$
(a) Or-False ($\lor F$)

2 T A & Premise
F A∨B Conclusion
F A 2
F B 2
⊥ 1,3

(b) $A\vdash A\lor B$

Figure 9: Or-False Rule

The implication-true rule ($\rightarrow T$) is presented in Figure 10(a). We
apply this rule to $T~{}\varphi\rightarrow\psi$ in line $m$ and we split this
branch into two new branches: one that starts in line $n$ with $F~{}\varphi$;
and the other in line $p$ with $T~{}\psi$. For example, in Figure 10(b), the
rule $\rightarrow T$ is applied to $T~{}A\rightarrow B$ in line $1$ and we
split this branch:

  1. 1.

In the branch that starts in line $5$ with $F~{}\lnot A$, in which we apply
$\lnot F$ to obtain $T~{}A$ in line $6$ and, then, we use $F~{}A$ in line $3$
to close this branch in line $7$.

  2. 2.

In the branch starting in line $8$ with $T~{}B$ which is used with $F~{}B$ in
line $4$ to close this branch in line $9$.

⋮ | ⋮ | ⋮
---|---|---
m. | $~{}T~{}\varphi\rightarrow\psi$ |
⋮ | ⋮ | ⋮
n. | { $F~{}\varphi$ | $m$
⋮ |  ⋮ | ⋮
| } |
p. | { $T~{}\psi$ | $m$
⋮ |  ⋮ | ⋮
| } |
(a) Implication-True ($\rightarrow T$)

2 T ¬A→B & Premise
F A∨B Conclusion
F A 2
F B 2
{ F ¬A 1
T A 5
⊥ 6,3$~{}~{}\\}$
{ T B 1
⊥ 8,4$~{}~{}\\}$

(b) $\lnot A\rightarrow B\vdash A\lor B$

Figure 10: Implication-True Rule

The implication-false rule ($\rightarrow F$) is shown in Figure 11(a), in
which the signed formulas $T~{}\varphi$ and $F~{}\psi$ in lines $n$ and $n+1$,
respectively, are obtained by the signed formula $F~{}\varphi\rightarrow\psi$.
For example, in Figure 11(b), we apply rule $\rightarrow F$ to
$F~{}A\rightarrow B$ in line $2$ and derive $T~{}A$ and $F~{}B$, in lines $3$
and $4$.

⋮ | ⋮ | ⋮
---|---|---
m. | $~{}F~{}\varphi\rightarrow\psi$ |
⋮ | ⋮ | ⋮
n. | $~{}T~{}\varphi$ | $m$
n+1. | $~{}F~{}\psi$ | $m$
(a) Implication-False ($\rightarrow F$)

2 T B & Premise
F A→B Conclusion
T A 2
F B 2
⊥ 1,4

(b) $B\vdash A\rightarrow B$

Figure 11: Implication-False Rule

The universal-true rule ($\forall T$) is shown in Figure 12(a), in which we
apply $\forall T$-rule to signed formula $T~{}\forall x\varphi(x)$ in line $m$
and obtain, in line $n$, a signed formula $T~{}\varphi^{x}_{t}$, where $t$ is
substitutable for $x$ in $\varphi$. Figure 12(b) shows the use of this rule to
$T~{}\forall x(H(x)\rightarrow M(x))$ in line $1$ to get $T~{}H(s)\rightarrow
M(s)$ in line $4$.

⋮ | ⋮ | ⋮
---|---|---
m. | $~{}T~{}\forall x\varphi$ |
⋮ | ⋮ | ⋮
n. | $~{}T~{}\varphi^{x}_{t}$ | $m$

$t$ is substitutable for $x$ in $\varphi$

(a) Universal-True ($\forall T$)

2 T ∀x(H(x) →M(x)) & Premise
T H(s) Premise
F M(s) Conclusion
T H(s) →M(s) 1
{ F H(s) 4
⊥ 2,5$~{}~{}\\}$
{ T M(s) 4
⊥ 7,3$~{}~{}\\}$

(b) $\forall x(H(x)\rightarrow M(x)),H(s)\vdash M(s)$

Figure 12: Universal-True Rule

The universal-false rule ($\forall F$) is shown in Figure 13(a), in which we
apply $\forall F$-rule to signed formula $F~{}\forall x\varphi(x)$ in line $m$
and obtain, in line $n$, a signed formula $F~{}\varphi^{x}_{a}$, where $a$ is
a new variable. Figure 13(b) illustrates the use of this rule to $F~{}\forall
xM(x)$ in line $3$ to conclude $F~{}M(a)$ in line $4$.

⋮ | ⋮ | ⋮
---|---|---
m. | $~{}F~{}\forall x\varphi$ |
⋮ | ⋮ | ⋮
n. | $~{}F~{}\varphi^{x}_{a}$ | $m$

$a$ is new variable

(a) Universal-False ($\forall F$)

2 T ∀x(H(x) →M(x)) & Premise
T ∀x H(x) Premise
F ∀x M(x) Conclusion
F M(a) 3
T H(a) 2
T H(a) →M(a) 1
{ F H(a) 6
⊥ 5,7$~{}~{}\\}$
{ T M(a) 6
⊥ 9,4$~{}~{}\\}$

(b) $\forall x(H(x)\rightarrow M(x)),\forall xH(x)\vdash\forall xM(x)$

Figure 13: Universal-False Rule

The existential-true rule ($\exists T$) is shown in Figure 14(a), in which we
apply $\exists T$-rule to signed formula $T~{}\exists x\varphi(x)$ in line $m$
and obtain, in line $n$, a signed formula $T~{}\varphi^{x}_{a}$, where $a$ is
a new variable. Figure 14(b) illustrates the use of this rule to $T~{}\exists
x~{}H(x)$ in line $2$ to get $T~{}H(a)$ in line $4$.

⋮ | ⋮ | ⋮
---|---|---
m. | $~{}T~{}\exists x\varphi$ |
⋮ | ⋮ | ⋮
n. | $~{}T~{}\varphi^{x}_{a}$ | $m$

$a$ is new variable

(a) Existential-True ($\exists T$)

2 T ∀x(H(x) →M(x)) & Premise
T ∃x H(x) Premise
F ∃x M(x) Conclusion
T H(a) 2
F M(a) 3
T H(a) →M(a) 1
{ F H(a) 6
⊥ 4,7$~{}~{}\\}$
{ T M(a) 6
⊥ 5,9$~{}~{}\\}$

(b) $\forall x(H(x)\rightarrow M(x)),\exists xH(x)\vdash\exists xM(x)$

Figure 14: Existential-True Rule

The existential-false rule ($\exists F$) is shown in Figure 15(a), in which we
apply $\exists F$-rule to signed formula $F~{}\exists x\varphi(x)$ in line $m$
and obtain, in line $n$, a signed formula $F~{}\varphi^{x}_{t}$, where $t$ is
substitutable for $x$ in $\varphi$. Figure 15(b) illustrates the use of this
rule to $F~{}\exists xP(x)$ in line $4$ to conclude $P(a)$ in line $5$.

⋮ | ⋮ | ⋮
---|---|---
m. | $~{}F~{}\exists x\varphi$ |
⋮ | ⋮ | ⋮
n. | $~{}F~{}\varphi^{x}_{t}$ | $m$

$t$ is substitutable for $x$ in $\varphi$

(a) Existential-False ($\exists F$)

2 T P(a) & Premise
T ∃x P(x) →B Premise
F B Conclusion
{ F ∃x P(x) 2
F P(a) 4
⊥ 1,5$~{}~{}\\}$
{ T B 2
⊥ 7,3$~{}~{}\\}$

(b) $P(a),\exists xP(x)\rightarrow B\vdash B$

Figure 15: Existential-False Rule

##  4 Analytic Tableau Proof Assistant (ANITA)

The ANITA222ANITA source-code is available at
https://github.com/daviromero/anita under a MIT License. proof assistant,
Analytic Tableau Proof Assistant, is a tool written in Python that can be used
as a desktop application, or in a web platform333ANITA is available at:
https://sistemas.quixada.ufc.br/anita/en/. The main idea is that the students
can write their proofs as similar as possible to what is available in the
textbooks and to what the students would usually write on paper. ANITA allows
the students to automatically check whether a proof in the analytic tableaux
is valid. If the proof is not correct, the tool will display the errors on the
proof. So, the students may make mistakes and learn from the errors. The web
interface is very easy-to-use and has:

  * •

An area for editing the proof in plain text. The students should write a proof
in Fitch-style presented in Section 3.

  * •

A message area to display whether the proof is valid, the countermodel, or the
errors on the proof.

  * •

And the following links: _Check_ , to check the correctness of the proof;
_Manual_ , to view a document with the inference rules and examples; _LaTeX_ ,
to generate the LaTeX code444Use the _qtree_ package in your LaTeX code. of
the trees from a valid proof; _Latex in Overleaf_ to open the proof source
code directly in Overleaf555Overleaf is a collaborative platform for editing
LaTeX. Available at: http://overleaf.com/.

To facilitate the writing of the proofs, we made the following conventions in
ANITA:

  * •

The Atoms666An atomic formula or atom is simply a predicate applied to a tuple
of terms; that is, an atomic formula is a formula of the form
$P(t_{1},\ldots,t_{n})$ for $P$ a predicate, and the $t_{n}$ terms. are
written in capital letters (e.g. A, B, H(x));

  * •

Variables are written with the first letter in lowercase, followed by letters
and numbers (e.g. x, x0);

  * •

Formulas with $\forall x$ and $\exists x$ are represented by $Ax$ and $Ex$
(‘A’ and ‘E’ followed by the variable x). For instance, Ax
(H(x)$-\\!\\!>$M(x)) represents $\forall x~{}(H(x)\rightarrow M(x))$.

  * •

Figure 16 shows the equivalence of logic symbols and those used in ANITA.

  * •

The order of precedence of quantifiers and logical connectives is defined by
$\lnot,\forall,\exists,\wedge,\vee,\rightarrow$ with right alignment. For
example:

    * –

Formula $\sim$A&B$-\\!\\!>$C represents formula $(((\lnot A)\land
B)\rightarrow C)$;

    * –

The theorem $\sim$A$\mid$B $|-$ A$-\\!\\!>$C represents $((\lnot A)\vee
B)\vdash(A\rightarrow C)$.

  * •

Each inference rule will be named by its respective connective and the truth
value of the signed formula. For example, &T represents the and-true rule.
Optionally, the rule name can be omitted.

  * •

The justifications for the premises and the conclusion use the reserved words
pre and conclusion, respectively.

Symbol | $\lnot$ | $\land$ | $\lor$ | $\rightarrow$ | $\forall x$ | $\exists x$ | $\bot$ | branch | $\vdash$
---|---|---|---|---|---|---|---|---|---
LaTeX | $\backslash\textrm{lnot}$ | $\backslash\textrm{land}$ | $\backslash\textrm{lor}$ | $\backslash\textrm{rightarrow}$ | $\backslash\textrm{forall x}$ | $\backslash\textrm{exists x}$ | $\backslash\textrm{bot}$ | $[.~{}]$ | $\backslash\textrm{vdash}$
ANITA | $\sim$ | & | $\mid$ | $-\\!\\!>$ | Ax | Ex | @ | $\\{\\}$ | $|-$
Figure 16: Equivalence between the symbols of logic, ANITA and LaTeX

Figure 17(a) shows a valid proof of $A\rightarrow B,B\rightarrow C,A\vdash C$
in ANITA, and Figure 17(b) shows the tree generated by ANITA, where the blue
nodes (signed formulas) point out the closed branches. Figure 17(c)
illustrates an example of an incomplete proof of $A\rightarrow B,B\rightarrow
C,A\vdash C$ in ANITA, whereas Figure 17(d) displays the open branch in red of
the analytic tableau that was generated by ANITA.

(a) ANITA: $A\rightarrow B,B\rightarrow C,A\vdash C$

[.$T~{}A\rightarrow B$
$T~{}B\rightarrow C$
$T~{}A$
$F~{}C$ [.$F~{}A$ [.$\times$ ] ] [.$T~{}B$ [.$F~{}B$ [.$\times$ ] ] [.$T~{}C$
[.$\times$ ] ] ] ]

(b) Analytic Tableau Proof

(c) Open Branch in ANITA: $A\rightarrow B,B\rightarrow C,A\vdash C$

[.$T~{}A\rightarrow B$
$T~{}B\rightarrow C$
$T~{}A$
$F~{}C$ [.$F~{}A$ [.$\times$ ] ] [.$T~{}B$ ] ]

(d) Analytic Tableau Proof

Figure 17: ANITA: $A\rightarrow B,B\rightarrow C,A\vdash C$

Figure 18 shows a message that the existential-true rule is not applied
correctly to signed formula $T~{}Ex~{}H(x)$ in line $1$ to obtain $T~{}H(a)$
in line 4, because the term $a$ is not a new variable (see line $3$).

Figure 18: ANITA: An error in a proof

Figure 19(a) presents a proof that $A,A\land B\rightarrow C$ does not entail
$C$, and ANITA displays the countermodel of the proof. Figure 19(b) displays
the saturated branch in red of the analytic tableau that provides a
countermodel that was generated by ANITA. Figure 19(d) displays two saturated
branches in red of the analytic tableau that provide countermodels of the
proof $A\lor B\not\vdash C$ that were generated by ANITA, see Figure 19(c).
Note that in the open branch (lines $1,2$ and $3$) the atomic formula $B$ does
not occur, then $v(B)$ can be $T$ or false $F$, and the countermodel is
displayed by $v(A)=T,v(C)=F$.

(a) ANITA: $A,A\land B\rightarrow C\not\vdash C$

[.$T~{}A$
$T~{}(A\land B)\rightarrow C$
$F~{}C$ [.$F~{}A\land B$ [.$F~{}A$ [.$\times$ ] ] [.$F~{}B$ ] ] [.$T~{}C$
[.$\times$ ] ] ]

(b) Analytic Tableau Proof

(c) ANITA: $A\lor B\not\vdash C$

[.$T~{}A\lor B$
$F~{}C$ [.$T~{}A$ ] [.$T~{}B$ ] ]

(d) Analytic Tableau Proof

Figure 19: ANITA: Sample of countermodel

##  5 Related Work

In this article, we focus on Natural Deduction and Analytic Tableau proof
assistants. Although, there are proof assistants for other systems, such as
SeCaV [6]. We summarize the features of proof assistants, as well as highlight
the similarities and differences between these tools and the proposal in this
work. We also provide the proof of
$A\rightarrow~{}B,B\rightarrow~{}C,A\vdash~{}C$ in each proof assistant.

  * •

The Jape777Jape source-code is available at https://github.com/RBornat/jape/
[2] is a desktop proof assistant to write proofs in Fitch-style in Natural
Deduction. The proofs are performed by inserting the inference rules through
its GUI.

  * •

The ProofWeb [11] is a web interface that intends to be an evolution of JAPE
and uses Coq888Coq is available at https://coq.inria.fr/ that is state-of-art
proof assistant for writing mathematical proofs. The user must write the
proofs in a text area or use the GUI to add the inference rules. The ProofWeb
can display proofs in Fitch or Gentzen-styles.

  * •

The Panda [7] is also a desktop proof assistant which differs from the
previous ones by allowing the writing of proofs in Gentzen-style from its GUI.

  * •

The NaDeA999Available at https://nadea.compute.dtu.dk/ [16] is a web proof
assistant for Natural Deduction with a formalization in Isabelle. The user
must write the proofs through its user interface which is based on clicking.

  * •

The NADIA101010Available at https://sistemas.quixada.ufc.br/nadia/111111NADIA
source-code is available at https://github.com/daviromero/nadia under a MIT
License. [15] is a web proof assistant for Natural Deduction, in Fitch-style.
NADIA allows students to write their proofs as closely as possible to the
proofs they take on paper, by using an input syntax code similar to [9]. NADIA
displays proofs in Fitch or Gentzen-style.

  * •

The Carnap.io121212Available at https://carnap.io [10] is a free and open-
source Haskell framework for creating and exploring formal languages, logics,
and semantics. A web proof assistant for Analytic Tableaux131313Available at
https://carnap.io/srv/doc/truth-tree.md is available and can be used to
construct proofs by using the GUI interface.

  * •

The Tree Proof Generator Tableau141414Available at https://www.umsu.de/trees
is a tableau prover for classical propositional and first-order logic, as well
as some modal logics. The prover is written in Javascript and runs entirely in
the browser. The user can enter a formula of standard propositional,
predicate, or modal logic and the prover will automatically try to find either
a countermodel or a tree proof.

ANITA is very similar to NADIA. Both systems receive as input a text with a
proof of a theorem and check whether the proof is correct or not. If not, the
tools display the errors found. The main difference between the proof
assistants is that ANITA accepts proofs in Analytic Tableaux (see Figure
20(a)) and NADIA in Natural Deduction (see Figure 20(b)). The parser of the
proofs in ANITA is completely different from the NADIA parser, as each
implements a very different set of inference rules.

(a) ANITA: $A\rightarrow B,B\rightarrow C,A\vdash C$

(b) NADIA: $A\rightarrow B,B\rightarrow C,A\vdash C$

Figure 20: ANITA and NADIA Proof Assistants

Figure 21(a) presents a proof in ProofWeb. Note that the student has to learn
a new syntax that differs a lot from what the student would write on paper. On
the other hand, the proofs in Jape (Figure 21(b)), Panda (Figure 21(c)), NaDeA
(Figure 21(d)), and Carnap.io (Figure 22(a)) are carried out by the GUI and
the user should click on the menu to add each inference rule. The proof
generator, in fact, is a prover instead of proof assistant. So, the user can
only interact with the tool to enter the theorem to be get either a
countermodel or a tree proof that it is not very useful in order to teach how
to use the inference rules.

(a) ProofWeb: $A\rightarrow B,B\rightarrow C,A\vdash C$

(b) JAPE: $A\rightarrow B,B\rightarrow C,A\vdash C$

(c) Panda: $A\rightarrow B,B\rightarrow C,A\vdash C$

(d) NaDeA: $A\rightarrow B,B\rightarrow C,A\vdash C$

Figure 21: Natural Deduction Tableau Proof Assistants

(a) Carnap.io: $A\rightarrow B,B\rightarrow C,A\vdash C$

(b) Proof Generator: $A\rightarrow B,B\rightarrow C,A\vdash C$

Figure 22: Analytic Tableau Proof Assistants

Below we summarize the assistant proofs regarding to: the deductive systems
(ND for Natural Deduction, AT for Analytic Tableaux); the display of the
proof-style (F for Fitch-style, G for Gentzen-style); The input proof-writing
(GUI for based on clicking in the GUI interface, PT for plain text).

| ProofWeb | Jape | Panda | NaDeA | NADIA | ANITA | Carnap.io | Proof Gen.
---|---|---|---|---|---|---|---|---
Deductive Systems | ND | ND | ND | ND | ND | AT | AT | AT
Display Proof-Style | F, G | F | G | F | F, G | F | T | T
Input Proof-Writing | GUI, PT | GUI | GUI | GUI | PT | PT | GUI | GUI

##  6 Evaluation of ANITA

In this section, we present the results of the evaluation of ANITA that were
carried out in two classes of Logic in Computer Science in 2022 at the Federal
University of Ceará at Quixadá Campus. Each class has 4 hours of class per
week and a total of 16 weeks. The classes had a total of 74 students enrolled.

###  6.1 Student Evaluations of ANITA

In total 36 out of 74 registered students answered the anonymous online form
(49%). 100% of the students stated that they used ANITA as a study tool and
considered that ANITA helped to exercise the content. 91.7% considered ANITA
very easy-to-use. Figure 23(a) shows how often did the students use ANITA and
Figure 23(b) shows how they rate ANITA error messages.

(a) How often did you use ANITA?

(b) How do you rate ANITA error messages?

Figure 23: Evaluation

###  6.2 Evaluation

We used NADIA and ANITA, integrated in the Moodle platform151515Moodle is
available at https://moodle.com/, in the second partial evaluation (AP2),
which was applied in the laboratory and had four theorems to be proved in
Natural Deduction (ND) and four in analytic Tableaux (AT), each item was worth
1.25. The students wrote down the proofs of each theorem in the Moodle
platform and checked automatically, by ANITA and NADIA, whether each proof was
correct. For instance, Figure 24(a) displays the answer of a student of
Question $1$ of ND in the Moodle platform. Figure 24(b) displays the answer of
a student of Question $4$ of AT in the Moodle platform.

(a) Moodle (NADIA) - Answer of Question 1:
$\lnot~{}A\rightarrow(\lnot~{}B\rightarrow~{}C),~{}\lnot~{}B\vdash~{}A\lor~{}C$

(b) Moodle (ANITA) - Answer of Question 4:
$(A\lor B)\rightarrow D,\lnot A,\lnot D\rightarrow A\not\vdash\lnot D$

Figure 24: AP2 - Samples of questions of NADIA and ANITA in the Moodle
Platform

In total 48 out of 74 registered students did the test (65%). The students got
a mean (M) of 6.80 with standard deviation (SD) of 3.28. For ND questions,
they got 2.76 (MND) and 4.04 (MAT) for AT. 63% (AND) answered the ND
questions, of which 87% (RND) got the questions right; 92% (AAT) answered from
AT and 88% (RAT) of those answered the questions correctly. Table 1 presents
the results by class.

Class | Students | M | SD | MND | SDND | AND | RND | MAT | SDAT | AAT | RAT
---|---|---|---|---|---|---|---|---|---|---|---
A | 20 | 7.31 | 2.93 | 2.94 | 2.08 | 65% | 90% | 4.38 | 1.43 | 94% | 93%
B | 28 | 6.44 | 3.53 | 2.64 | 2.03 | 62% | 85% | 3.80 | 1.82 | 91% | 84%
A+B | 48 | 6.80 | 3.28 | 2.76 | 2,05 | 63% | 87% | 4.04 | 1.66 | 92% | 88%
Table 1: Results by Class

##  7 Conclusion and Future Work

ANITA has been used for teaching analytic tableaux to computer science
students. We have compared ANITA as a tool for teaching logic to other tools.
From the evaluation point of view, ANITA has been a success in our courses.
49% of the students answered an anonymous online form, in which: 100% consider
that the tool helped to exercise the content; 91% consider the tool easy-to-
use (excellent or good); 90% used the tool two or more times a week; and 90%
considered the understanding of messages as Excellent or Good. We used ANITA,
integrated in the Moodle platform, in the partial evaluation. In total 48 out
of 74 registered students did the test (65%). 92% of the students submitted
their proofs to 4 theorems and of these 88% got the questions right.

As future work, we consider developing more teaching materials for ANITA and
making further evaluations of ANITA as a tool for teaching logic.

Acknowledgements: This work is partially supported by the project
04772314/2020/FUNCAP.

## References

  * [1]
  * [2] Richard Bornat & Bernard Sufrin (1996): _Jape’s quiet interface_.  User Interfaces for Theorem Provers UITP’98.
  * [3] M. D’Agostino, D.M. Gabbay, R. Hähnle & J. Posegga (1999): _Handbook of Tableau Methods_.  Springer Netherlands, 10.1007/978-94-017-1754-0.
  * [4] Dirk van Dalen (2013): _Logic and Structure (5th Ed.)_.  Springer London, London, 10.1007/978-1-4471-4558-5.
  * [5] Melvin Fitting (1996): _First-Order Logic and Automated Theorem Proving (2nd Ed.)_.  Springer-Verlag, Berlin, Heidelberg, 10.1007/978-1-4612-2360-3.
  * [6] Asta Halkjær From, Frederik Krogsdal Jacobsen & Jørgen Villadsen (2022): _SeCaV: A Sequent Calculus Verifier in Isabelle/HOL_.  In Mauricio Ayala-Rincon & Eduardo Bonelli, editors: Proceedings 16th Logical and Semantic Frameworks with Applications, Buenos Aires, Argentina (Online), 23rd - 24th July, 2021, Electronic Proceedings in Theoretical Computer Science 357, Open Publishing Association, pp. 38–55, 10.4204/EPTCS.357.4.
  * [7] Olivier Gasquet, François Schwarzentruber & Martin Strecker (2011): _Panda: A Proof Assistant in Natural Deduction for All. A Gentzen Style Proof Assistant for Undergraduate Students_.  In Patrick Blackburn, Hans van Ditmarsch, María Manzano & Fernando Soler-Toscano, editors: Tools for Teaching Logic, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 85–92, 10.1007/978-3-642-21350-2_11.
  * [8] Gerhard Gentzen (1969): _The collected papers_.  North-Holland Publishing Company, 10.2307/2272429.
  * [9] Michael Huth & Mark Ryan (2004): _Logic in Computer Science: Modelling and Reasoning about Systems (2nd Ed.)_.  Cambridge University Press, 10.1017/CBO9780511810275.
  * [10] Graham Leach-Krouse (2018): _Carnap: An Open Framework for Formal Reasoning in the Browser_.  In Pedro Quaresma & Walther Neuper, editors: Proceedings 6th International Workshop on Theorem proving components for Educational software, Gothenburg, Sweden, 6 Aug 2017, Electronic Proceedings in Theoretical Computer Science 267, Open Publishing Association, pp. 70–88, 10.4204/EPTCS.267.5.
  * [11] Hendriks Maxim, Cezary Kaliszyk, Femke van Raamsdonk & Freek Wiedijk (2010): _Teaching logic using a state-of-art proof assistant_.  Acta Didactica Napocensia 3\.  Available at https://files.eric.ed.gov/fulltext/EJ1056118.pdf.
  * [12] F.S.C. da Silva, M. Finger & A.C.V. de Melo (2006): _Lógica para computação_.  Cengage Learning.  Available at https://books.google.com.br/books?id=w27uOgAACAAJ.
  * [13] R.M. Smullyan (1995): _First-order Logic_.  Dover books on advanced mathematics, Dover, 10.1007/978-3-642-86718-7.
  * [14] J.N. de Souza (2008): _Logica Para Ciencia da Computação_.  Campus SBC, Elsevier.  Available at https://books.google.com.br/books?id=Y8GEsUoRKiEC.
  * [15] D. R. Vasconcelos, R. Paula & M. V. Menezes (2022): _NADIA - Natural DeductIon proof Assistant_.  In: Anais do XXX Workshop sobre Educação em Computação, SBC, Porto Alegre, RS, Brasil, pp. 427–438, 10.5753/wei.2022.222875.
  * [16] Jørgen Villadsen, Andreas Halkjær From & Anders Schlichtkrull (2018): _Natural Deduction and the Isabelle Proof Assistant_.  In Pedro Quaresma & Walther Neuper, editors: Proceedings 6th International Workshop on Theorem proving components for Educational software, Gothenburg, Sweden, 6 Aug 2017, Electronic Proceedings in Theoretical Computer Science 267, Open Publishing Association, pp. 140–155, 10.4204/EPTCS.267.9.