# CoTEVer: Chain of Thought Prompting Annotation Toolkit
for Explanation Verification

Seungone Kim1,2 Sejune Joo1,2 Yul Jang2 Hyungjoo Chae2 Jinyoung Yeo2

KAIST AI1 Yonsei University2
<EMAIL_ADDRESS>
<EMAIL_ADDRESS>

###### Abstract

Chain-of-thought (CoT) prompting enables large language models (LLMs) to solve
complex reasoning tasks by generating an explanation before the final
prediction. Despite it’s promising ability, a critical downside of CoT
prompting is that the performance is greatly affected by the factuality of the
generated explanation. To improve the correctness of the explanations, fine-
tuning language models with explanation data is needed. However, there exists
only a few datasets that can be used for such approaches, and no data
collection tool for building them. Thus, we introduce CoTEVer, a tool-kit for
annotating the factual correctness of generated explanations and collecting
revision data of wrong explanations. Furthermore, we suggest several use cases
where the data collected with CoTEVer can be utilized for enhancing the
faithfulness of explanations. Our toolkit is publicly available at
https://github.com/SeungoneKim/CoTEVer.

##  1 Introduction

Chain-of-thought prompting (Wei et al., 2022b) generates an explanation before
the answer to elicit the reasoning capabilities of large language models. An
intuitive way to interpret chain-of-thought prompting is that the process of
‘generating an explanation’ is analogous to ‘decomposing multiple step
problems into smaller sub-problems’, which enables to solve complex reasoning
tasks. Therefore, generating a plausible explanation is crucial to derive the
correct answer (Wang et al., 2022).

To generate a plausible explanation, previous works have attempted to generate
multiple explanations and use a task-specific verifier that would access the
quality of the explanations and choose one of them (Cobbe et al., 2021; Shen
et al., 2021; Thoppilan et al., 2022; Li et al., 2022). A more fundamental
solution to this problem is fine-tuning the underlying language model with
high-quality annotated explanations (Ling et al., 2017; Cobbe et al., 2021;
Zelikman et al., 2022; Huang et al., 2022; Chung et al., 2022). However, fine-
tuning would require to gather large amounts of annotated explanation data,
which is impractical.

Figure 1: Example of Explanation Verification and Answer Verification of
GPT-3’s output. Explanation Verification requires additional knowledge which
makes it hard for annotators to intuitively write a revised explanation and
answer.

Collecting large amounts of annotated explanation data is difficult for
several reasons. First, while existing works gather explanation data by asking
annotators to manually write explanations using existing datasets (Wiegreffe
and Marasovic, 2021), gathering human authored labels is often expensive in
terms of time and cost (West et al., 2021). Second, writing a good quality
explanation from scratch is difficult because it requires sufficient
background knowledge (Geva et al., 2021).

In this paper, we address the question: can we gather explanation data in a
more efficient manner? Inspired by human-in-the-loop methods, we ask
annotators to verify a machine generated explanation instead of manually
writing them (Wallace et al., 2019; Weber et al., 2021; Du et al., 2022). In
other words, annotators get to check whether the underlying language model
hallucinate (i.e., generate explanations that are factually incorrect)
(Shuster et al., 2021; Lin et al., 2022a). To do this, we provide a set of
supporting evidence documents retrieved from the web. Annotators access the
quality of the given explanation, and provide a feedback score along with a
better alternative.

As shown in Figure 1, let’s consider gathering an explanation and answer for
the question, ‘Can you see harbor seals in Washington D.C.?’111Example from
StrategyQA (Geva et al., 2021). In this example, GPT-3 generates an
explanation ‘1) You can see harbor seals in the Pacific Ocean. 2) Washington
D.C. is not in the Pacific Ocean. 3) Therefore you cannot see harbor seals in
Washington D.C.’ and predicts ‘No’ as the answer. In this case, the first
sentence of the explanation missed the point that harbor seals not only live
in the west coast, but also in the east coast of the US. By providing the
background knowledge ‘Harbor Seals live in east and west coasts of United
States’, annotators could successfully revise the explanation.

To this end, we propose CoTEVer (Chain of Thought Prompting Annotation Toolkit
for Explanation Verification), which is designed to efficiently gather
explanation data, by 1) alleviating the role of annotators to verify instead
of writing from scratch and 2) supplementing the required background knowledge
via evidence documents. With the gathered explanation data, researchers could
use them for CoT fine-tuning (Chung et al., 2022) or transform them into other
knowledge intensive datasets.

##  2 Related Works

###  2.1 Tool-kits for Data Annotation

There exists a number of interactive tool-kits for annotating and verifying
labels (Götze et al., 2022; Lin et al., 2022b; Friedrich et al., 2021; Bach et
al., 2022; Thrush et al., 2022). For instance, Promptsource (Bach et al.,
2022), is a framework designed to try out diverse set of prompts that can be
used in in-context learning (Liu et al., 2021), or instruction tuning (Sanh et
al., 2021; Wei et al., 2021; Min et al., 2021; Ye et al., 2022; Jang et al.,
2023). Other human-in-the-loop annotation toolkits (Wallace et al., 2019;
Weber et al., 2021; Du et al., 2022) provides functionality for annotators to
verify the neural model’s prediction instead of manually creating them.
Compared to these toolkits, CoTEver provides additional features specifically
designed for gathering explanation data such as retrieving evidence documents
and supporting different Chain of Thought prompts.

###  2.2 Explanation Data

Chain of Thought Prompting is an in-context learning based methodology that
generates an explanation before the answer. Instead of directly answering to
the question, Wei et al. (2022b) conjectures that generating an explanation
on-the-fly (explain-and-generate) enhances the reasoning capabilities of large
language models. Wei et al. (2022a) argues that the ability to solve complex
reasoning only appears when using large-scale language models, and defines
this phenomenon as ‘Emergent Abilities’. CoTEver uses Chain of Thought
Prompting to generate an explanation that could serve as a starting point for
annotators to verify.

Recently, Chung et al. (2022) has shown that fine-tuning with explanation data
unlocks the emergent abilities in large language models and achieves good
performance not only at seen tasks (Ling et al., 2017; Cobbe et al., 2021;
Zelikman et al., 2022), but also unseen tasks. The explanation data collected
by CoTEVer could be used for CoT Finetuning since we collect a revised
explanation.

###  2.3 Hallucination in Language Models

Hallucination is a phenomenon where a model generates a falsehood output that
may contradict with the factual knowledge. Lin et al. (2022a) reported that as
the model size increases, the less truthful they tend to be. Lewis et al.
(2020) explains that models that rely only on parametric memory (e.g., GPT-3)
are more likely to suffer from hallucination. When collecting explanation data
from annotators, hallucination is a critical issue because the model may
generate an unfaithful but very fluent output that is not easily
distinguishable (Gao et al., 2022). To collect factually correct explanations
from annotators, we provide supporting evidence documents using a search
engine.

Figure 2: The overall illustration of CoTEver. An annotator asks a question to
CoTEver and receives an explanation, supporting evidence documents, and a
prediction. Then, the annotator’s rating of the explanation (5 for most
relevant), suggestions for a better explanation is stored in the Database
which can be used for research purposes.

##  3 System Design and Workflow

In Figure 2, we present an illustration of the overall explanation
verification process of CoTEver with 3 steps and show how the annotated
explanations could be obtained effectively. We assume a scenario where a
researcher requests a group of annotators to query a large language model and
verify the explanations and predictions to collect explanation data. Although
CoTEVer could support gathering free-form questions from annotators, it would
either require 1) the researcher to make predefined few-shot demonstrations
and retrieving them on-the-fly or 2) generating the explanation in a zero-shot
setting (Kojima et al., 2022), which is both challenging to gather good
quality explanations. Therefore, we define a scenario where a researcher
assign users to query specific type of questions, such as ‘Ask a question that
could be answered with yes/no’(Answer Format) or ‘Ask a question that is
related to economics’(Domain). In this case, we could assume that the
researcher prepared few-shot demonstrations beforehand.

###  3.1 S1: Prompting

Prompting Composition. We use GPT-3 (Brown et al., 2020) which is one of the
standard large language models for CoT prompting (Wei et al., 2022b; Kojima et
al., 2022). CoT prompting has limitations in that the generated explanations
does not have a unified format, which makes verification harder. So, we adopt
Self Ask (Press et al., 2022) as our prompting method to generate explanations
composed of sub-questions and sub-answers. We provide more details of our
prompt in Table 4.
Explanation Generation. As a first step, annotators are asked to explore our
framework by querying a variety of different questions under the designated
requirements. The user question is concatenated to the demonstrations as an
input for the model. We then send a request via OpenAI API and get a response
which contains the output of GPT-3. Upon obtaining the responses, we decompose
the output into reasoning steps consist of a sub-question and sub-answer.

###  3.2 S2: Evidence Retrieval

Document Retrieval. To help the annotators’ judgement, we provide documents
that can be used as evidence to the generated explanation. For that, we
retrieve documents using the sub-question directly as a query for document
retrieval. Note that while Press et al. (2022) use the sub-questions to
retrieve and answer to the question, we instead use them to retrieve and help
annotators verify the explanations. In order to retrieve documents that are
not outdated from the Web database, we use Google Search API
222https://pypi.org/project/google-api-python-client/. We use the top-10
documents as candidates for reranking.

Document Reranking. We first split the retrieved documents into smaller chunks
of maximum 512 tokens, the maximum number of input tokens acceptable in our
reranking module. To provide reliable evidence documents to the annotators, we
rerank the documents candidates and choose the order to be displayed on the
user interface. We obtain the embeddings of the query and the supporting
document candidates using Sentence-T5 (Ni et al., 2021), a state-of-the-art
sentence embedding model trained to capture the semantic textual similarity
between two input sequences. We then rank the retrieved documents with a
cosine similarity score between the document and query embedding.

Error Type | Example
---|---
Insufficient Knowledge 18% | Do all crustaceans live in the ocean?
Q#1: What are crustaceans? |  Crabs can be found in all oceans and in freshwater. Some crabs live on land, sometimes several miles from water. Species such as the fiddler crab live in burrows in the sand or mud, where they stay during winter and high tides.
| A#1: Crustaceans are a group of animals that
---
include crabs, lobsters, and shrimp.
Q#2: Where do crabs live?
A#2: Crabs live in the ocean.
Q#3: Where do lobsters live?
A#3: Lobsters live in the ocean.
Q#4: Where do shrimp live? |  Shrimp occur in all oceans—in shallow and deep water—and in freshwater lakes and streams.
A#4: Shrimp live in the ocean.
Q#5: Do all crustaceans live in the ocean? |
| A#5: Since crabs, lobsters, and shrimp live in the
---
ocean, all crustaceans live in the ocean.
Out of Date 22% | Could a single bitcoin ever cover cost of a Volkswagen Jetta?
Q#1: How much is a single bitcoin? |  Bitcoin’s price today is $ 21,282.48, with a 24-hour trading volume of $ 37.84 B.
A#1: A single bitcoin is about $6,000.
Q#2: How much is a Volkswagen Jetta?
A#2: A Volkswagen Jetta is about $18,645. |
| Q#3: Could a single bitcoin ever cover cost
---
of a Volkswagen Jetta?
| A#3: Since a single bitcoin is about $ 6,000,
---
and a Volkswagen Jetta is about $ 18,645,
and $ 6,000 is smaller than $ 18,645,
single bitcoin could not cover the cost
of a Volkswagen Jetta.
Wrong Fact 43% | Can a lifeboat rescue people in the Hooke Sea?
Q#1: What is the Hooke Sea? |  Hooke Crater is an impact crater in the Argyre quadrangle on Mars at 45.2°S and 44.4°W and is 139.0 km in diameter. It was named after British physicist- astronomer Robert Hooke.[1]
A#1: The Hooke Sea is a sea in Antarctica.
Q#2: Is the Hooke Sea a dangerous place?
| A#2: The Hooke Sea is a dangerous place
---
because it is a sea in Antarctica.
Q#3: What is a lifeboat? |
| A#3: A lifeboat is a boat designed for
---
rescuing people in danger.
Q#4: Can a lifeboat rescue people in the Hooke Sea? |
| A#4: Since the Hooke Sea is a dangerous place
---
in Antarctica, and a lifeboat is a boat
designed for rescuing people in danger,
lifeboat can rescue people in
the Hooke Sea.
Table 1: Examples of frequent error types within explanations. The left side
is the original explanation generated by a language model, and the right side
is the retrieved evidence document. The evidence documents could provide the
required knowledge when revising the original explanation.

###  3.3 S3: Explanation and Answer Verification

Explanation verification. In light of the provided evidence documents,
annotators could easily check the correctness of the given explanation and
give a 1-5 star Likert scale rating for each step in the explanation. In cases
where the explanation needs to be revised, annotators can submit a better
alternative. Our main intuition is that compared to writing a new explanation
from scratch, revising an explanation with the evidence documents is much more
easier for the annotators. Also, it is more likely that the revised
explanation would be factually correct because the evidence documents would
ground the required knowledge during annotation. The rating data is further
used to determine the quality of a given explanation, which we further explain
in Section 5

During the verification process, the annotators also label which evidence
document is used as an evidence. For example, in Step 2 of Figure 2, the
annotator put a check mark on the document that contains the information about
the habitat of harbor seals which contradicts to the sub-answer in the first
step, “You can see harbor seals in the Pacific Ocean.”. We further explain how
this data could be utilized in Section 5.

Answer verification. Lastly, annotators are asked to verify the correctness of
the model’s final prediction. Since large language models tend to output
incorrect conclusions when the explanation is factually mistaken (Wang et al.,
2022), it is very likely that the answer would be wrong when the original
explanation got a low score in S3.

##  4 Analysis of Explanation Data

In this section, we analyze what error cases are abundant within an
explanation and show how they can be revised using evidence documents
retrieved by CoTEVer. As mentioned in Section 3.1, we adopt a Self-Ask style
prompt and use text-davinci-002 (Ouyang et al., 2022) to generate a
corresponding explanation and answer for the train set of StrategyQA (Geva et
al., 2021). Then, we sample 300 instances where the prediction is incorrect,
ask annotators to classify the error type and revise the explanation using
CoTEVer.

While we analyze the error types of explanations using human evaluation,
automatic evaluation metrics proposed to measure the quality of a given
explanation (Golovneva et al., 2022; Chen et al., 2022) is another promising
direction, and we leave for future work. Also, we provide more detail of the
human evaluation experiment process in Appendix B. Table 1 shows three
frequently observed errors types, Insufficient Knowledge, Out of Date and
Wrong Fact along with the corresponding percentage among the error cases (18%,
22%, 43% respectively).

Insufficient Knowledge. It is well known that language models mainly learn
from high-frequency patterns and largely fail when tested on low resource
tasks such as few-shot learning Tänzer et al. (2021). Such behavior can be
seen in the first example of Table 1. In general, it may be correct that
crabs, lobsters and shrimp live in the oceans. However, the important point of
the question is whether all crustaceans live in the ocean, making the
generated explanation insufficient. The knowledge needed in such situation is
included in the evidence documents, where it indicates that crabs and shrimp
also live in freshwater.

Out of Date. The static nature of the text data that large language models are
trained on makes it difficult to cope with rapidly changing real world
situations Jang et al. (2021). For instance, in the second example of Table 1,
bitcoin is a highly volatile asset that has gone up significantly in the past
few years. According to the retrieved evidence document, it is no longer $6000
but actually more than $20k which exceeds the price of a Volkswagen Jetta.
These types of updates need to be done frequently through retrieval of up-to-
date documents.

Wrong Fact. As shown in the third example of Table 1, large language models
also generate false facts within the explanation. In this case, the first step
within the explanation quoting, "The Hooke Sea is a sea in Antarctica." is not
true. Because the Hooke Sea is not in Antarctica but on Mars, it isn’t
actually a sea, eliminating the lifeboat scenario. This fact can also be found
in the retrieved document.

##  5 How to Utilize Explanation Data gathered with CoTEVer

In this section, we suggest three promising directions on how the explanation
data collected with CoTEVer can be utilized. We define $\mathcal{E}$ and
$\mathcal{A}$ to be the original explanation and answer generated by a
language model, respectively. Similarly, the revised explanation and answer
from the annotator can be defined as $\mathcal{E}^{*}$ and $\mathcal{A}^{*}$.
Explanations consist of pairs of sub-questions ${sq}_{i}$ and sub-answers
${sa}_{i}$ which brings the following definition:

  * •

Explanation $\mathcal{E}$ with $N$ pairs of $e_{i}=({sq}_{i},{sa}_{i})$ is
$\mathcal{E}=\\{e_{i}\\}_{i=1}^{N}$

  * •

A revised explanation $\mathcal{E}^{*}$ with $N^{*}$ pairs of
$e^{*}=({sq^{*}}_{i},{sa^{*}}_{i})$ is
$\mathcal{E}^{*}=\\{e^{*}_{i}\\}_{i=1}^{N^{*}}$

Now for an explanation, sets of documents $\mathcal{D}_{i}$ are retrieved for
each pair $e_{i}$, based on ${sq}_{i}$. Within $\mathcal{D}_{i}$, we define
the top-$k^{th}$ document aligned by the re-ranking module as
$\mathcal{D}_{i}^{k}$. Finally, $\tilde{\mathcal{D}_{i}}$ is defined as the
evidence document chosen by the annotator upon the set $\mathcal{D}_{i}$.

###  5.1 Chain of Thought Fine-tuning

Chung et al. (2022) indicated that fine-tuning language models to generate an
explanation is effective to improve reasoning abilities of language models. We
suggest training a model using the revised explanation collected by CoTEVer
instead of using manually collected explanations. The objective could be
formalized such as:

$\mbox{${\cal
L}$}_{e^{*}}=-\sum_{i=1}^{|\mathcal{E^{*}}|}\sum_{j=1}^{|e^{*}_{i}|}\log
P(e^{*}_{i,j}|e^{*}_{<i},e^{*}_{i,<j})$ (1)

$\mbox{${\cal L}$}_{a^{*}}=-\sum_{i=1}^{|\mathcal{A^{*}}|}\log
P(a^{*}_{i}|a_{<i},\mathcal{E^{*}})$ (2)

where the $i^{th}$ explanation $e^{*}$ consists of $|e^{*}_{i}|$ tokens. Note
that in CoT Fine-tuning, the explanation is first generated by conditioning on
the question, and then the answer is generated by conditioning on the question
and explanation (explain-and-generate).

Unlikelihood Training In addition to using the revised explanation to teach
language models to generate an explanation coupled with the final prediction,
we also suggest using the incorrect explanations for knowledge unlearning via
unlikelihood training (Welleck et al., 2019). Prior work proposed that simply
negating the original cross entropy loss is effective in knowledge unlearning
(Jang et al., 2022). In the case of explanation data, models can forget
incorrect explanations and learn the correct explanations instead. Using the
rating score provided by the annotators, we could define how much room of
improvement there was between the original explanation and the revised
explanation. We could use ‘original explanations with relatively low scores’
among the collected explanations as hard negatives. Then, the objective could
be formalized such as:

$\mbox{${\cal
L}$}_{e}=-\sum_{i=1}^{|\mathcal{E}|}\sum_{j=1}^{|e_{i}|}\log(1-P(e_{i,j}|e_{<i},e_{i,<j}))$
(3)

Future work could consider analyzing whether forgetting the incorrect
explanation before learning the correct explanation is more effective, or vice
versa. Also, a more sophisticated definition of how to determine ‘incorrect
explanations’ and ‘correct explanations’ using the user’s feedback score could
be explored.

###  5.2 Knowledge-Intensive Tasks

As we show in Table 1, large language models tend to generate unfaithful
explanations, which is especially problematic when solving knowledge-intensive
tasks (Lewis et al., 2020). We suggest two approaches that could resolve this
issue by building datasets for fact verification and information retrieval
from the revised explanations and the evidence documents.

Fact Verification. Following the task definition of FEVER (Thorne et al.,
2018), we define labels for each pair of sub-answer ${sa}_{i}$ and a evidence
document from $\mathcal{D}_{i}$ as either Supported, Refuted, and
NotEnoughInfo.

Since the annotators use $\tilde{\mathcal{D}_{i}}$ as evidence when finding
contradictions, ${sa}_{i}$ rated as 1 and $\tilde{\mathcal{D}_{i}}$ can be
labeled as Refuted. Similarly, the pair of ${sa}^{*}_{i}$333${sa}^{*}_{i}$
where the original ${sa}_{i}$ was rated as 1, which is the lowest score. and
document $\tilde{\mathcal{D}_{i}}$ can be labeled as Supported. As low-ranked
documents $\mathcal{D}_{i}^{10}$ from our re-ranking module are less likely to
contain information that supports nor refutes the explanations, we use them as
examples for NotEnoughInfo. The fact verification data obtained with CoTEVer
could be used to to train a factual error correction model (Thorne and
Vlachos, 2021).

Information Retrieval. Karpukhin et al. (2020) explains that using negative
examples helps substantially, whilst they mitigated the difficulty in
obtaining them via setting in-batch negatives. CoTEVer is effective to acquire
hard negative as well as positive pairs using the sub-questions ${sq}_{i}$ and
a evidence document from $\mathcal{D}_{i}$.

Since the annotators find $\tilde{\mathcal{D}_{i}}$ to contain the most
helpful information when revising ${sa}_{i}$ rated as 1 to ${sa}^{*}_{i}$,
$\tilde{\mathcal{D}_{i}}$ would form a positive relation with ${sq}_{i}$.
Meanwhile, $\mathcal{D}_{i}^{10}$, which was ranked low by our re-ranking
module would serve as a hard negative for ${sq}_{i}$. The information
retrieval data obtained with CoTEVer could be used to train a enhanced dense
embedding model (Gao et al., 2021; Chuang et al., 2022).

##  6 Conclusion

In this work, we introduce CoTEver, an interactive annotation framework
designed to verify unfaithful outputs and gather truthful explanation data
from annotators. To reduce the cost of manually searching for evidence while
verifying an explanation, we provide supporting evidence documents via a
search engine. Next, we analyze some of the abundant reasons where large
language models generated incorrect explanations. Also, we suggest three
directions on how explanation data gathered with CoTEVer can be utilized. We
hope CoTEVer will contribute to gather high quality explanation data used for
future research.

## Acknowledgements

We thank Minkyeong Moon for helping make the demonstration video; Sangwon
Park, Sehwan Jeon, Imsung Yu, and Donghwan Park for helping implement the
frontend and backend of CoTEVer; Seonghyeon Ye, Hoyeon Chang, Joel Jang,
Yongho Song, and anonymous reviewers for helpful feedback. This work was
partly supported by Institute of Information & communications Technology
Planning & Evaluation (IITP) grant funded by the Korea government(MSIT) (No.
2020-0-01361, Artificial Intelligence Graduate School Program (Yonsei
University)), (No.2021-0-02068, Artificial Intelligence Innovation Hub), and
(No. 2022-0-00077, AI Technology Development for Commonsense Extraction,
Reasoning, and Inference from Heterogeneous Data). Jinyoung Yeo is the
corresponding author.

## References

  * Bach et al. (2022) Stephen H Bach, Victor Sanh, Zheng-Xin Yong, Albert Webson, Colin Raffel, Nihal V Nayak, Abheesht Sharma, Taewoon Kim, M Saiful Bari, Thibault Fevry, et al. 2022.  Promptsource: An integrated development environment and repository for natural language prompts.  _arXiv preprint arXiv:2202.01279_.
  * Brown et al. (2020) Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, et al. 2020.  Language models are few-shot learners.  _Advances in neural information processing systems_ , 33:1877–1901.
  * Chen et al. (2022) Hanjie Chen, Faeze Brahman, Xiang Ren, Yangfeng Ji, Yejin Choi, and Swabha Swayamdipta. 2022.  Rev: Information-theoretic evaluation of free-text rationales.  _arXiv preprint arXiv:2210.04982_.
  * Chuang et al. (2022) Yung-Sung Chuang, Rumen Dangovski, Hongyin Luo, Yang Zhang, Shiyu Chang, Marin Soljačić, Shang-Wen Li, Wen-tau Yih, Yoon Kim, and James Glass. 2022\.  Diffcse: Difference-based contrastive learning for sentence embeddings.  _arXiv preprint arXiv:2204.10298_.
  * Chung et al. (2022) Hyung Won Chung, Le Hou, Shayne Longpre, Barret Zoph, Yi Tay, William Fedus, Eric Li, Xuezhi Wang, Mostafa Dehghani, Siddhartha Brahma, et al. 2022.  Scaling instruction-finetuned language models.  _arXiv preprint arXiv:2210.11416_.
  * Cobbe et al. (2021) Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Jacob Hilton, Reiichiro Nakano, Christopher Hesse, and John Schulman. 2021.  Training verifiers to solve math word problems.  _arXiv preprint arXiv:2110.14168_.
  * Du et al. (2022) Wanyu Du, Zae Myung Kim, Vipul Raheja, Dhruv Kumar, and Dongyeop Kang. 2022.  Read, revise, repeat: A system demonstration for human-in-the-loop iterative text revision.  In _Proceedings of the First Workshop on Intelligent and Interactive Writing Assistants (In2Writing 2022)_ , pages 96–108.
  * Friedrich et al. (2021) Niklas Friedrich, Kiril Gashteovski, Mingying Yu, Bhushan Kotnis, Carolin Lawrence, Mathias Niepert, and Goran Glavaš. 2021.  Annie: An annotation platform for constructing complete open information extraction benchmark.  _arXiv preprint arXiv:2109.07464_.
  * Gao et al. (2022) Luyu Gao, Zhuyun Dai, Panupong Pasupat, Anthony Chen, Arun Tejasvi Chaganty, Yicheng Fan, Vincent Y Zhao, Ni Lao, Hongrae Lee, Da-Cheng Juan, et al. 2022.  Attributed text generation via post-hoc research and revision.  _arXiv preprint arXiv:2210.08726_.
  * Gao et al. (2021) Tianyu Gao, Xingcheng Yao, and Danqi Chen. 2021.  Simcse: Simple contrastive learning of sentence embeddings.  In _Proceedings of the 2021 Conference on Empirical Methods in Natural Language Processing_ , pages 6894–6910.
  * Geva et al. (2021) Mor Geva, Daniel Khashabi, Elad Segal, Tushar Khot, Dan Roth, and Jonathan Berant. 2021.  Did aristotle use a laptop? a question answering benchmark with implicit reasoning strategies.  _Transactions of the Association for Computational Linguistics_ , 9:346–361.
  * Golovneva et al. (2022) Olga Golovneva, Moya Chen, Spencer Poff, Martin Corredor, Luke Zettlemoyer, Maryam Fazel-Zarandi, and Asli Celikyilmaz. 2022.  Roscoe: A suite of metrics for scoring step-by-step reasoning.  _arXiv preprint arXiv:2212.07919_.
  * Götze et al. (2022) Jana Götze, Maike Paetzel-Prüsmann, Wencke Liermann, Tim Diekmann, and David Schlangen. 2022.  The slurk interaction server framework: Better data for better dialog models.  _arXiv preprint arXiv:2202.01155_.
  * Huang et al. (2022) Jiaxin Huang, Shixiang Shane Gu, Le Hou, Yuexin Wu, Xuezhi Wang, Hongkun Yu, and Jiawei Han. 2022.  Large language models can self-improve.  _arXiv preprint arXiv:2210.11610_.
  * Jang et al. (2023) Joel Jang, Seungone Kim, Seonghyeon Ye, Doyoung Kim, Lajanugen Logeswaran, Moontae Lee, Kyungjae Lee, and Minjoon Seo. 2023.  Exploring the benefits of training expert language models over instruction tuning.  _arXiv preprint arXiv:2302.03202_.
  * Jang et al. (2021) Joel Jang, Seonghyeon Ye, Sohee Yang, Joongbo Shin, Janghoon Han, Gyeonghun Kim, Stanley Jungkyu Choi, and Minjoon Seo. 2021.  Towards continual knowledge learning of language models.  _arXiv preprint arXiv:2110.03215_.
  * Jang et al. (2022) Joel Jang, Dongkeun Yoon, Sohee Yang, Sungmin Cha, Moontae Lee, Lajanugen Logeswaran, and Minjoon Seo. 2022.  Knowledge unlearning for mitigating privacy risks in language models.  _arXiv preprint arXiv:2210.01504_.
  * Karpukhin et al. (2020) Vladimir Karpukhin, Barlas Oguz, Sewon Min, Patrick Lewis, Ledell Wu, Sergey Edunov, Danqi Chen, and Wen-tau Yih. 2020.  Dense passage retrieval for open-domain question answering.  In _Proceedings of the 2020 Conference on Empirical Methods in Natural Language Processing (EMNLP)_ , pages 6769–6781.
  * Kojima et al. (2022) Takeshi Kojima, Shixiang Shane Gu, Machel Reid, Yutaka Matsuo, and Yusuke Iwasawa. 2022.  Large language models are zero-shot reasoners.  _arXiv preprint arXiv:2205.11916_.
  * Lewis et al. (2020) Patrick Lewis, Ethan Perez, Aleksandra Piktus, Fabio Petroni, Vladimir Karpukhin, Naman Goyal, Heinrich Küttler, Mike Lewis, Wen-tau Yih, Tim Rocktäschel, et al. 2020.  Retrieval-augmented generation for knowledge-intensive nlp tasks.  _Advances in Neural Information Processing Systems_ , 33:9459–9474.
  * Li et al. (2022) Yifei Li, Zeqi Lin, Shizhuo Zhang, Qiang Fu, Bei Chen, Jian-Guang Lou, and Weizhu Chen. 2022.  On the advance of making language models better reasoners.  _arXiv preprint arXiv:2206.02336_.
  * Lin et al. (2022a) Stephanie Lin, Jacob Hilton, and Owain Evans. 2022a.  Truthfulqa: Measuring how models mimic human falsehoods.  In _Proceedings of the 60th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers)_ , pages 3214–3252.
  * Lin et al. (2022b) Yupian Lin, Tong Ruan, Ming Liang, Tingting Cai, Wen Du, and Yi Wang. 2022b.  Dotat: A domain-oriented text annotation tool.  In _Proceedings of the 60th Annual Meeting of the Association for Computational Linguistics: System Demonstrations_ , pages 1–8.
  * Ling et al. (2017) Wang Ling, Dani Yogatama, Chris Dyer, and Phil Blunsom. 2017.  Program induction by rationale generation: Learning to solve and explain algebraic word problems.  In _Proceedings of the 55th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers)_ , pages 158–167.
  * Liu et al. (2021) Jiachang Liu, Dinghan Shen, Yizhe Zhang, Bill Dolan, Lawrence Carin, and Weizhu Chen. 2021.  What makes good in-context examples for gpt-$3$?  _arXiv preprint arXiv:2101.06804_.
  * Min et al. (2021) Sewon Min, Mike Lewis, Luke Zettlemoyer, and Hannaneh Hajishirzi. 2021.  Metaicl: Learning to learn in context.  _arXiv preprint arXiv:2110.15943_.
  * Ni et al. (2021) Jianmo Ni, Gustavo Hernández Ábrego, Noah Constant, Ji Ma, Keith B Hall, Daniel Cer, and Yinfei Yang. 2021.  Sentence-t5: Scalable sentence encoders from pre-trained text-to-text models.  _arXiv preprint arXiv:2108.08877_.
  * Ouyang et al. (2022) Long Ouyang, Jeff Wu, Xu Jiang, Diogo Almeida, Carroll L Wainwright, Pamela Mishkin, Chong Zhang, Sandhini Agarwal, Katarina Slama, Alex Ray, et al. 2022\.  Training language models to follow instructions with human feedback.  _arXiv preprint arXiv:2203.02155_.
  * Press et al. (2022) Ofir Press, Muru Zhang, Sewon Min, Ludwig Schmidt, Noah A Smith, and Mike Lewis. 2022.  Measuring and narrowing the compositionality gap in language models.  _arXiv preprint arXiv:2210.03350_.
  * Sanh et al. (2021) Victor Sanh, Albert Webson, Colin Raffel, Stephen H Bach, Lintang Sutawika, Zaid Alyafeai, Antoine Chaffin, Arnaud Stiegler, Teven Le Scao, Arun Raja, et al. 2021.  Multitask prompted training enables zero-shot task generalization.  _arXiv preprint arXiv:2110.08207_.
  * Shen et al. (2021) Jianhao Shen, Yichun Yin, Lin Li, Lifeng Shang, Xin Jiang, Ming Zhang, and Qun Liu. 2021.  Generate & rank: A multi-task framework for math word problems.  _arXiv preprint arXiv:2109.03034_.
  * Shuster et al. (2021) Kurt Shuster, Spencer Poff, Moya Chen, Douwe Kiela, and Jason Weston. 2021.  Retrieval augmentation reduces hallucination in conversation.  In _Findings of the Association for Computational Linguistics: EMNLP 2021_ , pages 3784–3803.
  * Srivastava et al. (2022) Aarohi Srivastava, Abhinav Rastogi, Abhishek Rao, Abu Awal Md Shoeb, Abubakar Abid, Adam Fisch, Adam R Brown, Adam Santoro, Aditya Gupta, Adrià Garriga-Alonso, et al. 2022.  Beyond the imitation game: Quantifying and extrapolating the capabilities of language models.  _arXiv preprint arXiv:2206.04615_.
  * Tänzer et al. (2021) Michael Tänzer, Sebastian Ruder, and Marek Rei. 2021.  Bert memorisation and pitfalls in low-resource scenarios.  _arXiv preprint arXiv:2105.00828_.
  * Thoppilan et al. (2022) Romal Thoppilan, Daniel De Freitas, Jamie Hall, Noam Shazeer, Apoorv Kulshreshtha, Heng-Tze Cheng, Alicia Jin, Taylor Bos, Leslie Baker, Yu Du, et al. 2022.  Lamda: Language models for dialog applications.  _arXiv preprint arXiv:2201.08239_.
  * Thorne and Vlachos (2021) James Thorne and Andreas Vlachos. 2021.  Evidence-based factual error correction.  In _Proceedings of the 59th Annual Meeting of the Association for Computational Linguistics and the 11th International Joint Conference on Natural Language Processing (Volume 1: Long Papers)_ , pages 3298–3309.
  * Thorne et al. (2018) James Thorne, Andreas Vlachos, Christos Christodoulopoulos, and Arpit Mittal. 2018\.  Fever: a large-scale dataset for fact extraction and verification.  In _Proceedings of the 2018 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, Volume 1 (Long Papers)_ , pages 809–819.
  * Thrush et al. (2022) Tristan Thrush, Kushal Tirumala, Anmol Gupta, Max Bartolo, Pedro Rodriguez, Tariq Kane, William Gaviria Rojas, Peter Mattson, Adina Williams, and Douwe Kiela. 2022.  Dynatask: A framework for creating dynamic ai benchmark tasks.  _arXiv preprint arXiv:2204.01906_.
  * Wallace et al. (2019) Eric Wallace, Pedro Rodriguez, Shi Feng, Ikuya Yamada, and Jordan Boyd-Graber. 2019\.  Trick me if you can: Human-in-the-loop generation of adversarial examples for question answering.  _Transactions of the Association for Computational Linguistics_ , 7:387–401.
  * Wang et al. (2022) Xuezhi Wang, Jason Wei, Dale Schuurmans, Quoc Le, Ed Chi, and Denny Zhou. 2022.  Self-consistency improves chain of thought reasoning in language models.  _arXiv preprint arXiv:2203.11171_.
  * Weber et al. (2021) Verena Weber, Enrico Piovano, and Melanie Bradford. 2021.  It is better to verify: Semi-supervised learning with a human in the loop for large-scale nlu models.  In _Proceedings of the Second Workshop on Data Science with Human in the Loop: Language Advances_ , pages 8–15.
  * Wei et al. (2021) Jason Wei, Maarten Bosma, Vincent Y Zhao, Kelvin Guu, Adams Wei Yu, Brian Lester, Nan Du, Andrew M Dai, and Quoc V Le. 2021.  Finetuned language models are zero-shot learners.  _arXiv preprint arXiv:2109.01652_.
  * Wei et al. (2022a) Jason Wei, Yi Tay, Rishi Bommasani, Colin Raffel, Barret Zoph, Sebastian Borgeaud, Dani Yogatama, Maarten Bosma, Denny Zhou, Donald Metzler, et al. 2022a.  Emergent abilities of large language models.  _arXiv preprint arXiv:2206.07682_.
  * Wei et al. (2022b) Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Ed Chi, Quoc Le, and Denny Zhou. 2022b.  Chain of thought prompting elicits reasoning in large language models.  _arXiv preprint arXiv:2201.11903_.
  * Welleck et al. (2019) Sean Welleck, Ilia Kulikov, Stephen Roller, Emily Dinan, Kyunghyun Cho, and Jason Weston. 2019.  Neural text generation with unlikelihood training.  _arXiv preprint arXiv:1908.04319_.
  * West et al. (2021) Peter West, Chandra Bhagavatula, Jack Hessel, Jena D Hwang, Liwei Jiang, Ronan Le Bras, Ximing Lu, Sean Welleck, and Yejin Choi. 2021.  Symbolic knowledge distillation: from general language models to commonsense models.  _arXiv preprint arXiv:2110.07178_.
  * Wiegreffe and Marasovic (2021) Sarah Wiegreffe and Ana Marasovic. 2021.  Teach me to explain: A review of datasets for explainable natural language processing.  In _Thirty-fifth Conference on Neural Information Processing Systems Datasets and Benchmarks Track (Round 1)_.
  * Ye et al. (2022) Seonghyeon Ye, Doyoung Kim, Joel Jang, Joongbo Shin, and Minjoon Seo. 2022.  Guess the instruction! making language models stronger zero-shot learners.  _arXiv preprint arXiv:2210.02969_.
  * Zelikman et al. (2022) Eric Zelikman, Yuhuai Wu, and Noah D Goodman. 2022.  Star: Bootstrapping reasoning with reasoning.  _arXiv preprint arXiv:2203.14465_.

##  Appendix A Link to Video & Code

The link to our video and code is as follows:

  1. 1.

Demonstration Video: Link

  2. 2.

Official Code: Link

##  Appendix B Experiment Details for Human Evaluation

Following Wei et al. (2022b), we use the open-domain setting (question-only
set) of StrategyQA (Geva et al., 2021) from Srivastava et al. (2022). We use
text-davinci-002 to generate explanations. We set the temperature as 0.

The 6-shot prompt we used are shown in Table 4. Our prompt are divided into
sub-questions and sub-answers where the sub-questions are used as a query for
retrieving the evidence documents.

strategyQA
---
CoT (Wei et al., 2022b) | CoTEVer (Ours)
65.4 | 70.52

Table 2: Few-shot Prompting accuracy on StrategyQA(question-only set). Our
prompt consists of sub-questions and sub-answers.

Table 2 shows the performance when using our designed prompt. Although our
purpose of consisting prompts with sub-questions was for evidence retrieval,
Self-Ask (Press et al., 2022) style prompts achieves better performance
compared to the prompts used in Wei et al. (2022b). Also, these results
support the fact that the incorrect explanations(29.18%) were not generated
due to the quality of our prompt.

To analyze the error types, we sample 300 incorrect instances since the
explanation is likely to be wrong when the prediction is incorrect (Wang et
al., 2022). We ask 20 annotators with background in deep learning and
proficient English skills to 1)classify the error type and 2)revise the
explanation using CoTEVer. While the error types introduced in Table 1 (total
83%) could be revised based on the supporting evidence documents, 17% were
error types were GPT-3 didn’t generate a final prediction by keep repeating
itself, or error types where the knowledge was all correct, but the reasoning
was incorrect. In this case, retrieving evidence documents does not help
during explanation verification.

##  Appendix C Limitations

The following are the limitations of CoTEVer.

Dependency on Prompt Design. While we experimented with prompts from
StrategyQA, where only yes/no questions are given, annotators could type in
any form of questions such as multiple choice questions or ‘why’ style
questions. In this case, the prompts used to query a large language model
should be changed. Therefore, we provide functionality where the researcher
using CoTEVer could change the prompt. To prevent unexpected behavior of large
language models, it is recommended to instruct annotators what types of
questions they should ask. Also beside output format, large language models
are also sensitive to the domain of the question. For example, when annotators
ask questions requiring financial of legal domain knowledge, the prompts we
provided might not perform well. In this case, researchers should change the
prompts to their needs.

Prevention on Usage for Unethical Use Cases. Large language models often tend
to generate toxic outputs. This is a critical issue when annotators use our
framework. Our annotation toolkit is built on top of the Open AI API, where
there has been various attempts to mitigate the toxic behavior of GPT-3. For
instance, their text-davinci-002 version uses reinforcement learning to align
towards non-toxic language.

Cases when Explanation is wrong due to In-correct Reasoning. While CoTEVer
could supplement insufficient knowledge for annotators, it couldn’t tell which
step within the explanation contains incorrect reasoning.

Error Type | Example
---|---
Incomplete Answer | Is Black Lives Matter connected with capsaicin?
#Q1 : What is capsaicin? |  Capsaicin (8-methyl-N-vanillyl-6-none namide) is an active component of chili peppers, which are plants belonging to the genus Capsicum. It is a chemical irritant for mammals, including humans, and produces a sensation of burning in any tissue with which it comes into contact.
#A1 : Capsaicin is a chemical compound
that can be found in chili peppers.
#Q1 : What is Black Lives Matter?
#A1 : Black Lives Matter is a movement that fights against
racism and violence towards black people.
#Q2 : Is Black Lives Matter connected with capsaicin?
#A2 : Since Black Lives Matter is a movement that fights
against racism and violence towards black people,
and capsaicin is a chemical compound that can be found
in chili peppers, Black Lives Matter is not connected
with capsaicin.
So the answer is no.
Wrong Fact | Does Soylent use Pea for their source of protein?
#Q1 : What is Soylent? |  Soy protein isolate is the ingredient we use in Soylent as our source of protein.
#A1 : Soylent is a meal replacement drink.
#Q2 : What is the source of protein for Soylent?
#A2 : Soylent uses pea protein.
#Q3 : Does Soylent use Pea for their source
#A3 : Since Soylent uses pea protein, Soylent uses pea for
their source of protein.
So the answer is yes.
Update Required | Has Kelly Clarkson outsold season 4 American Idol winner?
#Q1 : Who won season 4 of American Idol? |  To date, Clarkson has sold over 28 million albums and 54 million singles worldwide.
#A1 : Carrie Underwood won season 4 of American Idol.
#Q2 : How many albums did Carrie Underwood sell?
#A2 : Carrie Underwood sold over 15 million albums.
#Q2 : How many albums did Kelly Clarkson sell?
#A2 : Kelly Clarkson sold over 25 million albums.
#Q3 : Has Kelly Clarkson outsold season 4 American Idol |  Throughout her career, Underwood has sold 66 million albums worldwide. In the United States, she remains the best -selling album artist from American Idol franchise with a total of 16.3 million albums sold
winner?
#A3 : Since Kelly Clarkson sold over 25 million albums, and
Carrie Underwood sold over 15 million albums, Kelly
Clarkson sold more albums than Carrie Underwood.
So the answer is yes.
Table 3: Additional Examples of frequent error types within explanations. The
left side is the original explanation generated by a language model, and the
right side is the retrieved evidence document. The evidence documents could
provide the required knowledge when revising the original explanation. Figure
3: Snapshot of CoTEVer. Annotator gets to type in a question, and receive the
output of a large language model(e.g., GPT-3). Figure 4: Snapshot of CoTEVer.
Annotator could check the retrieved evidence documents in order to verify each
step within the explanation. Prompt
---
| [Example 1]
---
Question: Do hamsters provide food for any animals?
Output:
Sub Question #0 : What type of animals are hamsters?
Sub Answer #0 : Hamsters are prey animals.
Sub Question #1 : Can prey animals be food for other animals?
Sub Answer #1 : Prey are food for predators.
Sub Question #2 : Do hamsters provide food for any animals?
Sub Answer #2 : Since hamsters are prey animals, and prey are food
for predators, hamsters provide food for some animals.
Final Answer : So the answer is yes.
[Example 2]
Question: Could Brooke Shields succeed at University of Pennsylvania?
Output:
Sub question #0 : What university did Brooke Shields went to?
Sub answer #0 : Brooke Shields went to Princeton University.
Sub question #1 : Did Brooke Shields succeed at Princeton University?
Sub answer #1 : At Princeton University, she got all As and Bs while
pursing her bachelor’s degree in French literature, meaning she had a
successful school life.
Sub question #2 : How rigorous is Princeton University compared to
University of Pennsylvania?
Sub answer #2 : Princeton University is about as academically rigorous
as the University of Pennsylvania because they have a similar ranking
according to U.S. News Rankings.
Sub question #3 : Could Brooke Shields succeed at University of Pennsylvania?
Sub answer #3 : Since University of Pennsylvania and University of
Princeton are in similar circumstances, Brooke Shields has been successful
in University of Princeton, Brooke Shields could also succeed at the
University of Pennsylvania.
So the answer is yes.
[Example 3]
Question: Hydrogen\u2019s atomic number squared exceeds number of Spice Girls?
Output:
Sub question #0 : What is the atomic number of Hydrogen?
Sub answer #0 : Hydrogen has an atomic number of 1.
Sub question #1 : What is 1 squared?
Sub answer #1 : 1 squared is 1.
Sub question #2 : How much Spice Girls are there?
Sub answer #2 : There are 5 Spice Girls.
Sub question #3 : Hydrogen\u2019s atomic number squared exceeds number
of Spice Girls?
Sub answer #3 : Since Hydrogen’s atomic number squared is 1, the number of
Spice Girls are 5, and 1 is smaller than 5, Hydrogen\u2019s atomic number
squared is less than the number of Spice Girls.
So the answer is no.
| [Example 4]
---
Question: Is it common to see frost during some college commencements?
Output:
Sub question #0 : When does College commencement ceremonies usually happen?
Sub answer #0 : College commencement ceremonies can happen in December,
May, and June.
Sub question #1 : Does it usually frost in December?
Sub answer #1 : December is in the winter, so there can be frost.
Sub question #2 : Is it common to see frost during some college commencements?
Sub answer #2 : Since there can be frost in December and a college
commencement are held in December, there could be frost at some commencements.
So the answer is yes.
[Example 5]
Question: Could a llama birth twice during War in Vietnam (1945-46)?
Output:
Sub question #0 : How long was the Vietnam war?
Sub answer #0 : The War in Vietnam was 6 months.
Sub question #1 : How long is the gestation period?
Sub answer #1 : The gestation period for a llama is 11 months.
Sub question #2 : How long does it take for a llama to birth twice?
Sub answer #2 : Since the gestation period for a llama is 11 months,
and 11 times 2 is 22, it will take 22 months.
Sub question #3 : Could a llama birth twice during War in Vietnam (1945-46)?
Sub answer #3 : Since it takes 22 months for a llama to birth twice,
War in Vietnam was 6 months, and 22 is bigger than 6, llama could not
give birth twice during the War in Vietnam.
So the answer is no.
[Example 6]
Question: Would a pear sink in water?
Output:
Sub question #0 : What is the density of a pear?
Sub answer #0 : The density of a pear is about 0.6g/cm3.
Sub question #1 : What is the density of water?
Sub answer #1 : The density of water is 1g/cm3.
Sub question #2 : Is the density of pear smaller than water?
Sub answer #2 : Since 0.6 is smaller than 1, the density of pear
is smaller than water.
Sub question #3 : If the density of an object is less than water, what
happens?
Sub answer #3 : Objects less dense than water float.
Sub question #4 : Would a pear sink in water?
Sub answer #4 : Since a pear has a smaller density than water, a pear would
float.
So the answer is no.
[Example 7]
Table 4: Prompt used to gather explanations for human evaluation experiments.


where $\sigma_2$ = { v2 $\mapsto$ v2, v3 $\mapsto$ v3, e2 $\mapsto$ e2,
e3 $\mapsto$ e3, e4 $\mapsto$ e4 }

Representing the shared variable modularisation used
in Figure <ref> using specification-building operators.

Figure <ref> recasts the shared variable example of
Figure <ref> using specification-building operators.
The specification-building operator hide via, used on lines 2
and 8 of Figure <ref>, is used to hide auxiliary
signature items (variables and events in this case) by means of
omitting them from the signature morphisms $\sigma_1$ and
$\sigma_2$.  The two external events are created using the signature
morphisms defined in lines 3 and 9 of Figure <ref>.

In contrast, Figure <ref> illustrates shared event
decomposition, which partitions an Event-B machine
based on variables which participate in the same events
In this example, a clean partition is not possible, and the user has
chosen to allocate variable  to sub-machine
and variables  and  to sub-machine .
The problem now is caused by event  which uses variables
and  and thus cannot be cleanly allocated to
either machine.   The solution is to decompose event  into
two events  and . These new events
each correspond to a restricted version of the original event
, each confined to the guards and actions that refer to
each of the variable sets (i.e.  contains only the
guards and actions of  that referenced ).

The shared event decomposition of machine
into sub-machines  and . Here we
wish to partition machine  into two sets of variables, as shown by
the dotted line.

(M hide via $\sigma_1$)
with { e2 $\mapsto$ e2_1 }
$\sigma_1$ = { v1 $\mapsto$ v1, e1 $\mapsto$ e1, e2 $\mapsto$ e2 }

(M hide via $\sigma_2$)
with { e2 $\mapsto$ e2_2 }
$\sigma_2$ = { v2 $\mapsto$ v2, v3 $\mapsto$ v3, e2 $\mapsto$ e2,
e3 $\mapsto$ e3, e4 $\mapsto$ e4 }

Representing the shared event modularisation used
in Figure <ref> using specification-building operators

Figure <ref> represents this decomposition using
specification-building operators.  In each case we use hiding with a
signature morphism to specify the signature components that we wish to
keep, and then the shared event is renamed.  The identity mappings for
the variables on lines 6, 12 and 13 have the effect of hiding those
variables that belong to the other machine.  Thus these variables can
still be used in constraints, but are no longer externally visible.
Since the machines  and  do not share any common
variables they can now be refined independently.

§.§.§ Generic Instantiation

The generic instantiation approach to re-use in Event B is
intended to facilitate the parametrisation of machines, so that a
refinement chain can be re-used [4].  The
idea is that a chain of existing machine refinements is made generic
with respect to all of the carrier sets, constants and axioms that
have been collected in the contexts used throughout. It is then
possible for a user to instantiate these sets and constants
differently in a new model.  In order to reuse the proofs of the old
model, its axioms must then be proven as theorems after instantiation
in the new model. This process facilitates the reuse of existing
Event-B models thus providing a more modular approach to specification
in Event-B.

Figure <ref> is an example of using the generic
instantiation plugin for  [62]. Here, a
machine  has been specified (in outline) on lines 6–10,
and it depends on a context  specified on lines 1–5.
This is standard Event B syntax, and the machine is not marked as
genericised in any way.  The instantiation is shown on lines 11–20 of
Figure <ref>, where a machine  is
specified (again, in outline), and declared to instantiate
, by providing a context  as an
implementation of  (lines 12–13).  The details of the
instantiation are made explicit in the following lines, where the
elements of the context  are replaced by corresponding
elements from  (lines 14–16), and the variables and events of
are renamed (lines 17–19).

The generic instantiation plugin generates extra proof
obligations to ensure that the instantiation of the original machine
is a valid one and that if the instantiated machine refines an
existing model that this is a valid refinement. The machine and its
instance are linked via refinement and once the proof obligations have
been carried out successfully then the rest of the pattern refinement
chain can be instantiated.

ctx2 //contains instance properties
//replace parameters defined in ctx1
S$_1$ := ctx2_S$_1$,…, S$_m$ := ctx2_S$_m$
C$_1$ := ctx2_C$_2$,…, C$_n$ := ctx2_C$_n$
// rename elements in mac
v$_1$ := ctx2_v$_1$,…, v$_q$ := ctx2_v$_q$
ev$_1$ := ctx2_ev$_1$,…, ev$_r$ := ctx2_ev$_r$

The machine  is defined as an instantiation of
the machine  using the generic instantiation plugin.

sorts S$_1$,…, S$_m$
ops C$_1$,…, C$_n$
. Ax$_1$,…,Ax$_p$

ctx1 then
ops v$_1$,…,v$_q$

(ctx2 then mac)
{S$_1$ $\mapsto$ ctx2_S$_1$,…, S$_m$ $\mapsto$ ctx2_S$_m$,
C$_1$ $\mapsto$ ctx2_C$_2$,…, C$_n$ $\mapsto$ ctx2_C$_n$,
v$_1$ $\mapsto$ ctx2_v$_1$,…, v$_q$ $\mapsto$ ctx2_v$_q$,
ev$_1$ $\mapsto$ ctx2_ev$_1$,…, ev$_r$ $\mapsto$ ctx2_ev$_r$}

A representation of generic instantiation using
specification-building operators in .

There are many ways of implementing this using the specification-building operators, and we provide one example in Figure
<ref>. In fact, the theory of institutions is equipped with
a concept of parameterisation and it is easy to see how we could have
used this to represent the generic instantiation in Figure
<ref> by giving the context,  as a parameter
to the specification for  with the appropriate signature
morphisms in the  institution.  However, this would involve
changing the original specification of , and so we have
chosen a specification in Figure <ref> that more closely
resembles the approach shown in Figure <ref>.
The main elements of the instantiation are the inclusion of
and  in  (line 12), along
with a series of appropriate renamings (lines 13–17) to match those in
the original.

In fact, the possibilities provided by the specification-building
operators are much more general than those provided by the generic
instantiation plugin.  Using the generic instantiation plugin, only
user defined sets can be replaced so it is not possible, for example,
to replace $\mathbb{Z}$, $\mathbb{N}$ or $BOOL$.  Moreover, it is a
requirement that all sets and contexts be replaced ensuring
that there are no uninstantiated parameters.  One of the main benefits
of using specification-building operators over  is that it is
now possible to replace any sets that a user wishes, once the
appropriate signature morphisms have been defined by the user.  It is
also possible to generalise machines in  using any signature
elements, including other machines, as parameterisation is not limited
to just sorts and constants.

§ CONCLUSIONS AND FUTURE WORK

In this paper, we provide a detailed description of the Event-B institution, .
Our definition of  allows the restructuring of Event-B specifications using the standard specification-building operators for institutions <cit.>. Thus  provides a means for writing down and splitting up the components of an Event-B system, facilitating increased modularity for Event-B specifications. We have also shown how the institutional framework subsumes and can explicitly represent Event-B refinement.

Moreover, we contribute a formal semantics for the Event-B formal specification language. We achieved this by constructing a three-layer model for the Event-B language that decomposed it into its mathematical, infrastructure and superstructure sub-languages.
The  semantics that we have presented for each of these three constituent languages and thus for Event-B itself is grounded in the theory of institutions using our institution for Event-B () and the institution for first-order predicate logic with equality (). We have described a Haskell implementation of this semantics in our  translator tool and illustrated how it is used to generate syntactically sugared -specifications. We demonstrate our approach using the cars on a bridge example taken from Abrial's book [2].

Further to this, we have discussed refinement and illustrated the use of the specification-building operators as modularisation constructs in the  institution.
Institutions are designed with modularity and interoperability in mind and so our approach does not inhibit using multiple modelling domains to evaluate the semantics of an Event-B model. In fact, we have provided scope for the interoperability of Event-B with other formalisms that have been described in this institutional framework. Future work includes defining further institution-theoretic relationships between  and other formalisms that have been defined in the theory of institutions. This will provide a solid, mathematical foundation for their combination.

[1]
J.-R. Abrial.
Event model decomposition.
Technical report, Department of Computer Science, ETH Zurich, 2009.

[2]
J.-R. Abrial.
Modeling in Event-B: System and Software Engineering.
Cambridge University Press, 1st edition, 2010.

[3]
J.-R. Abrial, M. Butler, S. Hallerstede, T. S. Hoang, F. Mehta, and L. Voisin.
Rodin: an open toolset for modelling and reasoning in Event-B.
International Journal on Software Tools for Technology
Transfer, 12(6):447–466, 2010.

[4]
J.-R. Abrial and S. Hallerstede.
Refinement, decomposition, and instantiation of discrete models:
Application to Event-B.
Fundamenta Informaticae, 77(1-2):1–28, 2007.

[5]
T. K. Astarte and C. B. Jones.
An exegesis of four formal descriptions of ALGOL 60.
Technical Report CS-TR-1498, Computing Science, Newcastle University,
September 2016.

[6]
R.-J. Back.
Refinement calculus, part II: Parallel and reactive programs.
In Stepwise Refinement of Distributed Systems Models,
Formalisms, Correctness, volume 430 of Lecture Notes in Computer
Science, pages 67–93, 1990.

[7]
R.-J. Back and J. von Wright.
Refinement Calculus: A systematic introduction.
Springer, 1998.

[8]
J. A. Bergstra, J. Heering, and P. Klint, editors.
Algebraic Specification.
Addison Wesley, 1989.

[9]
D. Bjørner.
Software Engineering 1: Abstraction and Modelling.
Springer, 2006.

[10]
R. M. Burstall and J. A. Goguen.
Putting theories together to make specifications.
In 5th International Joint Conference on Artificial
intelligence, IJCAI, volume 2, pages 1045–1058. Morgan Kaufmann, 1977.

[11]
R. M. Burstall and J. A. Goguen.
The semantics of Clear, a specification language.
In Abstract Software Specifications, volume 86 of Lecture
Notes in Computer Science, pages 292–332, 1980.

[12]
M. Butler.
Decomposition structures for Event-B.
In 7th International Conference on Integrated Formal Methods,
volume 5423 of Lecture Notes in Computer Science, pages 20–38, 2009.

[13]
P. F. Castro, N. Aguirre, C. L. Pombo, and M. TSE.
Categorical foundations for structured specifications in Z.
Formal Aspects of Computing, 27(5–6):831–865, 2015.

[14]
R. Diaconescu, J. Goguen, and P. Stefaneas.
Logical support for modularisation.
In Workshop on Logical Frameworks, pages 83–130, 1991.

[15]
H. Ehrig, B. Mahr, I. Classen, and F. Orejas.
Introduction to algebraic specification. part 1: Formal methods for
software development.
The Computer Journal, 35(5):460–467, 1992.

[16]
M. Farrell.
Event-B in the Institutional Framework: Defining a Semantics,
Modularisation Constructs and Interoperability for a Specification Language.
PhD thesis, Department of Computer Science, Maynooth University,
Ireland, 2017.

[17]
M. Farrell, R. Monahan, and J. F. Power.
Combining Event-B and CSP: An Institution Theoretic Approach to
In 19th International Conference on Formal Engineering Methods,
ICFEM, volume 10610 of Lecture Notes in Computer Science, pages
140–156, 2017.

[18]
M. Farrell, R. Monahan, and J. F. Power.
An institution for Event-B.
In Recent Trends in Algebraic Development Techniques, volume
10644 of Lecture Notes in Computer Science, pages 104–119, 2017.

[19]
M. Farrell, R. Monahan, and J. F. Power.
Specification Clones: An empirical study of the structure of
Event-B specifications.
In 15th International Conference on Software Engineering
and Formal Methods, SEFM, volume 10469 of Lecture Notes in Computer
Science, pages 152–167, 2017.

[20]
L. M. G. Feijs.
An overview of the development of COLD.
In Semantics of Specification Languages (SoSL), pages 15–22.
Springer London, 1994.

[21]
C. Ghezzi, M. Jazayeri, and D. Mandrioli.
Fundamentals of Software Engineering.
Prentice Hall, 2002.

[22]
J. A. Goguen and R. M. Burstall.
Introducing institutions.
In Workshop on Logic of Programs, volume 164 of Lecture
Notes in Computer Science, pages 221–256, 1983.

[23]
J. A. Goguen and R. M. Burstall.
Institutions: abstract model theory for specification and
Journal of the ACM, 39(1):95–146, 1992.

[24]
J. A. Goguen, J. Goguen, and G. Malcolm.
Algebraic semantics of imperative programs.
MIT Press, 1996.

[25]
A. Gondal, M. Poppleton, and M. Butler.
Composing Event-B specifications – case-study experience.
In 10th International Conference on Software Composition,
volume 6708 of Lecture Notes in Computer Science, pages 100–115, 2011.

[26]
A. Gondal, M. Poppleton, and C. Snook.
Feature composition-towards product lines of Event-B models.
In 3rd International Workshop on Model-Driven Product Line
Engineering, volume 6698 of Lecture Notes in Computer Science, pages
18–25, 2009.

[27]
C. A. Gunter.
Semantics of Programming Languages: Structures and
MIT Press, Cambridge, Mass., Nov. 1992.

[28]
S. Hallerstede.
On the purpose of Event-B proof obligations.
In 1st International Conference on Abstract State
Machines, B and Z, ABZ, volume 5238 of Lecture Notes in Computer
Science, pages 125–138, 2008.

[29]
J. He and Q. Li.
A new roadmap for linking theories of programming and its
applications on GCL and CSP.
Science of Computer Programming, 162:3–34, 2018.

[30]
M. Hennessy.
The Semantics of Programming Languages.
Wiley, 1990.

[31]
T. S. Hoang, A. Iliasov, R. Silva, and W. Wei.
A survey on Event-B decomposition.
Electronic Communications of the EASST, 46:1–15, 2011.

[32]
C. A. R. Hoare.
An axiomatic basis for computer programming.
Communications of the ACM, 12(10):576–580, 1969.

[33]
C. A. R. Hoare.
Communicating sequential processes.
In The Origin of Concurrent Programming, pages 413–443.
Springer, 1978.

[34]
C. A. R. Hoare and H. Jifeng.
Unifying Theories of Programming.
Prentice Hall, 1998.

[35]
A. Iliasov, E. Troubitsyna, L. Laibinis, A. Romanovsky, K. Varpaaniemi,
D. Ilic, and T. Latvala.
Supporting reuse in Event-B development: Modularisation approach.
In 2nd International Conference on Abstract State Machines,
Alloy, B and Z, ABZ, volume 5977 of Lecture Notes in Computer Science,
pages 174–188, 2010.

[36]
Information Technology — Z Formal Specification Notation —
Syntax, Type System and Semantics.
ISO/IEC 13568:2002. International Organization for Standardization,
July 2002.

[37]
C. B. Jones.
The transition from VDL to VDM.
J. UCS, 7(8):631–640, 2001.

[38]
Y. Kesten and A. Pnueli.
Modularization and abstraction: The keys to practical formal
In 40th International Symposium on Mathematical Foundations of
Computer Science, MFCS, volume 9234 of Lecture Notes in Computer
Science, pages 54–71, 1998.

[39]
L. Lamport.
Specifying Systems: The TLA+ Language and Tools for Hardware
and Software Engineers.
Addison-Wesley, 2002.

[40]
P. G. Larsen and W. Pawlowski.
The formal semantics of ISO VDM-SL.
Computer Standards and Interfaces, 17(5):585–601, 1995.

[41]
K. R. M. Leino.
Dafny: An automatic program verifier for functional correctness.
In International Conference on Logic for Programming Artificial
Intelligence and Reasoning, volume 6355 of Lecture Notes in Computer
Science, pages 348–370, 2010.

[42]
S. Merz.
On the logic of TLA+.
Computing and Informatics, 22(3-4):351–379, 2012.

[43]
C. A. Middelburg.
VVSL: A language for structured VDM specifications.
Formal Aspects of Computing, 1:115–135, 1989.

[44]
C. Morgan, K. Robinson, and P. Gardiner.
On the Refinement Calculus.
Springer, 1988.

[45]
J. Morris.
A theoretical basis for stepwise refinement and the programming
Science of Computer Programming, 9(3):287–306, 1987.

[46]
T. Mossakowski, C. Maeder, and K. Lüttich.
The heterogeneous tool set, Hets.
In 13th International Conference on Tools and Algorithms for
the Construction and Analysis of Systems, TACAS, volume 4424 of Lecture Notes in Computer Science, pages 519–522, 2007.

[47]
P. D. Mosses, editor.
CASL Reference Manual, volume 2960 of Lecture Notes in
Computer Science.
Springer, 2004.

[48]
M. Oliveira, A. Cavalcanti, and J. Woodcock.
A UTP semantics for Circus.
Formal Aspects of Computing, 21(1-2):3–32, 2009.

[49]
UML Infrastructure Specification, v2.4.1.
Specification formal/2011-08-05, Object Management Group, August

[50]
UML Superstructure Specification, v2.4.1.
Specification formal/2011-08-06, Object Management Group, August

[51]
M. Poppleton.
The composition of Event-B models.
In 1st International Conference on Abstract State Machines, B
and Z, ABZ, volume 5238 of Lecture Notes in Computer Science, pages
209–222, 2008.

[52]
S. Reeves and D. Streader.
General refinement, part one: Interfaces, determinism and special
Electronic Notes in Theoretical Computer Science, 214:277–307,

[53]
S. Reeves and D. Streader.
General refinement, part two: Flexible refinement.
Electronic Notes in Theoretical Computer Science, 214:309–329,

[54]
B. Roscoe.
The Theory and Practice of Concurrency.
Prentice Hall, 1998.

[55]
D. Sannella and A. Tarlecki.
Specifications in an arbitrary institution.
Information and Computation, 76(2-3):165–210, 1988.

[56]
D. Sannella and A. Tarlecki.
Foundations of Algebraic Specification and Formal Software
Springer, 2012.

[57]
M. Schmalz.
The Logic of Event-B.
Technical Report 698, Department of Computer Science, ETH Zurich,

[58]
D. A. Schmidt.
Denotational Semantics: a methodology for language
Allyn and Bacon, 1986.

[59]
S. Schneider.
The B-method: An introduction.
Palgrave, 2001.

[60]
S. Schneider, H. Treharne, and H. Wehrheim.
The behavioural semantics of Event-B refinement.
Formal Aspects of Computing, 26:251–280, 2014.

[61]
D. S. Scott and C. Strachey.
Toward a mathematical semantics for computer languages.
Technical Monograph PRG-6, Oxford University Computing Laboratory,
Programming Research Group, 1971.

[62]
R. Silva and M. Butler.
Supporting reuse of Event-B developments through generic
In 11th International Conference on Formal Engineering
Methods, ICFEM, volume 5885 of Lecture Notes in Computer Science,
pages 466–484, 2009.

[63]
R. Silva and M. Butler.
Shared event composition/decomposition in Event-B.
In 9th International Symposium on Formal Methods for Components
and Objects, FMCO, volume 6957 of Lecture Notes in Computer Science,
pages 122–141, 2012.

[64]
G. Smith.
A fully abstract semantics of classes for Object-Z.
Formal Aspects of Computing, 7(3):289–313, May 1995.

[65]
G. Smith.
The Object-Z Specification Language.
Springer, 2012.

[66]
J. M. Spivey.
Understanding Z: a specification language and its formal
semantics, volume 3 of Cambridge Tracts in Theoretical Computer
Cambridge University Press, 1988.

[67]
A. Tarski.
The semantic conception of truth: and the foundations of semantics.
Philosophy and Phenomenological Research, 4(3):341–376, 1944.

[68]
S. Thompson.
Haskell: the craft of functional programming.
Addison-Wesley, 1999.

[69]
D. A. Watt.
Programming Language Syntax and Semantics.
Prentice Hall, 1991.

[70]
G. Winskel.
The Formal Semantics of Programming Languages.
MIT Press, February 1993.

[71]
J. B. Wordsworth.
Software Development with Z: a Practical Approach to Formal
Methods in Software Engineering.
Addison-Wesley, 1992.

§ APPENDIX

-signatures and signature morphisms define a category $\mathbf{Sign}_{\iEVT}$. The objects are signatures and the arrows are signature morphisms.

Let $\Sigma = \langle S, \Omega, \Pi, E, V\rangle$ be an -signature where $\langle S, \Omega, \Pi \rangle$ is a signature over , $\Sigma_{{\iFOPEQ}}$, the institution for first-order predicate logic with equality <cit.>. $E$ is a set of tuples of the form $(event \ name, \mapsto status )$ and $V$ is a set of sort-indexed variable names.

In a category, morphisms can be composed, their composition is associative and identity morphisms exist for every object in the category. We show that $\mathbf{Sign}_{{\iEVT}}$ preserves these three properties:

(a) Composition of ${\iEVT}$-signature morphisms:

-signature morphisms can be composed, the composition of $\sigma_S, \sigma_\Omega$ and $\sigma_\Pi$ is inherited from . Therefore, we only examine the composition of $\sigma_E$ and $\sigma_V$.

$\sigma_E$: Event names do not have a sort or arity, so the only restrictions are (1) on functions of the form $( \texttt{Init}\mapsto \texttt{ordinary})$ and (2) that the ordering in the status poset is preserved. In both of these cases the composition is well-defined for $\sigma_E$.

$\sigma_V$: Variable names are sort-indexed so $\sigma_V$ utilises $\sigma_S$ on these sorts.

\begin{align*}
\sigma_2(\sigma_1(v:s)) &= \sigma_2((\sigma_{1_{V}}(v): \sigma_{1_S}(s))) \\
&= \sigma_{2_{V}}(\sigma_{1_{V}}(v)): \sigma_{2_S}(\sigma_{1_S}(s))
\end{align*}

Let $\sigma_1: \Sigma_1 \rightarrow \Sigma_2$ and $\sigma_2: \Sigma_2 \rightarrow \Sigma_3$, then we prove that $\sigma_2 \circ \sigma_1$ is a morphism in the category of -signatures.

* For all $(e_1 \mapsto st_1 ) \in \Sigma_1.E_1$, $\sigma_1(e_1\mapsto st_1) \in \Sigma_2.E_2$ and for all $(e_2\mapsto st_2) \in \Sigma_2.E_2$,  $\sigma_2(e_2\mapsto st_2 ) \in \Sigma_3.E_3$. Therefore $\sigma_2(\sigma_1( e_1\mapsto st_1 )) \in \Sigma_3.E_3$ so
$$\forall ( e_1\mapsto st_1 ) \in \Sigma_1.E_1  \Rightarrow \sigma_2 \circ \sigma_1 (e_1 \mapsto st_1 ) \in \Sigma_3.E_3$$

* For all $(v_1:s_1) \in \Sigma_1.V_1$, $\sigma_1((v_1:s_1)) \in \Sigma_2.V_2$ and for all $(v_2:s_2) \in\Sigma_2.V_2$, $\sigma_2((v_2:s_2))  \in \Sigma_3.V_3$. Therefore $\sigma_2(\sigma_1((v_1:s_1))) \in \Sigma_3.V_3$ so

$$\forall (v_1:s_1) \in \Sigma_1.V_1\Rightarrow \sigma_2 \circ \sigma_1 ((v_1:s_1)) \in \Sigma_3.V_3$$

Therefore, -signature morphisms can be composed.

(b) Composition of ${\iEVT}$-signature morphisms is associative:

$$(\sigma_3 \circ \sigma_2) \circ \sigma_1 = \sigma_3 \circ (\sigma_2 \circ \sigma_1)$$

For $(e\mapsto st )\in \Sigma.E$:

\begin{align*}
\sigma_2 \circ \sigma_1( e\mapsto st ) &= \sigma_2(\sigma_1(e\mapsto st ))\\
\text{Then, by definition of }& \text{composition}\\
\sigma_3 \circ (\sigma_2 \circ \sigma_1)(e\mapsto st ) &= \sigma_3(\sigma_2(\sigma_1(e\mapsto st ))) \\
&= \sigma_3 \circ \sigma_2 \circ(\sigma_1(e\mapsto st ))\\
& = (\sigma_3 \circ \sigma_2) \circ \sigma_1( e\mapsto st )
\end{align*}

Similarly, for $(v:s) \in \Sigma.V$,
$$\sigma_3 \circ (\sigma_2 \circ \sigma_1)((v:s)) = (\sigma_3 \circ \sigma_2) \circ \sigma_1((v:s))$$

Therefore, the composition of -signature morphisms is associative.

(c) Identity morphisms for ${\iEVT}$-signatures:

For any -signature $\Sigma$, there exists an identity signature morphism $id_{\Sigma}: \Sigma \rightarrow \Sigma$.
$id_E$ and $id_V$ are such that $id_E(e\mapsto st ) = (e\mapsto st )$ and $id_V((v:s)) = (v:s)$. This morphism satisfies the following signature morphism condition
$$( e\mapsto st)\in \Sigma.E \Rightarrow id_E(e\mapsto st ) \in \Sigma.E \ \ \land \ \ (v:s) \in \Sigma.V \Rightarrow id_V(v:s) \in \Sigma.V$$

We have thus shown that $\mathbf{Sign}_{{\iEVT}}$ forms a category as instructed by the definition of an institution (Definition <ref>).

There is a functor $\mathbf{Sen}_{\iEVT}: \mathbf{Sign}_{\iEVT} \rightarrow \mathbf{Set}$ generating for each -signature $\Sigma$ a set of -sentences (objects in the category Set) and for each -signature morphism $\sigma: \Sigma_1 \rightarrow \Sigma_2$ (morphisms in the category $\mathbf{Sign}_{\iEVT}$) a function $Sen(\sigma): Sen(\Sigma_1) \rightarrow Sen(\Sigma_2)$ (morphisms in the category Set) translating -sentences.

$\mathbf{Sen}_{\iEVT}$ is a functor therefore it is necessary to map the -signature morphisms to corresponding functions over sentences. The functor maps morphisms to functions between sets of sentences respecting sort, arity and  events. The image of a signature $\Sigma_i$ ($i \in \mathbb{N}$) in $\mathbf{Sign}_{{\iEVT}}$ is an object $\mathbf{Sen}(\Sigma_i)$ in the category $\mathbf{Set}$. By the definition of the extension of the signature morphism to sentences <cit.>, the translation of the object $\mathbf{Sen}(\Sigma_1)$ coincides with an object in $\mathbf{Sen}(\Sigma_2)$ with sort, operation, predicate, event and variable names translated with respect to the signature morphism $\sigma: \Sigma_1 \rightarrow \Sigma_2$. Thus, the image of a morphism in $\mathbf{Sign}_{{\iEVT}}$ is a function $Sen(\sigma): Sen(\Sigma_1) \rightarrow Sen(\Sigma_2)$ in the category $\mathbf{Set}$.

Then we prove that $\mathbf{Sen}$ preserves the composition of -signature morphisms and identities as follows.

(a) Composition of ${\iEVT}$-sentence morphisms:

$$Sen(\sigma_2 \circ \sigma_1) = Sen(\sigma_2) \circ Sen(\sigma_1)$$

Let $\Sigma_i$ ($i = 1..4$) be -signatures and let $\sigma_1:\Sigma_1 \rightarrow \Sigma_2$ and $\sigma_2: \Sigma_3 \rightarrow \Sigma_4$ be -signature morphisms. Given an -sentence of the form $\langle e, \phi(\overline{x}, \overline{x}\prime)\rangle$, then by expanding each side of the following equivalence, since signature morphisms can be composed, we show that composition is preserved.

\begin{align*}
Sen(\sigma_2 \circ \sigma_1)(\langle e, \phi(\overline{x}, \overline{x}\prime)\rangle) &= Sen(\sigma_2) \circ Sen(\sigma_1) (\langle e, \phi(\overline{x}, \overline{x}\prime)\rangle)\\
\langle \sigma_2 \circ \sigma_1(e), \sigma_2 \circ \sigma_1(\phi(\overline{x}, \overline{x}\prime))\rangle &= Sen(\sigma_2)(\langle \sigma_1(e), \sigma_1(\phi(\overline{x}, \overline{x}\prime))\rangle)\\
\langle \sigma_2 (\sigma_1(e)), \sigma_2 (\sigma_1(\phi(\overline{x}, \overline{x}\prime)))\rangle &= \langle \sigma_2(\sigma_1(e)), \sigma_2(\sigma_1(\phi(\overline{x}, \overline{x}\prime)))\rangle
\end{align*}

Thus, composition is preserved.

(b) Preservation of identities:

Let $id_{\Sigma_1}: \Sigma_1 \rightarrow \Sigma_1$ be an identity -signature morphism as in Lemma <ref>. Since -signature morphisms already preserve identity and $Sen(id_{\Sigma_1})$ is the application of the identity signature morphisms to every element of the sentence, then the identities are preserved. We can illustrate this as follows. Given a $\Sigma_1$-sentence $\langle e, \phi(\overline{x}, \overline{x}\prime)\rangle$,

\begin{align*}
& Sen(id_{\Sigma_1}(\langle e, \phi(\overline{x}, \overline{x}\prime)\rangle)\\
&= \langle id_{\Sigma_1}(e), id_{\Sigma_1}(\phi(\overline{x}, \overline{x}\prime))\rangle\\
&= \langle e, \phi(\overline{x}, \overline{x}\prime)\rangle
\end{align*}

and so, identities are preserved.

Thus $\mathbf{Sen}_{{\iEVT}}$ is a functor.

For any -signature $\Sigma$ there is a category of -models $\mathbf{Mod}_{\iEVT}(\Sigma)$ where the objects in the category are -models and the arrows are -model morphisms.

We begin by describing -model morphisms and then prove that composition and identities are preserved.

In  a model morphism $h:A_1 \rightarrow A_2$ is a family of functions $h = \langle h_s:\lvert A_1\rvert _s \rightarrow \lvert A_2\rvert _s \rangle_{s \in S}$ which respects the sorts and arities of the operations and predicates. Recall from Definition <ref> that -models have the form $\langle A,L, R \rangle$, therefore -model morphisms are given by extending the corresponding -model morphisms for the $A$ component of the model to the initialising set $L$ and the relations in $R$.

Thus for each -model morphism $\mu : \langle A_1,L_1, R_1 \rangle \rightarrow \langle A_2,L_2, R_2 \rangle$ there is an underlying -model morphism $h: A_1 \rightarrow A_2$, and we extend this to the states in the set $L_1$ and in the relation $R_1$.  That is, for any element
$$\{x_1 \mapsto a_{1},...,x_n \mapsto a_{n}, x_1\prime \mapsto a_{1}\prime,...,x_n\prime \mapsto a_{n}\prime\} \in R_1.e$$
in $R_1$ there is

$$ \{x_1 \mapsto h(a_{1}),...,x_n \mapsto h(a_{n}),x_1\prime \mapsto h(a_{1}\prime),...,x_n\prime \mapsto h(a_{n}\prime)\} \in R_2.e $$

in $R_2$ where $x_1, \ldots, x_n, x_1\prime, \ldots, x_n\prime$ are variable names and their primed versions drawn from $V$. A similar construction follows for $L1$.
The composition of model morphisms, their associativity and identity derives from that of .

(a) Composition of ${\iEVT}$-model morphisms:

Let $M_i = \langle A_i,L_i, R_i \rangle$ be a model and $h_i : M_i \rightarrow M_{i+1}$ be an -model morphism where $i \in \mathbb{N}$. We can now show that the composition of -model morphisms is associative as follows:

We know that

$$(h_3 \circ h_2) \circ h_1(A_1)  =  h_3 \circ (h_2 \circ h_1)(A_1)$$
since model morphisms and thus their associativity for $A$ are inherited from .

Next, we consider $L_1$ and $R_1$ whose fundamental components are $\Sigma$-states (variable to value mappings). Signature morphisms on $\Sigma$-states follow the associated sort mappings in  and thus model morphisms on $\Sigma$-states follow model morphisms on $A$ as above. In this way, compositionality of model morphisms is associatve for $L_1$ and $R_1$.

(b) Identity morphism for ${\iEVT}$-models:

For any -model $M_i$ there exists an identity model morphism $h_{id} : M_i \rightarrow M_i$. If $M_i = \langle A_i,L_i, R_i\rangle$ then $h_{id}(M_i) = \langle A_i, L_i, R_i\rangle$

Thus $\mathbf{Mod}_{{\iEVT}}(\Sigma)$ forms a category.

For each -signature morphism $\sigma: \Sigma_1 \rightarrow \Sigma_2$ the -model reduct is a functor $\textbf{Mod}(\sigma)$ from $\Sigma_2$-models to $\Sigma_1$-models.

Recall that each $\Sigma$-State$_{A}$ is a set of variable-to-value mappings of the form

$$\{x_1 \mapsto a_{1}, \ldots ,x_n \mapsto a_{n}\}$$

where $x_1, \ldots, x_n \in \Sigma.V $ (Definition <ref>).

Let $M_2 = \langle A_2,L_2, R_2 \rangle$ be a $\Sigma_2$-model. Then the reduct $M_2\rvert _{\sigma}$ collapses the -model to only contain signature items supported by $\Sigma_1$ and consists of the tuple
$M_2\rvert _{\sigma} = \langle A_2\rvert _{\sigma}, L_2\rvert _{\sigma}, R_2\rvert _{\sigma} \rangle$ such that

* $A_2 \rvert_{\sigma}$ is the reduct of the -component of the -model along the -components of $\sigma: \Sigma \rightarrow \Sigma'$.

* $L_2\rvert _{\sigma}$ and $R_2\rvert _{\sigma}$ are based on the reduction of the states of $A_2$ along $\sigma$. In particular, given $e \in dom(E1)$ and $e \neq \texttt{Init}$ and $R_2.\sigma(e) \in R_2$

$$R_2.\sigma(e) = \{s_1, ..., s_m\} $$

where each $s_i$ is a $\Sigma_2$-state$_{A_2}$ ($1 \leq i \leq m$) is of the form

$$\{\sigma(x_1) \mapsto a_1,..., \sigma(x_n) \mapsto a_n, \sigma(x_1\prime) \mapsto a_1\prime,..., \sigma(x_n\prime) \mapsto a_n\prime\}$$

with $x_1,...,x_n \in \Sigma.V $ and $x_1\prime,...,x_n\prime \in \Sigma.V\prime$.

Then for each $e \in dom(E1)$, $e \neq \texttt{Init}$ and $R_2\rvert _{\sigma}.e \in R_2\rvert _{\sigma}$ there is

$$R_2\rvert_{\sigma}.e=\{s_1\rvert _{\sigma},..., s_m\rvert _{\sigma}\}$$

where each $s_i\rvert _{\sigma}$ ($1\leq i \leq m$) is of the form

$$\{x_1 \mapsto a_1, ..., x_n \mapsto a_n, x_1\prime \mapsto a_1\prime, ..., x_n\prime \mapsto a_n\prime\}$$

In order to prove that the model reduct is a functor, we show that it preserves composition and identities as follows:

(a) Preservation of composition for ${\iEVT}$-model reducts:

Our objective here is to show that the reduct of a composition of two -model morphisms is equal to the composition of the reducts of those -model morphisms.
Given -model morphisms $h_1: M_1 \rightarrow M_2$ and $h_2:  M_2 \rightarrow M_3$, then we show that

$$(h_2 \circ h_1)\rvert _{\sigma} = h_2\rvert _{\sigma} \circ h_1\rvert _{\sigma}$$

for some -signature morphism $\sigma: \Sigma \rightarrow \Sigma'$.
Given an -model of the form $M_1 = \langle A, L, R\rangle$ over $\Sigma$, then for any $R.e \in R$, as outlined above, of the form
$$\{x_1 \mapsto a_1 ,\ldots, x\prime_n \mapsto a\prime_n\}_e$$
Then $(h_2 \circ h_1)|_{\sigma}$ is defined as

$$(h_2 \circ h_1)\{\sigma(x_1) \mapsto a_1 ,\ldots, \sigma(x\prime_n) \mapsto a\prime_n\}_\sigma(e)$$

This is equal to

$$h_2 (\{\sigma(x_1) \mapsto h_1(a_1) ,\ldots, \sigma(x\prime_n) \mapsto h_1(a\prime_n)\}_\sigma(e)$$

Since -model morphisms can be composed, this is thus equal to $h_2\rvert _{\sigma} \circ h_1\rvert _{\sigma}$.

(b) Preservation of identities for ${\iEVT}$-model reducts:

The reduct of the identity is the identity.
Let $id_{M_2}$ be an identity $\Sigma_2$-morphism then $id_{M_2}\rvert _{\sigma}$ is an identity $\Sigma_1$-morphism $h_1$ defined by $h_1(R.e) = id_{M_2}\rvert _{\sigma} (R.e) = R.e$ for any $R.e \in R$ and $ e $ is an event other than .

For the components belonging to $A$ these proofs follow the corresponding proofs in .

There is a functor $\mathbf{Mod}_{\iEVT}$ yielding a category $\mathbf{Mod}(\Sigma)$ of -models for each -signature $\Sigma$, and for each -signature morphism $\sigma: \Sigma_1 \rightarrow \Sigma_2$ a functor $\mathbf{Mod}(\sigma)$ from $\Sigma_2$-models to $\Sigma_1$-models.

For each $\sigma: \Sigma_1 \rightarrow \Sigma_2$ in $\mathbf{Sign}_{\iEVT}$ there is an arrow in $\mathbf{Sign}_{\iEVT}^{op}$ going in the opposite direction. By Lemma 4, the image of this arrow in $\mathbf{Sign}_{\iEVT}^{op}$ is $\mathbf{Mod}(\sigma): \mathbf{Mod}(\Sigma_2) \rightarrow \mathbf{Mod}(\Sigma_1)$ in $\mathbf{Cat}$. By Lemma 3, the image of a signature in $\mathbf{Sign}_{\iEVT}$ is an object $\mathbf{Mod}(\Sigma)$ in $\mathbf{Cat}$. Therefore, domain and co-domain of the image of an arrow are the images of the domain and co-domain respectively.

(a) Preservation of composition:

$$\mathbf{Mod}(\sigma_2 \circ \sigma_1) = \mathbf{Mod}(\sigma_2) \circ \mathbf{Mod}(\sigma_1)$$

Let $\sigma_1: \Sigma_1 \rightarrow \Sigma_2$ and $\sigma_2: \Sigma_2 \rightarrow \Sigma_3$ be -signature morphisms and let $M_i = \langle A_i, L_i, R_i \rangle$ be an -model over $\Sigma_i$ and let $h_i$ be a $\Sigma_i$-model morphism with $i \in \{1,2,3\}$.

* $M_3\rvert _{\sigma_2 \circ \sigma_1} = (M_3\rvert _{\sigma_2})\rvert _{\sigma_1}$

By definition of reduct

$M_3\rvert _{\sigma_2} = \langle A_3, L_3, R_3 \rangle\rvert _{\sigma_2} = \langle A_2, L_2, R_2 \rangle = M_2$ .

$(M_3\rvert _{\sigma_2})\rvert _{\sigma_1} = M_2\rvert_{\sigma_1} = \langle A_2, L_2, R_2 \rangle\rvert _{\sigma_1} = \langle A_1, L_1, R_1 \rangle = M_1$.

By composition of signature morphisms $\sigma_2 \circ \sigma_1: \Sigma_1 \rightarrow \Sigma_3$, then
$$M_3\rvert _{\sigma_2 \circ \sigma_1}=\langle A_3, L_3, R_3 \rangle\rvert _{\sigma_2 \circ \sigma_1} = \langle A_1,L_1, R_1 \rangle = M_1$$

Therefore $M_3\rvert _{\sigma_2 \circ \sigma_1} = (M_3\rvert _{\sigma_2})\rvert _{\sigma_1}$

* $h_3\rvert _{\sigma_2 \circ \sigma_1} = (h_3\rvert _{\sigma_2})\rvert _{\sigma_1}$

Proof similar to above.

(b) Preservation of identities:

Let $id_{\Sigma_1}$ be an identity signature morphism as defined in Lemma <ref>. Since -signature morphisms already preserve identity and $Mod(id_{\Sigma_1})$ is the application of the identity signature morphisms to every part of the -model, the identities are preserved.

Pushouts exist in Sign$_{{\iEVT}}$.

Given two -signature morphisms $\sigma_1: \Sigma \rightarrow \Sigma_1$
and $\sigma_2 : \Sigma \rightarrow \Sigma_2$ a pushout is a triple
$(\Sigma', \sigma_1',\sigma_2')$ that satisfies the universal
property: for all triples $(\Sigma'', \sigma_1'',\sigma_2'')$ there
exists a unique morphism $u: \Sigma' \rightarrow \Sigma''$ such that
the diagram on the left below commutes. Our pushout construction
follows  for the elements that  has in common with
. In $\textbf{Sign}_{{\iEVT}}$ the additional elements are $E$
and $V$ as presented below.

(P0) at (90:2cm) $\Sigma$;
(P1) at (90+90:2.5cm) $\Sigma_1$ ;
(P2) at (90+2*90:2.5cm) $\Sigma'$;
(P3) at (90+3.75*72:2.5cm) $\Sigma_2$;
(P4) at (90+2*90:5cm) $\Sigma''$;
[commutative diagrams/.cd, every arrow, every label]
(P0) edge node [swap]$\sigma_1$ (P1)
(P1) edge node  $\sigma_1'$ (P2)
(P3) edge node[swap] $\sigma_2'$ (P2)
(P0) edge node $\sigma_2$ (P3)
(P1) edge node [swap]$\sigma_1''$ (P4)
(P3) edge node $\sigma_2''$ (P4)
(P2) edge[dashed] node $u$ (P4);

We base our constructions of the pushout in $E$ and $V$ on the canonical pushout in $\mathbf{Set}$.

* Set of functions of the form $($event name $\mapsto$ status$)$ in $E$:
The set of all event names in the pushout is the pushout in $\mathbf{Set}$ (disjoint union)
on event names only.  Then, the status of an event in the pushout is the supremum of all event statuses that are mapped to it, according to the ordering given in Definition <ref>.
Since -signature morphisms map $(\texttt{Init}\mapsto \texttt{ordinary})$ to $( \texttt{Init} \mapsto \texttt{ordinary})$ the pushout does likewise. The universality property for $E$ follows from that of $\mathbf{Set}$.

The canonical injectionsin $\mathbf{Set}$ for $E$ are denoted by $inl$ for inject left and $inr$ for inject right. Then, let $(e_1\mapsto status_1) = \sigma_1(e \mapsto status)$, $(e_2\mapsto status_2) = \sigma_2(e \mapsto status)$ and $status' = status_1 \sqcup status_2$ (where $\sqcup$ denotes the supremum).
Thus,Z the pushout in $E$ is given by the formula $E_1 \dot{\cup} E_2 / \sim$ where $\sim$ is the least equivalence relation such that

$$(inl(e_1)\mapsto status') \sim (inr(e_2)\mapsto status')$$

* Set of sort-indexed variable names $V$:
The set of sort-indexed variable names in the pushout is the pushout in  for the sort components and the pushout in $\mathbf{Set}$ for the variable names.
This is a similar construction to the pushout for operation names in  as these also have to follow the sort pushout.
Thus, the universality property for $V$ follows from that of $\mathbf{Set}$ and the  pushout for sorts.Thus the pushout in $V$ is given by the formula $V_1 \dot{\cup} V_2 / \sim$ where $\sim$ is the least equivalence relation such that
$$\sigma'_1 \circ \sigma_1(v:s) \sim \sigma'_2 \circ \sigma_2(v:s)$$
for $(v:s)\in \Sigma.V$.

Every pushout diagram in Sign$_{{\iEVT}}$ admits weak model amalgamation.

We decompose this proposition into two further sub-propositions:

For $M_1 \in \lvert\textbf{Mod}(\Sigma_1)\rvert$ and $M_2 \in \lvert\textbf{Mod}(\Sigma_2)\rvert$ such that $M_1\rvert _{\sigma_1} = M_2\rvert _{\sigma_2}$, there exists an -model (the amalgamation of $M_1$ and $M_2$) $ M' \in \lvert\textbf{Mod}(\Sigma')\rvert$ such that $M'\rvert _{\sigma'_1} = M_1$ and $M'\rvert _{\sigma'_2} = M_2$.

Given the -models $M \in \lvert \mathbf{Mod}(\Sigma)\rvert, M_1\in \lvert \mathbf{Mod}(\Sigma_1)\rvert, M2\in \lvert \mathbf{Mod}(\Sigma_2)\rvert$ and -signature morphisms $\sigma_1: \Sigma \rightarrow \Sigma_1, \sigma_2: \Sigma: \rightarrow \Sigma_2$ in the commutative diagram below.

(P0) at (90:4cm) $M' = \langle A',L',R'\rangle$;
(P1) at (90+72:5cm) $M_1 = \langle A_1,L_1,R_1\rangle$ ;
(P2) at (90+2*90:1cm) $M = \langle A,L,R\rangle$;
(P3) at (90+4*72:5cm) $M_2 = \langle A_2,L_2,R_2\rangle$;
[commutative diagrams/.cd, every arrow, every label]
(P0) edge node [swap] $Mod(\sigma_1')$ (P1)
(P1) edge node[swap]  $Mod(\sigma_1)$ (P2)
(P3) edge node$Mod(\sigma_2)$ (P2)
(P0) edge node $Mod(\sigma_2')$ (P3);

We compute the model amalgamation (following the corresponding pushout diagram in $\mathbf{Sign}$ as illustrated in Proposition <ref>) $M' = M_1 \otimes M_2$ which is of the form $\langle A', L', R' \rangle$ where
$A' = A_1 \otimes A_2$ is the
-model amalgamation of $A_1$ and $A_2$. We
construct the initialising set $L' = L_1 \otimes L_2$ by amalgamating the initialising sets $L_1$ and $L_2$ to
get the set of all possible combinations of variable mappings, while
respecting the amalgamations induced on variable names via the pushout

For example, suppose that the sort-indexed variable $x$ is in $\Sigma.V$. Then we can apply the -signature morphisms $\sigma_1: \Sigma \rightarrow \Sigma_1$ and $\sigma_2: \Sigma \rightarrow \Sigma_2$ to get $\sigma_1(x) = x_1 \in \Sigma_1.V$ and $\sigma_2(x) = x_2 \in \Sigma_2.V$.
From Proposition <ref>, we know that the pushout $ (\Sigma_1.V \; \cup \; \Sigma_2.V) /{}_{\sim}$ contains the variable name $x'$ such that $\sigma_1'(x_1) = \sigma_2'(x_2) = x' \in \Sigma'.V$. We follow this pushout construction in order to construct the corresponding model amalgamation. A model $M \in \lvert \mathbf{Mod}(\Sigma)\rvert$ contains an initialising set $L$ which, in turn, contains maplets of the form $x \mapsto a$ where $a$ is a sort-appropriate value for the variable $x$. In light of the -signature morphisms outlined above, we know that $M_1 \in \lvert \mathbf{Mod}(\Sigma_1)\rvert$ contains maplets of the form $x_1 \mapsto a_1$ and $M_2 \in \lvert \mathbf{Mod}(\Sigma_2)\rvert$ contains maplets of the form $x_2 \mapsto a_2$ where $a_1$ and $a_2$ are sort-appropriate values for $x_1$ and $x_2$ respectively. Then the amalgamation $M' \in \lvert \mathbf{Mod}(\Sigma) \rvert$ has the initialising set $L' = L_1 \otimes L_2$ which contains all maplets of the form $x' \mapsto a'$ where $a'$ is a sort-appropriate value for $x'$ drawn from $A'$ (the -amalgamation of $A_1$ and $A_2$). Note that initialising sets contain sets of variable-to-value mappings for all of the variables in the $V$ component of their signatures, as such, the amalgamation contains the above maplets in all possible combinations with those corresponding to any other variables that may be in the signature.

We construct the relation $R' = R_1 \otimes R_2$, which is the
amalgamation of $R_1$ and $R_2$, in a similar manner.
Specifically, starting from any $R.e = \{s_1,...,s_m\} \in R$ where $s_1,...,s_m$ are states of the form
$$\{x_1 \mapsto a_1,..., x_n\prime \mapsto a_n\prime\}$$

where $x_1,\ldots, x_n\prime$ are the variable names (and their primed versions drawn from $\Sigma.V$).
We construct the corresponding relation $R'.\sigma'(e)$ in $R'$ so that the diagram in Figure <ref> commutes.

In Figure <ref>, $h' = (h_1 + h_2)$ is the corresponding function over the carrier-sets in $M'$ obtained from , and $\sigma' = (\sigma_1' \; \circ \; \sigma_1)+(\sigma_2'\; \circ\; \sigma_2)$
is the mapping for variable and event names obtained from the corresponding construction in $\mathbf{Sign}_{\iEVT}$.

(P0) at (90:22cm)
$R'.\sigma'(e) = \{\sigma'(x_i) \mapsto h'(a_i)\} \in R'$;
(P1) at (70+72:22.5cm)
$R_1.\sigma_1(e) =\{\{\sigma_1(x_i) \mapsto h_1(a_i)\}\in R1$ ;
(P3) at (110+4*72:22.5cm)
$R_2.\sigma_2(e) =\{\sigma_2(x_i) \mapsto h_2(a_i1)\} \in R2$;
(P2) at (90:4cm)
$R.e =\{x_i \mapsto a_i\} \in R$;
[commutative diagrams/.cd, every arrow, every label]
(P0) edge node[swap] $Mod(\sigma_1')$ (P1)
(P1) edge node[swap] $Mod(\sigma_1)$ (P2)
(P3) edge node $Mod(\sigma_2)$ (P2)
(P0) edge node $Mod(\sigma_2')$ (P3);

The construction of $R' = R_1 \otimes R_2$, the amalgamation of $R_1$ and $R_2$.

For any two -model morphisms $f_1:M_{11} \rightarrow M_{12}$ in $\textbf{Mod}(\Sigma_1)$ and $f_2:M_{21} \rightarrow M_{22}$ in $\textbf{Mod}(\Sigma_2)$ such that $f_1\rvert _{\sigma_1} = f_2\rvert _{\sigma_2}$, there exists an -model morphism (the amalgamation of $f_1$ and $f_2$) called $f':M'_1 \rightarrow M'_2$ in $\textbf{Mod}(\Sigma')$, such that $f'\rvert _{\sigma'_1} = f_1$ and $f'\rvert _{\sigma'_2} = f_2$.

Given the -model morphisms $f_1$ and $f_2$ and their common reduct $f_0$, we construct $f'$ so that the following diagram commutes:

(P0) at (90:4cm) $f' : M_1' \rightarrow M_2'$;
(P1) at (90+72:5cm) $f_1 : M_{11} \rightarrow M_{12}$ ;
(P2) at (90+2*90:1cm) $f_0 : M_{01} \rightarrow M_{02}$;
(P3) at (90+4*72:5cm) $f_2 : M_{21} \rightarrow M_{22}$;
[commutative diagrams/.cd, every arrow, every label]
(P0) edge node [swap] $Mod(\sigma_1')$ (P1)
(P1) edge node[swap]  $Mod(\sigma_1)$ (P2)
(P3) edge node$Mod(\sigma_2)$ (P2)
(P0) edge node $Mod(\sigma_2')$ (P3);

Since each -model has a  model as its first component, each of the -model morphisms $f_0$, $f_1$, $f_2$ and $f'$ must have an underlying -model morphism, which we denote $f_0^-$, $f_1^-$, $f_2^-$ and $f^{'-}$ respectively. To build the amalgamation for -models we must show how to extend these to cover the data states of the -models. This -model morphism follows the underlying -model morphism on sort carrier sets for the values in the data states.

Given $R.e \in R$, suppose we start with any $f_0$-maplet of the form

\begin{align*}
& \{\ldots,\{x_1 \mapsto a_1, \ldots, x_n \mapsto a_n\}, \ldots\}\\
& \mapsto \{\ldots,\{ x_1 \mapsto f_0^-(a_{1}), \ldots, x_n \mapsto f_0^-(a_{n})\},\ldots\}_e \;\in\; f_0
\end{align*}

where $f_0^-$ is the underlying map on data types from the -model morphism.

Then the original two functions in $f_1$ and $f_2$ must have maplets of the form

\begin{align*}
& \{\ldots,\{\sigma_1(x_1) \mapsto h_1(a_1), \ldots, \sigma_1(x_n\prime) \mapsto h_1(a_n\prime)\}, \ldots\}\\
& \mapsto \{\ldots,\{ \sigma_1(x_1) \mapsto f_1^-(h_1(a_{1})), \ldots, \sigma_1(x_n\prime) \mapsto f_1^-(h_1(a_{n}\prime))\},\ldots\} \;\in\; f_1
\end{align*}

\begin{align*}
& \{\ldots,\{\sigma_2(x_1) \mapsto h_2(a_1), \ldots, \sigma_2(x_n\prime) \mapsto h_2(a_n\prime)\}, \ldots\}\\
& \mapsto \{\ldots,\{ \sigma_2(x_1) \mapsto f_2^-(h_2(a_{1})), \ldots, \sigma_2(x_n\prime) \mapsto f_2^-(h_2(a_{n}\prime))\},\ldots\} \;\in\; f_2
\end{align*}

where $f_1^-$ and $f_2^-$ are again the data type maps from the underlying -model morphism, and $h_1$ and $h_2$ are obtained from $Mod(\sigma_1)$ and $Mod(\sigma_2)$.

We then can construct the elements of the -model morphism $f'$, which is the amalgamation of $f_1$ and $f_2$, as $f'$-maplets of the form:

\begin{align*}
& \{\ldots,\{\sigma'(x_1) \mapsto h'(a_1), \ldots, \sigma'(x_n\prime) \mapsto h'(a_n\prime)\}, \ldots\}\\
& \mapsto \{\ldots,\{ \sigma'(x_1) \mapsto f'^-(h'(a_{1})), \ldots, \sigma'(x_n\prime) \mapsto f'^-(h'(a_{n}\prime))\},\ldots\} \;\in\; f'
\end{align*}

As before, $h' = (h_1 + h_2)$ is the corresponding function over the carrier-sets in $M'$ obtained from , and $\sigma' = (\sigma_1' \; \circ \; \sigma_1)+(\sigma_2'\; \circ\; \sigma_2)$ is
the mapping for variable and event names obtained from the corresponding construction in $\mathbf{Sign}$.  Here $f^{'-} = f_1^-+f_2^-$ is the model morphism amalgamation from the corresponding diagram for model morphisms in , which ensures that the data states are mapped to corresponding states in the model $M_2'$.

(P0) at (90:22cm) $R'.\sigma'(e) = \{\ldots,\{\sigma'(x_1) \mapsto h'(a_1), \ldots, \sigma'(x_n\prime) \mapsto h'(a_n\prime)\}, \ldots\} \in R'$;
(P1) at (90+72:22.5cm) $R_1.\sigma_1(e) =\{\ldots,\{\sigma_1(x_1) \mapsto h_1(a_1), \ldots, \sigma_1(x_n\prime) \mapsto h_1(a_n\prime)\}, \ldots\}\in R1$ ;
(P2) at (90+2*90:11cm) $R.e =\{\ldots,\{x_1 \mapsto a_1, \ldots, x_n\prime \mapsto a_n\prime\}, \ldots\} \in R$;
(P3) at (90+4*72:22.5cm) $R_2.\sigma_2(e) =\{\ldots,\{\sigma_2(x_1) \mapsto h_2(a_1), \ldots, \sigma_2(x_n\prime) \mapsto h_2(a_n\prime)\}, \ldots\} \in R2$;
[commutative diagrams/.cd, every arrow, every label]
(P0) edge node[swap] $Mod(\sigma_1')$ (P1)
(P1) edge node[swap] $Mod(\sigma_1)$ (P2)
(P3) edge node $Mod(\sigma_2)$ (P2)
(P0) edge node $Mod(\sigma_2')$ (P3);