# SourceP: Detecting Ponzi Schemes on Ethereum with Source Code

Pengcheng Lu1,Liang Cai 2, Keting Yin1 1School of Software Technology,
Zhejiang University, China
2College of Computer Science and Technology, Zhejiang University, China
<EMAIL_ADDRESS>
###### Abstract

As blockchain technology becomes more and more popular, a typical financial
scam, the Ponzi scheme, has also emerged in the blockchain platform Ethereum.
This Ponzi scheme deployed through smart contracts, also known as the smart
Ponzi scheme, has caused a lot of economic losses and negative impacts.
Existing methods for detecting smart Ponzi schemes on Ethereum mainly rely on
bytecode features, opcode features, account features, and transaction behavior
features of smart contracts, which are unable to truly characterize the
behavioral features of Ponzi schemes, and thus generally perform poorly in
terms of detection accuracy and false alarm rates. In this paper, we propose
SourceP, a method to detect smart Ponzi schemes on the Ethereum platform using
pre-trained models and data flow, which only requires using the source code of
smart contracts as features. SourceP reduces the difficulty of data
acquisition and feature extraction of existing detection methods.
Specifically, we first convert the source code of a smart contract into a data
flow graph and then introduce a pre-trained model based on learning code
representations to build a classification model to identify Ponzi schemes in
smart contracts. The experimental results show that SourceP achieves 87.2%
recall and 90.7% F-score for detecting smart Ponzi schemes within Ethereum’s
smart contract dataset, outperforming state-of-the-art methods in terms of
performance and sustainability. We also demonstrate through additional
experiments that pre-trained models and data flow play an important
contribution to SourceP, as well as proving that SourceP has a good
generalization ability.

###### Index Terms:

blockchain, Ethereum, smart contract, Ponzi scheme, pre-trained model

##  I Introduction

Blockchain technology is rapidly evolving as an open ledger of recorded
transactions maintained in a distributed network of mutually untrusted peers
(i.e., peer-to-peer network), where each peer verifies transactions through a
consensus protocol [1, 2, 3, 4]. Blockchain has now developed applications in
areas such as the Internet of Things [5], voting systems [6], authentication
[7], ledgers [3], disaster relief [8], healthcare [9], and edge computing
[10], which have attracted significant interest from industry and academia
[11]. Also, blockchain has become a common infrastructure for the emerging
metaverse and Web3, and DeFi, DAO, and Non-Fungible Tokens developed from
blockchain technology are becoming more and more popular [12].

Ethereum [13] is currently the most popular public blockchain platform with
smart contract functionality [14]. Ethereum handles peer-to-peer contracts
through the cryptocurrency Ether(ETH) and can store data, run smart contracts,
and share information globally. First proposed by Nick Szabo in the mid-1990s
[15], smart contracts contain contractual terms that will be automatically
executed when predefined conditions are met, stored, replicated, and updated
in a distributed blockchain. The combination of blockchain technology and
smart contracts makes the dream of a “peer-to-peer marketplace” come true,
which means that there will be no third-party intervention in transactions
between buyers and suppliers via smart contracts in a blockchain marketplace
[16].

Smart contracts on the Ethereum platform are Turing-complete, and through
Turing-complete smart contracts, users can not only trade in cryptocurrency
but also perform arbitrary actions on the blockchain [17]. Because of this,
decentralized applications (DApps) [18, 19] consisting of smart contracts are
currently growing rapidly, such as CryptoKitties [20] and IDEX [21]. Yet at
the same time, smart contracts have given a new opportunity for the spread of
Ponzi schemes [22].

Born 150 years ago, Ponzi schemes are a classic financial fraud that lures new
users in with the promise of high profits, with the core mechanism of
compensating the investors and creators who joined before with the investments
of new investors, creating no value themselves [23]. Once no new investors
join, the Ponzi scheme quickly collapses, new investors who are not
compensated lose their money, and the scam makers and early participants
receive illegal income. Smart contracts allow the creators of Ponzi schemes to
remain anonymous, while their immutability makes them extremely difficult to
change after being deployed to the blockchain, the feature that criminals
exploit to deploy scams on smart contract platforms like Ethereum [24]. Such
Ponzi schemes deployed on smart contracts are called smart Ponzi schemes.
Ponzitracker [25] found close to $3 billion amount of Ponzi schemes in 2022,
related to blockchain-based cryptocurrencies. The recent smart Ponzi scheme
event on the Forsage website involved more than $300 million [26]. The danger
of financial fraud is so serious that reducing smart Ponzi schemes is
imminent. Meanwhile, smart contracts are the building blocks of DApps, and if
individual smart contracts in DApps are Ponzi schemes, then the DApp may also
be dangerous. Therefore, detecting whether smart contracts deployed in
Ethereum are smart Ponzi schemes and flagging them are important to prevent
financial fraud and maintain the healthy development of DApps and blockchain
platforms.

Figure 1: Flowchart of our method.

Figure 2: Flowchart of the traditional method.

To the best of our knowledge, the existing methods for detecting smart Ponzi
schemes fall into three main categories; the first category of methods uses
bytecode or opcodes from smart contracts as features to train classifiers or
perform static analysis [27, 22]; the second category of methods uses the
transaction behavior features of smart contracts [28, 29]; the third category
of methods uses both opcodes features and account features to train the model
[4, 30, 31]. However, these three methods face some limitations. Firstly,
bytecode and opcode features lack interpretability, and adding or removing
some opcodes in smart contracts can be easily done to circumvent detection.
Second, it is also difficult to accurately locate the fraudster on the
anonymous Ethereum platform, so it is quite difficult to collect the
fraudster’s transaction behavior characteristics and account characteristics.
Third, static analysis methods suffer from recognition lag and rely on expert
rules. Finally, in the context of rapid updates to smart contracts, the
sustainability and performance of currently available methods for detecting
new smart Ponzi schemes have decreased significantly. So we consider using
other features to detect Ponzi schemes, such as smart contract source code,
which no one has considered before.

Our Method. To address these challenges, we propose a smart Ponzi scheme
detection approach based on pre-trained models and data flow called SourceP.
Pre-trained models in current natural language processing (NLP) techniques
have facilitated many tasks [32, 33, 34], thus, it is reasonable to explore
the great potential of pre-trained models in smart Ponzi scheme detection.
Since smart contracts on Ethereum are typically written in Solidity [35, 36],
SourceP will detect Ponzi schemes on smart contracts written in the Solidity
language.

SourceP embodies a key innovation point, namely the use of only the source
code of smart contracts as a feature. Figure 2 and Figure 2 show the
significant differences between existing traditional methods and our method in
detecting smart Ponzi schemes through flowcharts. As can be seen from the
comparison of the two figures, our approach omits to obtain the bytecode,
transaction, and account information of the smart contract, which reduces the
amount of data required while avoiding the various problems associated with
too many features. The specific implementation steps of SourceP can be seen in
Figure 4 and Figure 5. First, the smart contract source code is converted into
a data flow, then the source code information is fed into the pre-trained
model together with the data flow representing variable dependencies, and
finally, the identification results of the smart contract Ponzi scheme are
output and evaluated. Ultimately, we find that SourceP outperforms previous
methods in smart Ponzi scheme detection.

The main contributions are summarized as follows:

  * •

We propose a method, SourceP, to automatically detect Ponzi schemes in smart
contracts. To the best of our knowledge, SourceP is the first method to detect
smart Ponzi schemes using only the source code of smart contracts as features.
It introduces a pre-trained model for learning code representations and uses
the code semantic information provided by the data flow converted from the
source code for detection.

  * •

We conducted extensive experiments to demonstrate that SourceP outperforms the
state-of-the-art in detecting smart Ponzi schemes in terms of performance and
sustainability under the same conditions, and has a good generalization
ability.

  * •

We have exposed the dataset and source
code111https://github.com/Lpover/SourcePof this study for other researchers to
replicate our methods and evaluation to facilitate future research in this
direction.

##  II Background

###  II-A Ethereum and Smart contract

Ethereum is the first open-source public blockchain platform that supports
advanced and custom smart contracts with the help of a Turing-complete virtual
machine called Ethereum Virtual Machine (EVM) [37, 38]. EVM is the environment
in which smart contracts run, and each node in the Ethereum network runs an
implementation of EVM and executes the same instructions. Smart contracts are
written in languages such as Solidity and Serpent [39], and then the smart
contract code is compiled into EVM bytecode and deployed on the blockchain for
execution. Once the smart contract is deployed on the blockchain, the
corresponding bytecode and creation transactions are permanently stored on the
blockchain. Ethereum is now becoming the most popular platform for smart
contract development and can be used to design various types of decentralized
applications (DApps) that can be used for digital rights management,
crowdfunding, and gambling [14].

###  II-B Ponzi schemes on smart contract

The “Ponzi scheme” is a fraudulent investment scam that promises high rates of
return with little risk to the investor. Ponzi schemes create returns for
early investors by acquiring new investors. It is similar to a pyramid scheme
in that it is based on using new investors’ money to pay off early investors.
Both Ponzi schemes and pyramid schemes eventually bottom out when the influx
of new investors dries up and there is not enough money to turn around. Then
such scams simply fall apart and all those who have not yet recouped their
investments never get them back. Smart contracts provide a perfect breeding
ground for the modern fraudster. Whereas traditional financial fraudsters need
to worry about the law, third-party institutions, and their public image,
smart contracts don’t have the same problems.

Ponzi schemes on the blockchain have proliferated. Vasek et al. [40] analyzed
the supply and demand of bitcoin-based Ponzi schemes and identified 1780
different Ponzi schemes. Chainalysis [41] investigated cryptocurrency crimes
from 2017 to 2019 and found that 92% of cryptocurrency scams were Ponzi
schemes. Ponzi schemes on Ethereum are packaged as investment projects or
gambling games that promise huge returns to those who invest. Some large-scale
Ponzi schemes even build sophisticated websites and run aggressive marketing
campaigns to attract investors [26, 42]. It is difficult for investors with
little knowledge of blockchain to distinguish the true nature of smart
contracts that are disguised as high-yield investment schemes [27].

Bartoletti et al. [24] found that from August 2015 to May 2017, 191 smart
Ponzi schemes active on Ethereum had collected nearly $500,000 from more than
2,000 different users. They specifically analyzed 184 real smart Ponzi schemes
on Ethereum and classified smart Ponzi schemes into four types, chained-
shaped, tree-shaped, waterfall as well and handover, most of which are
chained-shaped with 82% of the total, while the other types have only 2% of
the total and the rest are The remaining are unclassified other types.

###  II-C Smart Ponzi Scheme Case

Figure 3 shows an example of a smart Ponzi scheme, a Chain-shaped scheme of
smart Ponzi source code fragment written by Roan [43]. Each time a new
investor participates in this smart Ponzi scheme, the $join()$ function is
called and then adds the new user to the list of investors with their
investment amount, and then transfers 10% of the investment amount to the
owner of the smart contract. Then, in a first come, first served order, if the
total amount of the pool is already more than twice the amount invested by the
first investor who has not been repaid, then he is compensated with twice the
amount invested in Ether.

Roan said of the Ponzi scheme, “That’s a complete lie, but enough to sucker
someone in.” [44]

Figure 3: Source code fragment of a smart Ponzi scheme.

###  II-D Data Flow

The data flow is a graph [45], which is also called a data flow graph (DFG),
and it is a graph that represents the dependencies between variables in a
code, where the nodes represent the variables and the edges represent the
sources of the values of each variable. Data flow graphs are very useful in
code analysis tasks [46, 47, 48]. Unlike abstract syntax tree (AST), data flow
has the same structure under different abstract syntaxes of the same source
code, and such a structure provides critical code semantic information for
code understanding. Moreover, dataflow has a simpler structure compared to
AST, which is more efficient when used in models. So SourceP will use the
dataflow graph as the input to the model. How to extract the dataflow from the
source code will be described in Section III-A.

###  II-E Pre-trained model

Pre-trained models can benefit a variety of downstream tasks by storing
knowledge into huge parameters and fine-tuning them on specific tasks, the
rich knowledge implicit in huge parameters has been extensively demonstrated
through experimental validation and empirical analysis [49]. Pre-trained
models such as BERT [50], ELMo [51], GPT [52], and XLNet [53] have been
successful on various tasks. Serval pre-trained models for learning code
representations are being applied, such as CodeBERT [54], CuBERT [55], GPT-C
[56], and Code-GPT [57]. SourceP uses GraphCodeBERT [45], a pre-trained model
for learning code representations trained on the CodeSearchNet [58] dataset,
as the main part of the model. The specific method of the pre-trained model
used by SourceP will be described in Section III.

(a) Partial source code in a smart Ponzi scheme

(b) Parse into AST

(c) Identify variable sequence in AST

(d) Data flow graph

Figure 4: The phase of input normalization, i.e., the process of converting
source code into data flow. (a) source code fragment of smart Ponzi scheme;
(b) conversion of source code into abstract syntax tree (AST); (c)
identification of variable sequences in abstract syntax tree (AST); (d)
generation of data flow graph by variable sequences.

##  III OUR METHOD

Method overview. Our method is divided into two main phases: 1) the input
normalization phase, which converts the source code of smart contracts into
AST and DFG; 2) the smart Ponzi scheme detection phase, which feeds the source
code and DFG into a pre-trained model and outputs the final detection results.
In the following, the first two subsections describe the details of each phase
in detail. The next subsection deals with the functions used to incorporate
the DFG into the Transformer. The last subsection is a detailed description of
the three pre-training tasks of the pre-trained model.

###  III-A Data Flow Graph Generation

Source code to AST. First, we have the source code
$SC=\left\\{sc_{1},sc_{2},\ldots,sc_{n}\right\\}$, then we convert the source
code into abstract syntax trees (ASTs). Here we need to use a tool called
tree-sitter [59], which can build a source code file into an AST. However, the
tree-sitter does not provide official Solidity language support, so we need to
use tree-sitter-solidity [60] to convert the Solidity language source code to
AST. This tool contains a grammar for tree-sitter which major inspiration and
some structures have been taken from tree-sitter-javascript [61]. AST includes
the syntax information of the code, and the leaf nodes in the tree are used to
identify the sequence of variables that are denoted as
$Var=\\{v_{1},v_{2},...,v_{n}\\}$.

AST to DFG. The data flow is a graph, so we can think of each variable in the
AST as a node. The edge connecting two nodes is denoted as
$\varepsilon=\left\langle v_{i},v_{j}\right\rangle$, which means that the
value of the $j$-th variable comes from the $i$-th variable. The set of all
directed edges in the graph is denoted as
$Edge=\left\\{\varepsilon_{1},\varepsilon_{2},\ldots,\varepsilon_{n}\right\\}$.
So the final data flow graph is represented as $\mathcal{G}(SC)=(Var,Edge)$,
this is the DFG we have constructed to represent the dependencies between
variables of the source code. Figure 4 shows the process of converting the
smart Ponzi scheme source code to AST and DFG.

###  III-B Model Structure

In this section, we will describe the model structure of SourceP in detail.
Our method primarily follows GraphCodeBert [45], so the model architecture
follows BERT [50] and the multi-layer bidirectional Transformer [62] is the
backbone of the model. Figure 5 shows the structure of the whole model.

The input to the model is the data flow graph converted from the source code,
since the detection task is different, the paired comments of the input
GraphCodeBert do not need to be considered. We modified the input by following
Peculiar’s [63] method. The difference is that Peculiar uses a crucial data
flow graph (CDFG) that retains only the data flow of key nodes as input to the
model, but we still choose to use the DFG as input to the model. This is
because Peculiar is designed to detect reentrant vulnerabilities in smart
contracts and only cares about the dependencies of functions related to
reentrancy vulnerabilities, while CDFG can remove redundant data flow
information. But the case of smart Ponzi schemes is more complex and it may
lurk in any function and variable, so it is necessary to use DFG as the input
to the model.

So the input to the model is a sequence $X=\\{[CLS],SC,[SEP],Var\\}$. Where
$[CLS]$ is a special classification token and $[SEP]$ is a special token used
to split the two different data types. The remaining two segments in $X$,
$SC=\left\\{sc_{1},sc_{2},...,sc_{n}\right\\}$ is the collection of source
code and $Var=\\{v_{1},v_{2},...,v_{n}\\}$ is the set of variables of data
flow graph $\mathcal{G}(SC)=(Var,Edge)$.

Figure 5: SourceP’s model structure.

Then the sequence $X$ will be converted to the input vector $W^{0}$. For each
token in $X$, the corresponding token and position embedding are summed to
construct its input vector. We use a special position embedding for all
variables in $X$ as a way to indicate that these variables are nodes in the
data flow. The model then uses the input vector $W^{0}$ to contextualize the
representation through $N$ transformer layers
$W^{n}=transformer_{n}(W^{n-1}),n\in[1,N]$. In our model, the value of $N$ is
12. The construction of each transformer layer is the same, and $U^{n}$ is
obtained by first applying a multi-headed self-attention operation[62] and
then applying a Layer Normalization operation. The feed-forward layer and a
Layer Normalization operation are then used on $U^{n}$. This way we get the
output $W^{n}$ of the $n$-th layer from the input $W^{n-1}$. Here is the
calculation for each transformer layer.

$U^{n}=LayN(MulA(W^{n-1})+W^{n-1})$ (1)

$W^{n}=LayN(FeeF(U^{n})+U^{n})$ (2)

Where $LayN$ means a Layer Normalization operation, $MulA$ means a multi-
headed self-attention mechanism and $FeeF$ is a two-layer feed-forward
network. In the $n$-th transformer layer, the multi-headed self-attention
operation computes the $\hat{U}^{n}$.

$Q_{i}=W^{n-1}P_{i}^{Q},\>K_{i}=W^{n-1}P_{i}^{K},\>V_{i}=W^{n-1}P_{i}^{V}$ (3)

$head_{i}=Softmax(\dfrac{Q_{i}{K_{i}}^{T}}{\sqrt{d_{k}}}+M)V_{i}$ (4)

$\hat{U}^{n}=[head_{1};...;head_{m}]{P_{n}}^{O}$ (5)

Where the output $W^{n-1}\in\mathbb{R}^{|X|\times d_{h}}$ of the previous
layer is linearly projected onto a triplet of queries, keys, and values using
the parameters $\begin{aligned}
P_{i}^{Q}\text{,}P_{i}^{K}\text{,}P_{i}^{V}\in\mathbb{R}^{d_{h}\times
d_{k}}\end{aligned}$ and $d_{k}$ is the dimension of a head.
$M\in\mathbb{R}^{|I|\times|I|}$ is a mask matrix, $M_{\textit{ij}}$ is 0 if
the $i$-th token is allowed to participate in the $j$-th token, otherwise it
is $\text{-}\infty$. And $P_{n}^{O}\in\mathbb{R}^{d_{h}\times d_{h}}$ is the
model parameters.

The model finally outputs the predicted label $\hat{y}$ through a linear
classifier and the $Softmax$ function.

$\hat{y}=\textit{Softmax}(\hat{U}^{n})$ (6)

###  III-C Graph-guided masked attention

In order to incorporate the structure of the data flow graph into the
Transformer, GraphCodeBERT [45] proposed this function. The masked attention
function avoids the key $k_{i}$ that the query $q_{j}$ focuses on by changing
the attention score ${q}_{j}^{T}k_{i}$ to $\text{-}\infty$ so that the
attention weight becomes 0 after using the softmax function. To represent
dependencies between variables, a node-query $q_{v_{i}}$ is allowed to attend
to on a node-key $k_{v_{j}}$ if there is a direct edge from node $v_{j}$ to
node $v_{i}$ where $\left\langle v_{j},v_{i}\right\rangle\in Edge$ or if
$i=j$. otherwise, attention is masked by adding $\text{-}\infty$ to the
attention score. To represent the relationship between source code tokens and
data flow nodes, we first define a set $Edge^{{}^{\prime}}$ where $\langle
v_{i},sc_{j}\rangle/\langle sc_{j},v_{i}\rangle\in Edge^{{}^{\prime}}$ if the
variable $v_{i}$ is identified from the source code token $sc_{j}$. Then, we
allow node $q_{v_{i}}$ and code $k_{sc_{j}}$ to attend each other when and
only when $\langle v_{i},sc_{j}\rangle/\langle sc_{j},v_{i}\rangle\in
Edge^{{}^{\prime}}$. We use the following graph-guided masked attention matrix
as the mask matrix $M$ in (4).

$M_{ij}=\begin{cases}0&\text{if }~{}q_{i}\in\\{[CLS],[SEP]\\}\\\
&\text{or}~{}q_{i},k_{j}\in P\cup SC\\\ &\text{or}~{}\langle
q_{i},k_{j}\rangle\in Edge\cup Edge^{\prime}\\\
-\infty&\text{otherwise}\end{cases}$ (7)

###  III-D Pre-Training Tasks

Masked Language Modeling. The task follows Devlin et al.[50] to apply a Masked
Language Modeling (MLM) pre-training task. In particular, we randomly sampled
15% of the tokens from the source code and paired annotations. We replace them
with a [MASK] token 80% of the time, replace them with random tokens 10% of
the time, and leave them unchanged 10% of the time. The goal of MLM is to
predict the original tokens of these sampled tokens, which is effective in
previous work [50, 64, 54]. In particular, if the source code context is not
sufficient to infer the masked code tokens, the model can make use of the
annotation context, encouraging the model to unify the natural language and
programming language representations.

Data Flow Edges Prediction. The purpose of this task is to learn
representations from the data flow. The motivation is to encourage models to
learn structure-aware representations that encode “where the value comes from”
relationships in order to better understand the code. In particular, we
randomly extract 20% of the nodes $Var_{s}$ in the data flow, mask the direct
edges connecting these extracted nodes by adding $\text{-}\infty$ to the
masking matrix, and then predict the $Edge_{\textit{mask}}$ of these masked
edges. Formally, the pre-training objective of the task is calculated as (8),
where $Edge_{\textit{sc}}=Var_{s}\times Var\cup Var\times Var_{s}$ is the set
of candidates for edge prediction, $\delta(e_{ij}\in Edge)$ is 1 if
$\left\langle v_{i},v_{j}\right\rangle\text{}\in Edge$ otherwise 0. The
probability $p_{e_{ij}}$ of the existence of an edge from the $i$-th node to
the $j$-th node is calculated by dot product according to the $Sigmoid$
function, using the representation of two nodes in the model. To balance the
positive-negative ratio of the examples, we sampled the same number of
negative and positive samples of $Edge_{\textit{mask}}$.

$\begin{split}loss_{EdgePred}=-\sum_{e_{ij}\in
Edge_{\textit{sc}}}[\delta(e_{ij}\in Edge_{mask})logp_{e_{ij}}\\\
+(1-\delta(e_{ij}\in Edge_{mask}))log(1-p_{e_{ij}})]\end{split}$ (8)

Node Alignment. The purpose of this task is to align the representation
between source code and data flow, which is similar to data flow edge
prediction. Instead of predicting the edges between nodes, we predict the
edges between code tokens and nodes. The motivation is to encourage the model
to align variables and source code to the data flow.

##  IV Experiments

To evaluate our method, we designed experiments to answer the following
research questions (RQs):

  * •

RQ1: How well does SourceP perform in detecting smart Ponzi schemes by relying
only on source code features, and how do its precision, recall, and F-score
compare to current state-of-the-art methods?

  * •

RQ2: How sustainable is SourceP in detecting smart Ponzi schemes?

  * •

RQ3: How do SourceP’s pre-training tasks and data flow affect detection
results?

  * •

RQ4: How well does SourceP generalization ability in detecting smart Ponzi
schemes?

###  IV-A Experiments Setting

Datasets. We used the Ponzi Contract Datasets provided by the XBlock platform
[4], a dataset that crawls 6,498 smart contracts on Etherscan [65], and
manually read the source code pairs to classify them with reference to the
methods used in some previous studies [24, 30], of which 318 smart contracts
were manually marked as Ponzi smart contracts and the rest were manually
marked as non-Ponzi smart contracts. We retained the source code in the
dataset, along with the corresponding serial number of idx and the label. If
the value of the label is 1 it means it is a smart Ponzi scheme, if it is 0 it
is not.

Evaluation metrics. For the experiments in the paper, we will use common
precision, recall, and F-score to evaluate the performance of the model.

Parameter settings. In the fine-turning step, we set the code length to 256,
data flow length to 64, train batch size to 1, eval batch size to 32, learning
rate to 2e-5, and used the Adam optimizer to update the model parameters.
Depending on the experiment, epochs were set to 3, 5, or 10. Because the
dataset has fewer positive category samples in some tasks, we set the
thresholds from 0.5 to 0.15 and 0.003, which allows the model to be more
inclined to predict positive samples that would otherwise be judged as
negative categories.

Implementation details. All the experiments were run on a computer with two
Intel(R) Xeon(R) Silver 4314 CPUs at 2.4GHz, one GPU at NVIDIA A40 or two GPUs
at NVIDIA A30, and 256GB of Memory.

###  IV-B Results Summary

RQ1: Performance comparison with state-of-the-art methods. We compare the
detection performance of SoucreP with the same division on the same dataset as
the existing state-of-the-art method according to the comparison method of
Zheng et al.[4]. Specifically, all contracts are ranked according to the order
of the block height at the time of smart contract creation, and the training
set consists of smart Ponzi schemes from the 1st to the 250th and non-Ponzi
smart contracts in between. The test set consists of the 251st to the last
341st smart Ponzi scheme and the remaining non-Ponzi scheme smart contracts.
Thus, the training set has a total of 5990 smart contracts, while the test set
has 508 smart contracts. Such a division, compared to random division,
provides a better representation of the model’s ability to detect emerging new
smart Ponzi schemes when it only has data on earlier smart Ponzi schemes. The
compared models include Ridge-NC [4]: a ridge classifier model trained with an
N-gram count feature; SVM-NC [4]: an SVM model trained with an N-gram count
feature; XGBoost-TF-IDF [4]: an XGBoost model trained model with TF-IDF
feature; MulCas [4]: a multi-view cascade combinatorial model; SadPonzi [22]:
a semantic-aware system for detecting smart Ponzi schemes. The first three
approaches use features extracted from the opcode of a smart contract, Mulcas
incorporates Developer Feature on top of that, while SadPonzi detects Ponzi
schemes based on the bytecode of a smart contract. The comparison results of
different methods are listed in Table I. As can be seen from the results,
SourceP shows the best performance in all three metrics. In particular,
SourceP gains a 21.3% recall improvement and a 12.9% F-score improvement over
the state-of-the-art method while ensuring that precision is also improved.
Since the ratio of positive and negative samples is about 1:20, it is
reasonable that the model prefers to classify the minority samples as the
majority, resulting in a relatively higher precision score than the recall
score.

TABLE I: Comparison of SourceP on recall, precision, and f-score on a fixed training and test set with state-of-the-art methods Method | Recall | Precision | F-score
---|---|---|---
XGBoost-TF-IDF | 0.234 | 0.882 | 0.370
SadPonzi | 0.52 | 0.59 | 0.55
SVM-NC | 0.375 | 0.923 | 0.533
Ridge-NC | 0.453 | 0.829 | 0.586
MulCas | 0.674 | 0.951 | 0.789
SourceP | 0.887 | 0.956 | 0.918
TABLE II: Comparison of SourceP on the three metrics on the dataset divided by block creation height with state-of-the-art methods Method | Metric | P2 | P3 | P4 | P5
---|---|---|---|---|---
| Precision | 0.33 | 0.42 | 0.18 | 0.24
SadPonzi | Recall | 1.0 | 0.71 | 0.25 | 0.18
| F-score | 0.5 | 0.53 | 0.21 | 0.20
| Precision | 0.88 | 0.96 | 0.81 | 0.95
MulCas | Recall | 0.38 | 0.32 | 0.94 | 0.67
| F-score | 0.53 | 0.48 | 0.87 | 0.79
| Precision | 0.99 | 0.97 | 0.88 | 0.96
SourceP | Recall | 0.55 | 0.89 | 0.90 | 0.89
| F-score | 0.59 | 0.92 | 0.88 | 0.92

RQ2: Sustainability of the model compared to other state-of-the-art methods.
Although SourceP has achieved excellent performance on the latest smart Ponzi
schemes detection, there is a new problem known as model aging that has
attracted widespread attention [66, 67]. In particular, there is a big
difference between the early smart Ponzi schemes and the latest Ponzi schemes
in smart contracts [4, 24]. To verify the sustainability of SourceP, in this
experiment, we divide the dataset into six parts (P0 to P5) according to the
height of the created blocks of Ponzi schemes, following the method of Zheng
et al. [4] divide the dataset by every 50 smart Ponzi schemes, e.g. block
height in the first 50 smart Ponzi schemes and the non-Ponzi contracts among
them are P0, while the smart Ponzi schemes with heights from 51 to 100 and the
non-Ponzi contracts among them are divided into P1, and so on for the
remaining P2, P3, P4, and P5. where P5 is the 251st to the last (314th) smart
Ponzi scheme and the non-Ponzi contracts among them. P5 is actually the
experiment of RQ1. The detection task is to predict the next dataset using the
previous dataset, e.g., P0 and P1 to predict P2, and P0, P1, and P2 to predict
P3. Because smart contracts are tamper-evident, a lower block height at
creation means an earlier creation time, which is equivalent to our use of an
earlier time smart Ponzi scheme to predict future smart Ponzi schemes as a way
to verify the sustainability of SourceP. Our comparison models include
SadPonzi [22] and MulCas [4], and the results are shown in Table II. It can be
seen that SourceP obtains the highest precision and F-score in each part of
the experiment, achieving the highest recall in P3 and P5, and the F-score
even improves by 39% when detecting the P3 part. Since the new smart Ponzi
scheme is deployed based on the ERC-20 token trading contract, the reward of
the Ponzi scheme is reflected in the increased value of the Ponzi tokens, and
SadPonzi and MulCas experience a degradation in their performance in detecting
this new smart Ponzi scheme. This experiment demonstrates that SourceP
achieves the best sustainability in detecting smart Ponzi schemes.

RQ3: Ablation experiments. We conducted ablation experiments to explore the
contribution played by the pre-training task and the data flow in the smart
Ponzi scheme detection by removing two pre-training tasks and the data flow
respectively and then performing the task of RQ1 to observe the final results.
The results are shown in Table III, where $-w/o$ is an abbreviation for
without. From the results, we can see that removing the two pre-training tasks
or not using the data flow makes the performance of the model degrade to
different degrees, which indicates that they play a role in improving the
model.

TABLE III: Comparison of ablation experiments on the three metrics with pre-training tasks or data flow removed Method | Recall | Precision | F-score
---|---|---|---
SourceP | 0.887 | 0.956 | 0.918
-w/o EdgePred | 0.867 | 0.919 | 0.891
-w/o NodeAlign | 0.821 | 0.914 | 0.860
-w/o Data Flow | 0.806 | 0.909 | 0.847

RQ4: Generalization ability of SourceP. To verify the generalization ability
of the model, we will divide the data set randomly to experiment. Also, to
prevent model overfitting, we divide the validation set separately from the
training set. Therefore, the ratio of training set: validation set: test set
in this experiment is 7:1:2. We show the average results of 20 experiments in
Table IV. As we can see from the table, SourceP has good performance and
generalization ability in detecting smart Ponzi schemes.

TABLE IV: SourceP on the three metrics on the randomly divided dataset Method | Recall | Precision | F-score
---|---|---|---
SourceP | 0.90 | 0.92 | 0.91

##  V Related Work

###  V-A Ponzi schemes on the blockchain

The Ponzi scheme is a classic financial fraud [23, 68]. With the development
of the Internet, online “High-Yield Investment Programs” (HYIP) became a
typical form of Ponzi scheme [69]. Because blockchain technology became
increasingly popular, unscrupulous individuals began to deploy such HYIPs on
the blockchain, and more and more Ponzi schemes and Internet scammers emerged
on the blockchain [70]. Chen et al. [30, 31] first proposed machine learning-
based identification of Ponzi schemes in Ethereum smart contracts by
extracting features from user accounts and the opcodes of smart contracts, and
then building a classification model to detect potential Ponzi schemes as
smart contract implementations. Fan et al. [27] based on CatBoost [71],
propose the Al-SPSD model to detect newly deployed smart Ponzi schemes from
the runtime opcode level promptly. Chen et al. [22] propose SADPonzi, a
working on Ethereum smart contract bytecode prototype system that identifies
smart Ponzi schemes. Zheng et al. [4] proposed building a multi-view cascade
model (MulCas) to identify Ponzi schemes. Liang et al. [72] detect Ponzi
schemes through contract runtime behavior graph (CRBG). Ponzi schemes in
blockchain platforms are not only present in Ethereum, some works have also
focused on Ponzi schemes in Bitcoin and detected them [73, 40, 74, 75].

###  V-B Smart Contract Analysis

Many smart contract analysis studies have been conducted on smart contract
security vulnerabilities in Ethereum, for example, Oyente [76], Osiris [77],
Mythril [78], Maian [79], and Manticore [80] use symbolic execution for
vulnerability detection. Securify [81] and Zeus [82] use formal verification
for vulnerability detection, and Slither [83] and SmartCheck [35] propose to
use static analysis for vulnerability detection. ContractFuzzer [84], and
ReGuardp [85] propose vulnerability detection using fuzzy testing. Thomas et
al.[86] provide an empirical review of these automated analysis tools for
smart contracts. Pinna et al.[87] conduct a comprehensive empirical study of
smart contracts deployed on the Ethereum blockchain, to provide an overview of
the characteristics of smart contracts. In addition, there are empirical
studies on the code smell of smart contracts [88], studies on the gas of
Ethereum smart contracts [89, 90], and the cloning behavior of the code [91,
92].

###  V-C Pre-Trained Models for Programming Languages

The emergence of pre-trained models (PTMs) has brought NLP into a new era
[93]. Some models such as BERT [50] and GPT [52] have recently achieved great
success and have become a milestone in the field of artificial intelligence
[49]. Several works have also explored the application of pre-trained models
(PTMs) on programming languages, such as Roberta [94], a model pre-trained on
a text corpus with a Mask Language Model (MLM) learning goal, where
RoBERTa(code) is pre-trained on code only. CuBERT [55] is the first work to
propose CodeBERT [54] pre-trained on code-text pairs with MLM and replacement
token detection learning goals, and is a representative pre-trained model for
multilingual code representation. The major difference between GraphCodeBERT
and CodeBERT is the inclusion of AST information [45]. UniXcoder [95] uses a
masked attention matrix with prefix adapters to control the behavior of the
model and enhances the code representation with cross-modal content such as
AST and code annotations.PLBART [96] is an application of the programming
language BART [97], which incorporates the advantages of both the
bidirectional encoder of the BERT model and the unidirectional left-to-right
decoder in GPT. CodeT5 [98] is a unified pre-trained Transformer model that
makes better use of code syntax information. Large-scale pre-trained models
have also evolved rapidly for code tasks, such as AlphaCode [99] which uses
the encoder-decoder architecture, Code-GPT [57] which uses a 12-layer
transformer decoder model, and GPT-C [56] which is designed for the task of
Code Completion.

##  VI Conclusion and future work

In this paper, we propose a method called SourceP to detect smart Ponzi
schemes on Ethereum. To the best of our knowledge, this is the first detection
method that uses only the source code of smart Ponzi schemes as features, and
the first method to detect smart Ponzi schemes based on pre-trained models and
data flows. In detecting smart Ponzi schemes on Ethereum, we experimentally
demonstrate that SourceP achieves better performance and sustainability
compared to existing state-of-the-art methods. We also design ablation
experiments to examine the contribution of pre-trained models and data flows
in SourceP. Finally, we experimentally demonstrate that SourceP possesses a
good generalization capability. We explore the feasibility of using variable
dependencies in source code to detect smart Ponzi schemes, avoiding some of
the drawbacks of traditional smart Ponzi scheme detection methods. We reveal
the potential for exploring Ponzi scheme features from smart contract source
code and getting better recognition. We believe that detecting smart contracts
as soon as possible after they are deployed can effectively reduce the
financial losses from Ponzi schemes on Ethereum and maintain a healthy ecology
of the blockchain community. We exposing the dataset and source code we used
to aid future research in this direction.

In our future work, the first step is to expand the dataset, which still has
few labeled smart Ponzi schemes, and expanding the dataset has a great effect
on improving the model. As mentioned in this paper, new types of smart Ponzi
schemes are more difficult to detect, so more data on new types of smart Ponzi
schemes are urgently needed. Or construct a Ponzi scheme dataset consisting of
multiple smart contracts, to detect whether the business logic consisting of
multiple contracts is a scheme. Given the excellent performance shown by pre-
trained models and data flow in smart Ponzi scheme detection, we will try to
explore the use of the method for other blockchain security tasks to advance
blockchain security technology.

## References

  * [1] S. Nakamoto, “Bitcoin: A peer-to-peer electronic cash system,” _Decentralized business review_ , p. 21260, 2008.
  * [2] W. Jiajing, Y. Qi, L. Dan, Y. Wei, C. Weili, C. Chuan, and Z. Zibin, “Who are the phishers? phishing scam detection on ethereum via network embedding,” in _IEEE Transactions on Systems, Man, and Cybernetics_ , vol. 52, 2022, pp. 1156–1166.
  * [3] E. Androulaki, A. Barger, V. Bortnikov, C. Cachin, K. Christidis, A. De Caro, D. Enyeart, C. Ferris, G. Laventman, Y. Manevich _et al._ , “Hyperledger fabric: a distributed operating system for permissioned blockchains,” in _Proceedings of the thirteenth EuroSys conference_ , 2018, pp. 1–15.
  * [4] Z. Zheng, W. Chen, Z. Zhong, Z. Chen, and Y. Lu, “Securing the ethereum from smart ponzi schemes: Identification using static features,” in _ACM Transactions on Software Engineering and Methodology 32.5 (2023): 1-28._ , 2022\.
  * [5] K. Christidis and M. Devetsikiotis, “Blockchains and smart contracts for the internet of things,” _Ieee Access_ , vol. 4, pp. 2292–2303, 2016.
  * [6] J. Huang, D. He, M. S. Obaidat, P. Vijayakumar, M. Luo, and K.-K. R. Choo, “The application of the blockchain technology in voting systems: A review,” _ACM Computing Surveys (CSUR)_ , vol. 54, no. 3, pp. 1–28, 2021.
  * [7] S. B. Patel, H. A. Kheruwala, M. Alazab, N. Patel, R. Damani, P. Bhattacharya, S. Tanwar, and N. Kumar, “Biouav: Blockchain-envisioned framework for digital identification to secure access in next-generation uavs,” in _Proceedings of the 2nd ACM MobiCom Workshop on Drone Assisted Wireless Communications for 5G and Beyond_ , 2020, pp. 43–48.
  * [8] Y. Wang, Z. Su, Q. Xu, R. Li, and T. H. Luan, “Lifesaving with rescuechain: Energy-efficient and partition-tolerant blockchain based secure information sharing for uav-aided disaster rescue,” in _IEEE INFOCOM 2021-IEEE Conference on Computer Communications_. IEEE, 2021, pp. 1–10.
  * [9] T. McGhin, K.-K. R. Choo, C. Z. Liu, and D. He, “Blockchain in healthcare applications: Research challenges and opportunities,” _Journal of network and computer applications_ , vol. 135, pp. 62–75, 2019.
  * [10] C. Xu, K. Wang, P. Li, S. Guo, J. Luo, B. Ye, and M. Guo, “Making big data open in edges: A resource-efficient blockchain-based approach,” _IEEE Transactions on Parallel and Distributed Systems_ , vol. 30, no. 4, pp. 870–882, 2018.
  * [11] R. Belchior, A. Vasconcelos, S. Guerreiro, and M. Correia, “A survey on blockchain interoperability: Past, present, and future trends,” _ACM Computing Surveys (CSUR)_ , vol. 54, no. 8, pp. 1–41, 2021.
  * [12] K. Qin, L. Zhou, and A. Gervais, “Quantifying blockchain extractable value: How dark is the forest?” in _2022 IEEE Symposium on Security and Privacy (SP)_. IEEE, 2022, pp. 198–214.
  * [13] “Ethereum,” https://www.ethereum.org/.
  * [14] S. Wang, L. Ouyang, Y. Yuan, X. Ni, X. Han, and F.-Y. Wang, “Blockchain-enabled smart contracts: Architecture, applications, and future trends,” _IEEE Transactions on Systems, Man, and Cybernetics_ , vol. 49, pp. 1–12, 2019.
  * [15] N. Szabo, “The idea of smart contracts,” _Nick Szabo’s papers and concise tutorials_ , vol. 6, no. 1, p. 199, 1997.
  * [16] Z. Zheng, S. Xie, H.-N. Dai, W. Chen, X. Chen, J. Weng, and M. Imran, “An overview on smart contracts: Challenges, advances and platforms,” _Future Generation Computer Systems_ , vol. 105, pp. 475–491, 2020.
  * [17] X. Liu, Z. Tang, P. Li, S. Guo, X. Fan, and J. Zhang, “A graph learning based approach for identity inference in dapp platform blockchain,” _IEEE Transactions on Emerging Topics in Computing_ , vol. 10, no. 1, pp. 438–449, 2020\.
  * [18] W. Cai, Z. Wang, J. B. Ernst, Z. Hong, C. Feng, and V. C. Leung, “Decentralized applications: The blockchain-empowered software system,” _IEEE access_ , vol. 6, pp. 53 019–53 033, 2018.
  * [19] S. Raval, _Decentralized applications: harnessing Bitcoin’s blockchain technology_. ” O’Reilly Media, Inc.”, 2016\.
  * [20] “Cryptokitties,” https://www.cryptokitties.co.
  * [21] “Idex,” https://idex.market/eth/aura.
  * [22] W. Chen, X. Li, Y. Sui, N. He, H. Wang, L. Wu, and X. Luo, “Sadponzi: Detecting and characterizing ponzi schemes in ethereum smart contracts,” in _Proceedings of the ACM on Measurement and Analysis of Computing Systems_ , 2021, pp. 35–36.
  * [23] M. Artzrouni, “The mathematics of ponzi schemes,” _Mathematical Social Sciences_ , vol. 58, no. 2, pp. 190–201, 2009.
  * [24] M. Bartoletti, S. Carta, T. Cimoli, and R. Saia, “Dissecting ponzi schemes on ethereum: Identification, analysis, and impact,” _Future Generation Computer Systems_ , vol. 102, pp. 259–277, 2020.
  * [25] “Ponzitracker,” https://www.ponzitracker.com/2022-ponzi-schemes.
  * [26] “Sec charges eleven individuals in $300 million crypto pyramid scheme,” https://www.sec.gov/news/press-release/2022-134.
  * [27] S. Fan, S. Fu, H. Xu, and X. Cheng, “Al-spsd: Anti-leakage smart ponzi schemes detection in blockchain,” _Information Processing & Management_, vol. 58, pp. 102 587–, 2021.
  * [28] E. Jung, M. L. Tilly, A. Gehani, and Y. Ge, “Data mining-based ethereum fraud detection,” _2019 IEEE international conference on blockchain_ , pp. 266–273, 2019.
  * [29] X. He, T. Yang, and L. Chen, “Ctrf: Ethereum-based ponzi contract identification,” _Security and Communication Networks_ , vol. 2022, 2022\.
  * [30] W. Chen, Z. Zheng, J. Cui, E. Ngai, P. Zheng, and Y. Zhou, “Detecting ponzi schemes on ethereum: Towards healthier blockchain technology.” _Proceedings of the 2018 world wide web conference_ , pp. 1409–1418, 2018\.
  * [31] W. Chen, Z. Zheng, E. C.-H. Ngai, P. Zheng, and Y. Zhou, “Exploiting blockchain data to detect smart ponzi schemes on ethereum,” _IEEE Access_ , vol. 7, pp. 37 575–37 586, 2019.
  * [32] OpenAI, “Gpt-4 technical report,” _arXiv preprint arXiv:2303.08774_ , 2023\.
  * [33] C.-Y. Wang, A. Bochkovskiy, and H.-Y. M. Liao, “Yolov7: Trainable bag-of-freebies sets new state-of-the-art for real-time object detectors,” _Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition_ , 2022.
  * [34] K. Clark, M.-T. Luong, Q. V. Le, and C. D. Manning, “Electra: Pre-training text encoders as discriminators rather than generators,” _arXiv preprint arXiv:2003.10555_ , 2020.
  * [35] S. Tikhomirov, E. Voskresenskaya, I. Ivanitskiy, R. Takhaviev, E. Marchenko, and Y. Alexandrov, “Smartcheck: Static analysis of ethereum smart contracts.” 2018, pp. 9–16.
  * [36] “Solidity,” http://solidity.readthedocs.io/en/latest.
  * [37] N. Szabo, “Smart contracts: building blocks for digital markets,” _EXTROPY: The Journal of Transhumanist Thought,(16)_ , vol. 18, no. 2, p. 28, 1996.
  * [38] V. Buterin _et al._ , “A next-generation smart contract and decentralized application platform,” _white paper_ , vol. 3, no. 37, pp. 2–1, 2014.
  * [39] “Serpent,” https://github.com/ethereum/wiki/wiki/Serpent.
  * [40] M. Vasek and T. Moore, “Analyzing the bitcoin ponzi scheme ecosystem.” _Springer Berlin Heidelberg_ , pp. 101–112, 2019.
  * [41] “Chainalysis,” https://go.chainalysis.com/2023-Crypto-Crime-Report.html.
  * [42] “Onecoin,” https://en.wikipedia.org/wiki/OneCoin.
  * [43] A. Roan, “Ethereum smart contract ponzi schemes,” https://medium.com/blockcentric/ethereum-smart-contract-ponzi-schemes-9e43015b56f8.
  * [44] ——, “Ethereum smart contract ponzi schemes: Part 3,” https://medium.com/blockcentric/ethereum-smart-contract-ponzi-schemes-part-3-c99e9d608c9b.
  * [45] D. Guo, S. Ren, S. Lu, Z. Feng, D. Tang, S. Liu, L. Zhou, N. Duan, J. Yin, D. Jiang, and M. Zhou, “Graphcodebert: Pre-training code representations with data flow,” _arXiv preprint arXiv:2009.08366_ , 2021.
  * [46] M. Allamanis, M. Brockschmidt, and M. Khademi, “Learning to represent programs with graphs,” _arXiv preprint arXiv:1711.00740_ , 2017.
  * [47] D. Liu, S. Yin, G. Luo, J. Shang, L. Liu, S. Wei, Y. Feng, and S. Zhou, “Data-flow graph mapping optimization for cgra with deep reinforcement learning,” _IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems_ , vol. 38, no. 12, pp. 2271–2283, 2018.
  * [48] V. J. Hellendoorn, C. Sutton, R. Singh, P. Maniatis, and D. Bieber, “Global relational models of source code,” in _International conference on learning representations_ , 2019.
  * [49] X. Han, Z. Zhang, N. Ding, Y. Gu, X. Liu, Y. Huo, J. Qiu, L. Zhang, W. Han, M. Huang, Q. Jin, Y. Lan, Y. Liu, Z. Liu, Z. Lu, X. Qiu, R. Song, J. Tang, J.-R. Wen, J. Yuan, W. X. Zhao, and J. Zhu, “Pre-trained models: Past, present and future,” _AI Open_ , 2021.
  * [50] J. Devlin, M.-W. Chang, K. Lee, and K. Toutanova, “Bert: Pre-training of deep bidirectional transformers for language understanding,” _arXiv preprint arXiv:1810.04805_ , 2018.
  * [51] M. E. Peters, M. Neumann, M. Iyyer, M. Gardner, C. Clark, K. Lee, and L. S. Zettlemoyer, “Deep contextualized word representations.” vol. abs/1802.05365, 2018.
  * [52] A. Radford, K. Narasimhan, T. Salimans, I. Sutskever _et al._ , “Improving language understanding by generative pre-training,” 2018.
  * [53] Z. Yang, Z. Dai, Y. Yang, J. G. Carbonell, R. Salakhutdinov, Q. V. Le, and R. R. Salakhutdinov, “Xlnet: Generalized autoregressive pretraining for language understanding.” vol. 32, pp. 5754–5764, 2019.
  * [54] F. Zhangyin, G. Daya, T. Duyu, D. Nan, F. Xiaocheng, G. Ming, S. Linjun, Q. Bing, L. Ting, J. Daxin, and Z. Ming, “Codebert: A pre-trained model for programming and natural languages,” _arXiv preprint arXiv:2002.08155_ , vol. 2020.findings-emnlp, pp. 1536–1547, 2020.
  * [55] A. Kanade, P. Maniatis, G. Balakrishnan, and K. Shi, “Learning and evaluating contextual embedding of source code,” _International conference on machine learning_ , pp. 5110–5121, 2020.
  * [56] S. Alexey, D. S. Kun, F. Shengyu, and S. Neel, “Intellicode compose: Code generation using transformer,” _Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering_ , pp. 1433–1443, 2020.
  * [57] S. Lu, D. Guo, S. Ren, J. Huang, A. Svyatkovskiy, A. Blanco, C. Clement, D. Drain, D. Jiang, D. Tang, G. Li, L. Zhou, L. Shou, L. Zhou, M. Tufano, M. Gong, M. Zhou, N. Duan, N. Sundaresan, S. K. Deng, S. Fu, and S. Liu, “Codexglue: A machine learning benchmark dataset for code understanding and generation.” _arXiv preprint arXiv:2102.04664_ , 2021.
  * [58] H. Husain, H.-H. Wu, T. Gazit, M. Allamanis, and M. Brockschmidt, “Codesearchnet challenge: Evaluating the state of semantic code search,” _arXiv preprint arXiv:1909.09436_ , 2019.
  * [59] “tree-sitter,” https://tree-sitter.github.io/tree-sitter.
  * [60] “tree-sitter-solidity,” https://github.com/JoranHonig/tree-sitter-solidity.
  * [61] “tree-sitter-javascript,” https://github.com/tree-sitter/tree-sitter-javascript.
  * [62] A. Vaswani, N. Shazeer, N. Parmar, J. Uszkoreit, L. Jones, A. N. Gomez, L. Kaiser, and I. Polosukhin, “Attention is all you need.” _Advances in neural information processing systems_ , vol. 30, pp. 5998–6008, 2017.
  * [63] H. Wu, Z. Zhang, S. Wang, Y. Lei, B. Lin, Y. Qin, H. Zhang, and X. Mao, “Peculiar: Smart contract vulnerability detection based on crucial data flow graph and pre-training techniques,” _2021 IEEE 32nd International Symposium on Software Reliability Engineering (ISSRE)_ , pp. 378–389, 2021.
  * [64] Y. Liu, M. Ott, N. Goyal, J. Du, M. Joshi, D. Chen, O. Levy, M. Lewis, L. Zettlemoyer, and V. Stoyanov, “Roberta: A robustly optimized bert pretraining approach,” _arXiv preprint arXiv:1907.11692_ , 2019.
  * [65] “Etherscan,” https://etherscan.io/.
  * [66] H. Cai, “Assessing and improving malware detection sustainability through app evolution studies,” _ACM Transactions on Software Engineering and Methodology (TOSEM)_ , vol. 29, no. 2, pp. 1–28, 2020.
  * [67] F. Pendlebury, F. Pierazzi, R. Jordaney, J. Kinder, and L. Cavallaro, “Tesseract: Eliminating experimental bias in malware classification across space and time,” in _28th USENIX Security Symposium (USENIX Security 19)_ , 2019, pp. 729–746.
  * [68] A. Zhu, P. Fu, Q. Zhang, and Z. Chen, “Ponzi scheme diffusion in complex networks,” _Physica A: Statistical Mechanics and its Applications_ , vol. 479, pp. 128–136, 2017.
  * [69] T. Moore, J. Han, and R. Clayton, “The postmodern ponzi scheme: Empirical analysis of high-yield investment programs.” _Financial Cryptography and Data Security: 16th International Conference, FC 2012_ , pp. 41–56, 2012.
  * [70] K. Toyoda, T. Ohtsuki, and P. T. Mathiopoulos, “Identification of high yielding investment programs in bitcoin via transactions pattern analysis.” _GLOBECOM 2017-2017 IEEE Global Communications Conference_ , pp. 1–6, 2017\.
  * [71] L. O. Prokhorenkova, G. Gusev, A. Vorobev, A. V. Dorogush, and A. Gulin, “Catboost - unbiased boosting with categorical features.” _Advances in neural information processing systems_ , pp. 6639–6649, 2018.
  * [72] R. Liang, J. Chen, K. He, Y. Wu, G. Deng, R. Du, and C. Wu, “Ponziguard: Detecting ponzi schemes on ethereum with contract runtime behavior graph (crbg),” in _2024 IEEE/ACM 46th International Conference on Software Engineering (ICSE)_. IEEE Computer Society, 2023, pp. 755–766.
  * [73] Y. Boshmaf, C. Elvitigala, H. Al Jawaheri, P. Wijesekera, and M. Al Sabah, “Investigating mmm ponzi scheme on bitcoin,” in _Proceedings of the 15th ACM Asia Conference on Computer and Communications Security_ , 2020, pp. 519–530.
  * [74] M. Vasek and T. Moore, “There’s no free lunch, even using bitcoin: Tracking the popularity and profits of virtual currency scams,” in _Financial Cryptography and Data Security: 19th International Conference, FC 2015, San Juan, Puerto Rico, January 26-30, 2015, Revised Selected Papers 19_. Springer, 2015, pp. 44–61.
  * [75] M. Bartoletti, B. Pes, and S. Serusi, “Data mining for detecting bitcoin ponzi schemes,” in _2018 Crypto Valley Conference on Blockchain Technology (CVCBT)_. IEEE, 2018, pp. 75–84.
  * [76] L. Luu, D.-H. Chu, H. Olickel, P. Saxena, and A. Hobor, “Making smart contracts smarter.” _IACR Cryptology ePrint Archive_ , vol. 2016, pp. 254–269, 2016.
  * [77] C. F. Torres, J. Schütte, and R. State, “Osiris: Hunting for integer bugs in ethereum smart contracts,” pp. 664–676, 2018.
  * [78] B. Mueller, “Smashing ethereum smart contracts for fun and real profit,” _HITB SECCONF Amsterdam_ , vol. 9, p. 54, 2018.
  * [79] I. Nikolic, A. Kolluri, I. Sergey, P. Saxena, and A. Hobor, “Finding the greedy, prodigal, and suicidal contracts at scale,” vol. abs/1802.06038, pp. 653–663, 2018.
  * [80] M. Mossberg, F. Manzano, E. Hennenfent, A. Groce, G. Grieco, J. Feist, T. Brunson, and A. Dinaburg, “Manticore: a user-friendly symbolic execution framework for binaries and smart contracts,” pp. 1186–1189, 2019.
  * [81] P. Tsankov, A. Dan, D. Drachsler-Cohen, A. Gervais, F. Buenzli, and M. Vechev, “Securify: Practical security analysis of smart contracts,” in _Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security_ , 2018, pp. 67–82.
  * [82] S. Kalra, S. Goel, M. Dhawan, and S. Sharma, “Zeus: Analyzing safety of smart contracts.” in _ISOC Network and Distributed System Security Symposium_ , 2018.
  * [83] J. Feist, G. Greico, and A. Groce, “Slither: a static analysis framework for smart contracts,” pp. 8–15, 2019.
  * [84] B. Jiang, Y. Liu, and W. K. Chan, “Contractfuzzer: Fuzzing smart contracts for vulnerability detection.” in _Automated Software Engineering_ , vol. abs/1807.03932, 2018, pp. 259–269.
  * [85] C. Liu, H. Liu, Z. Cao, Z. Chen, B. Chen, and B. Roscoe, “Reguard: finding reentrancy bugs in smart contracts.” 2018, pp. 65–68.
  * [86] D. Thomas, F. J. F., A. Rui, and C. Pedro, “Empirical review of automated analysis tools on 47,587 ethereum smart contracts,” vol. abs/1910.10601, 2020, pp. 530–541.
  * [87] A. Pinna, S. Ibba, G. Baralla, R. Tonelli, and M. Marchesi, “A massive analysis of ethereum smart contracts empirical study and code metrics.” vol. 7, pp. 78 194.0–78 213.0, 2019.
  * [88] J. Chen, X. Xia, D. Lo, J. Grundy, D. X. Luo, and T. Chen, “Domain specific code smells in smart contracts.” vol. abs/1905.01467, 2019.
  * [89] A. Elvira, C. Jesús, G. Pablo, R.-D. Guillermo, and R. Albert, “Gasol: Gas analysis and optimization for ethereum smart contracts.” 2020, pp. 118–125.
  * [90] N. Grech, M. Kong, A. Jurisevic, L. Brent, B. Scholz, and Y. Smaragdakis, “Madmax: Surviving out-of-gas conditions inethereum smart contracts,” vol. 2, pp. 1–27, 2018.
  * [91] N. He, L. Wu, H. Wang, Y. Guo, and X. Jiang, “Characterizing code clones in the ethereum smart contract ecosystem.” pp. 654–675, 2020.
  * [92] H. Liu, Z. Yang, C. Liu, Y. Jiang, W. Zhao, and J. Sun, “Eclone: detect semantic clones in ethereum via symbolic transaction sketch.” in _ESEC/SIGSOFT FSE_ , 2018, pp. 900–903.
  * [93] Q. Xipeng, S. Tianxiang, X. Yige, S. Yunfan, D. Ning, and H. Xuanjing, “Pre-trained models for natural language processing: A survey,” vol. 63.0, pp. 1872.0–1897.0, 2020.
  * [94] Y. Liu, M. Ott, N. Goyal, J. Du, M. Joshi, D. Chen, O. Levy, M. Lewis, L. Zettlemoyer, and V. Stoyanov, “Roberta: A robustly optimized bert pretraining approach,” _arXiv preprint arXiv:1907.11692_ , 2019.
  * [95] D. Guo, S. Lu, N. Duan, Y. Wang, M. Zhou, and J. Yin, “Unixcoder: Unified cross-modal pre-training for code representation,” vol. Proceedings of the 60th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pp. 7212–7225, 2022.
  * [96] W. U. Ahmad, S. Chakraborty, B. Ray, and K.-W. Chang, “Unified pre-training for program understanding and generation,” pp. 2655–2668, 2021.
  * [97] L. Mike, L. Yinhan, G. Naman, G. Marjan, M. Abdelrahman, L. Omer, S. Ves, and Z. Luke, “Bart: Denoising sequence-to-sequence pre-training for natural language generation, translation, and comprehension,” pp. 7871–7880, 2020.
  * [98] Y. Wang, W. Wang, S. Joty, and S. C. H. Hoi, “Codet5 - identifier-aware unified pre-trained encoder-decoder models for code understanding and generation.” vol. 2021.emnlp-main, pp. 8696–8708, 2021.
  * [99] Y. Li, D. Choi, J. Chung, N. Kushman, J. Schrittwieser, R. Leblond, T. Eccles, J. Keeling, F. Gimeno, A. D. Lago, T. Hubert, P. Choy, C. de Masson d’Autume, I. Babuschkin, X. Chen, P.-S. Huang, J. Welbl, S. Gowal, A. Cherepanov, J. Molloy, D. J. Mankowitz, E. S. Robson, P. Kohli, N. de Freitas, K. Kavukcuoglu, and O. Vinyals, “Competition-level code generation with alphacode.” vol. 378, pp. 1092–1097, 2022.


# An Intuitionisticaly based Description Logic

Alexandre Rademaker  IBM Research and FGV/EMAp<EMAIL_ADDRESS>Edward
Hermann Haeusler  Dep. Informática, PUC-Rio<EMAIL_ADDRESS>
###### Abstract

This article presents $i\mathcal{ALC}$, an intuitionistic version of the
classical description logic $\mathcal{ALC}$, based on the framework for
constructive modal logics presented by Simpson [14] and related to description
languages, via hybrid logics, by dePaiva [3]. This article corrects and
extends the presentation of $i\mathcal{ALC}$ appearing in [4]. It points out
the difference between $i\mathcal{ALC}$ and the intuitionistic hybrid logic
presented in [3]. Completeness and soundness proofs are provided. A brief
discussion on the computational complexity of $i\mathcal{ALC}$ provability is
taken. It is worth mentioning that $i\mathcal{ALC}$ is used to formalize legal
knowledge [10, 9, 8, 7], and in fact, was specifically designed to this goal.

##  1 Intuitionistic ALC

The $i\mathcal{ALC}$ logic is based on the framework for intuitionistic modal
logic IK proposed in [14, 5, 13]. These modal logics arise from interpreting
the usual possible worlds definitions in an intuitionistic meta-theory. As we
will see in the following paragraphs, ideas from [1] were also used, where the
framework IHL, for _intuitionistic hybrid logics_ , is introduced.
$i\mathcal{ALC}$ concepts are described as:

$C,D::=A\mid\bot\mid\top\mid\neg C\mid C\sqcap D\mid C\sqcup D\mid
C\sqsubseteq D\mid\exists R.C\mid\forall R.C$

where $C,D$ stands for concepts, $A$ for an atomic concept, $R$ for an atomic
role. We could have used distinct symbols for subsumption of concepts and the
subsumption concept constructor but this would blow-up the calculus
presentation. This syntax is more general than standard $\mathcal{ALC}$ since
it includes subsumption $\sqsubseteq$ as a concept-forming operator. We have
no use for nested subsumptions, but they do make the system easier to define,
so we keep the general rules. Negation could be defined via subsumption, that
is, $\neg C=C\sqsubseteq\bot$, but we find it convenient to keep it in the
language. The constant $\top$ could also be omitted since it can be
represented as $\neg\bot$.

A constructive interpretation of $i\mathcal{ALC}$ is a structure $\mathcal{I}$
consisting of a non-empty set $\Delta^{\mathcal{I}}$ of entities in which each
entity represents a partially defined individual; a refinement pre-ordering
$\preceq^{\cal I}$ on $\Delta^{\cal I}$, i.e., a reflexive and transitive
relation; and an interpretation function $\cdot^{\cal I}$ mapping each role
name $R$ to a binary relation $R^{\cal I}\subseteq\Delta^{\cal
I}\times\Delta^{\cal I}$ and atomic concept $A$ to a set $A^{\cal
I}\subseteq\Delta^{\cal I}$ which is closed under refinement, i.e., $x\in
A^{\cal I}$ and $x\preceq^{\cal I}y$ implies $y\in A^{\cal I}$. The
interpretation $\cal I$ is lifted from atomic concepts to arbitrary concepts
via:

$\begin{array}[]{rl}\top^{\cal I}&=_{df}\Delta^{\cal I}\\\ \bot^{\cal
I}&=_{df}\emptyset\\\ (\neg C)^{\cal I}&=_{df}\\{x\mid\forall y\in\Delta^{\cal
I}.x\preceq y\Rightarrow y\not\in C^{\cal I}\\}\\\ (C\sqcap D)^{\cal
I}&=_{df}C^{\cal I}\cap D^{\cal I}\\\ (C\sqcup D)^{\cal I}&=_{df}C^{\cal
I}\cup D^{\cal I}\\\ (C\sqsubseteq D)^{\cal I}&=_{df}\\{x\mid\forall
y\in\Delta^{\cal I}.(x\preceq y\text{ and }y\in C^{\cal I})\Rightarrow y\in
D^{\cal I}\\}\\\ (\exists R.C)^{\cal I}&=_{df}\\{x\mid\exists y\in\Delta^{\cal
I}.(x,y)\in R^{\cal I}\mbox{ and }y\in C^{\cal I}\\}\\\ (\forall R.C)^{\cal
I}&=_{df}\\{x\mid\forall y\in\Delta^{\cal I}.x\preceq y\Rightarrow\forall
z\in\Delta^{\cal I}.(y,z)\in R^{\cal I}\Rightarrow z\in C^{\cal I}\\}\\\
\end{array}$

Following the semantics of IK, the structures $\cal I$ are models for
$i\mathcal{ALC}$ if they satisfy two frame conditions:

F1

if $w\leq w^{\prime}$ and $wRv$ then $\exists
v^{\prime}.w^{\prime}Rv^{\prime}$ and $v\leq v^{\prime}$

F2

if $v\leq v^{\prime}$ and $wRv$ then $\exists
w^{\prime}.w^{\prime}Rv^{\prime}$ and $w\leq w^{\prime}$

The above conditions are diagrammatically expressed as:

$\begin{array}[]{ccc}\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
11.44446pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{w^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
13.24402pt\raise 5.39166pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.39166pt\hbox{$\scriptstyle{R}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 31.48412pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces{\hbox{\kern
11.71953pt\raise-17.54166pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{(F1)}$}}}}}\ignorespaces{}{\hbox{\kern
31.48412pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{v^{\prime}}$}}}}}}}{\hbox{\kern-6.71413pt\raise-35.08331pt\hbox{\hbox{\kern
0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{w\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
13.24402pt\raise-29.69165pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.39166pt\hbox{$\scriptstyle{R}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern
32.25412pt\raise-35.08331pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\leq}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 0.0pt\raise-3.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
32.25412pt\raise-35.08331pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{v\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
37.85712pt\raise-17.54166pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\leq}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 37.85712pt\raise-3.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces}}}}\ignorespaces&\mbox{and}&\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
11.44446pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{w^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
13.24402pt\raise 5.39166pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.39166pt\hbox{$\scriptstyle{R}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 31.48412pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces{\hbox{\kern
11.71953pt\raise-17.54166pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{(F2)}$}}}}}\ignorespaces{}{\hbox{\kern
31.48412pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{v^{\prime}}$}}}}}}}{\hbox{\kern-6.71413pt\raise-35.08331pt\hbox{\hbox{\kern
0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{w\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
13.24402pt\raise-29.69165pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.39166pt\hbox{$\scriptstyle{R}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern
32.25412pt\raise-35.08331pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\leq}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 0.0pt\raise-3.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern
32.25412pt\raise-35.08331pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{v\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
37.85712pt\raise-17.54166pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{\leq}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 37.85712pt\raise-3.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces}}}}\ignorespaces\end{array}$

Our setting simplifies [11], since $i\mathcal{ALC}$ satisfies (like classical
$\mathcal{ALC}$) $\exists R.\bot=\bot$ and $\exists R.(C\sqcup D)=\exists
R.C\sqcup\exists R.D$.

Building up from the Simpson’s constructive modal logics (called here IML), in
[1], it is introduced _intuitionistic hybrid logics_ , denoted by IHL. Hybrid
logics add to usual modal logics a new kind of propositional symbols, the
_nominals_ , and also the so-called _satisfaction operators_. A nominal is
assumed to be true at exactly one world, so a nominal can be considered the
name of a world. If $x$ is a nominal and $X$ is an arbitrary formula, then a
new formula $x\colon{}\mkern-4.0muX$ called a satisfaction statement can be
formed. The satisfaction statement $x\colon{}\mkern-4.0muX$ expresses that the
formula $X$ is true at one particular world, namely the world denoted by $x$.
In hindsight one can see that IML shares with hybrid formalisms the idea of
making the possible-world semantics part of the deductive system. While IML
makes the relationship between worlds (e.g., $xRy$) part of the deductive
system, IHL goes one step further and sees the worlds themselves $x,y$ as part
of the deductive system, (as they are now nominals) and the satisfaction
relation itself as part of the deductive system, as it is now a syntactic
operator, with modality-like properties. In contrast with the above mentioned
approaches, ours assign a truth values to some formulas, also called
assertions, they are not concepts as in [1], for example. Below we define the
syntax of general assertions ($A$) and nominal assertions ($N$) for ABOX
reasoning in $i\mathcal{ALC}$. Formulas ($F$) also includes subsumption of
concepts interpreted as propositional statements.

$N::=x\colon C\mid x\colon N\hskip 56.9055ptA::=N\mid xRy\hskip
56.9055ptF::=A\mid C\sqsubseteq C$

where $x$ and $y$ are nominals, $R$ is a role symbol and $C$ is a concept. In
particular, this allows $x\colon(y\colon C)$, which is a perfectly valid
nominal assertion.

######  Definition 1 (outer nominal)

In a nominal assertion $x\colon\gamma$, $x$ is said to be the outer nominal of
this assertion. That is, in an assertion of the form $x\colon(y\colon\gamma)$,
$x$ is the outer nominal.

We write $\mathcal{I},w\models C$ to abbreviate $w\in C^{\mathcal{I}}$ which
means that entity $w$ satisfies concept $C$ in the interpretation $\cal
I$111In IHL, this $w$ is a world and this satisfaction relation is possible
world semantics. Further, $\cal I$ is a model of $C$, written
$\mathcal{I}\models C$ iff $\forall w\in{\cal I}.{\cal I},w\models C$.
Finally, $\models C$ means $\forall{\cal I}.{\cal I}\models C$. All previous
notions are extended to sets $\Phi$ of concepts in the usual universal
fashion. Given the hybrid satisfaction statements, the interpretation and
semantic satisfaction relation are extended in the expected way. The statement
$\mathcal{I},w\models x\colon C$ holds, if and only if, $\forall
z_{x}\succeq^{\cal I}x\ .\ \mathcal{I},z_{x}\models C$. In a similar fashion,
$\mathcal{I},w\models xRy$ holds ,if and only if, $\forall z_{x}\succeq
x.\forall z_{y}\succeq y.(x_{x}^{\mathcal{I}},z_{y}^{\mathcal{I}})\in
R^{\mathcal{I}}$. That is, the evaluation of the hybrid formulas does not take
into account only the world $w$, but it has to be monotonically preserved. It
can be observed that for every $w^{\prime}$, if $x^{\mathcal{I}}\preceq
w^{\prime}$ and $\mathcal{I},x^{\prime}\models\alpha$, then
$\mathcal{I},w^{\prime}\models\alpha$ is a property holding on this
satisfaction relation.

In common reasoning tasks the interpretation $\cal I$ and the entity $w$ in a
verification goal such as ${\cal I},w\models\delta$ are not given directly but
are themselves axiomatized by sets of concepts and formulas. Usually we have a
set $\Theta$ 222Here we consider only acycled TBox with $\sqsubseteq$ and
$\equiv$. of formulas and the set $\Gamma$ of concepts. Accordingly:

###### Definition 2

We write $\Theta,\Gamma\models\delta$ if it is the case that:

$\forall{\cal I}.((\forall x\in\Delta^{\cal I}.({\cal I},x\models\Theta))\\\
\Rightarrow\forall(Nom(\Gamma,\delta)).\forall\vec{z}\succeq
Nom(\Gamma,\delta).({\cal I},\vec{z}\models\Gamma\Rightarrow{\cal
I},\vec{z}\models\delta)$ (1)

where $\vec{z}$ denotes a vector of variables $z_{1},\ldots,z_{k}$ and
$Nom(\Gamma,\delta)$ is the vector of all outer nominals occurring in each
nominal assertion of $\Gamma\cup\\{\delta\\}$. $x$ is the only outer nominal
of a nominal assertion $\\{x\colon\gamma\\}$, while a (pure) concept $\gamma$
has no outer nominal.

A Hilbert calculus for $i\mathcal{ALC}$ is provided following [13, 14, 5]. It
consists of all axioms of intuitionistic propositional logic plus the axioms
and rules displayed in Figure 1. The Hilbert calculus implements TBox-
reasoning. That is, it decides the semantical relationship
$\Theta,\emptyset\models C$. $\Theta$ has only formulas as members.

$\displaystyle 0.$ all substitution instances of theorems of IPL
$\displaystyle 1.$ $\displaystyle\quad\forall R.(C\sqsubseteq
D)\sqsubseteq(\forall R.C\sqsubseteq\forall R.D)$ $\displaystyle 2.$
$\displaystyle\quad\exists R.(C\sqsubseteq D)\sqsubseteq(\exists
R.C\sqsubseteq\exists R.D)$ $\displaystyle 3.$ $\displaystyle\quad\exists
R.(C\sqcup D)\sqsubseteq(\exists R.C\sqcup\exists R.D)$ $\displaystyle 4.$
$\displaystyle\quad\exists R.\bot\sqsubseteq\bot$ $\displaystyle 5.$
$\displaystyle\quad(\exists R.C\sqsubseteq\forall R.C)\sqsubseteq\forall
R.(C\sqsubseteq D)$ $\displaystyle\mathsf{MP}$ If $C$ and $C\sqsubseteq D$ are
theorems, $D$ is a theorem too. $\displaystyle\mathsf{Nec}$ If $C$ is a
theorem then $\forall R.C$ is a theorem too. Figure 1: The $i\mathcal{ALC}$
axiomatization

A Sequent Calculus for $i\mathcal{ALC}$ is also provided. The logical rules of
the Sequent Calculus for $i\mathcal{ALC}$ are presented in Figure 2. 333The
reader may want to read Proof Theory books, for example, [15, 2, 12, 6]. The
structural rules and the cut rule are omitted but they are as usual. The
$\delta$ stands for concepts or assertions ($x\colon C$ or $xRy$), $\alpha$
and $\beta$ for concept and $R$ for role. $\Delta$ is a set of formulas. In
rules p-$\exists$ and p-$\forall$, the syntax $\forall R.\Delta$ means
$\\{\forall R.\alpha\mid\alpha\in concepts(\Delta)\\}$, that is, all concepts
in $\Delta$ are universal quantified with the same role. The assertions in
$\Delta$ are kept unmodified. In the same way, in rule p-N the addition of the
nominal is made only in the concepts of $\Delta$ (and in $\delta$ if that is a
concept) keeping the assertions unmodified.

The propositional connectives ($\sqcap,\sqcup,\sqsubseteq$) rules are as
usual, the rule $\sqcup_{2}$-r is omitted. The rules are presented without
nominals but for each of these rules there is a counterpart with nominals. For
example, the rule $\sqsubseteq$-r has one similar:

$\mathord{\Delta,x\colon\alpha}\Rightarrow\ \mathord{}$$x\colon\beta$
n-$\sqsubseteq$-r $\mathord{\Delta}\Rightarrow\
\mathord{}$$x\colon(\alpha\sqsubseteq\beta)$

The main modification comes for the modal rules, which are now role
quantification rules. We must keep the intuitionistic constraints for modal
operators. Rule $\exists$-l has the usual condition that $y$ is not in the
conclusion. Concerning the usual condition on the $\forall$-r rule, it is not
the case in this system, for the interpretation of the a nominal assertion in
a sequent is already implicitly universal (Definition 2).

$\mathord{\Delta,\delta}\Rightarrow\ \mathord{}$$\delta$ |  |  $\mathord{\Delta,x\colon\bot}\Rightarrow\ \mathord{}$$\delta$
---|---|---
$\mathord{\Delta,xRy}\Rightarrow\ \mathord{}$$y\colon\alpha$ $\forall$-r $\mathord{\Delta}\Rightarrow\ \mathord{}$$x\colon\forall R.\alpha$ |  |  $\mathord{\Delta,x\colon\forall R.\alpha,y\colon\alpha,xRy}\Rightarrow\ \mathord{}$$\delta$ $\forall$-l $\mathord{\Delta,x\colon\forall R.\alpha,xRy}\Rightarrow\ \mathord{}$$\delta$
$\mathord{\Delta}\Rightarrow\ \mathord{}$$xRy$ $\mathord{\Delta}\Rightarrow\ \mathord{}$$y\colon\alpha$ $\exists$-r $\mathord{\Delta}\Rightarrow\ \mathord{}$$x\colon\exists R.\alpha$ |  |  $\mathord{\Delta,xRy,y\colon\alpha}\Rightarrow\ \mathord{}$$\delta$ $\exists$-l $\mathord{\Delta,x\colon\exists R.\alpha}\Rightarrow\ \mathord{}$$\delta$
$\mathord{\Delta,\alpha}\Rightarrow\ \mathord{}$$\beta$ $\sqsubseteq$-r $\mathord{\Delta}\Rightarrow\ \mathord{}$$\alpha\sqsubseteq\beta$ |  |  $\mathord{\Delta_{1}}\Rightarrow\ \mathord{}$$\alpha$ $\mathord{\Delta_{2},\beta}\Rightarrow\ \mathord{}$$\delta$ $\sqsubseteq$-l $\mathord{\Delta_{1},\Delta_{2},\alpha\sqsubseteq\beta}\Rightarrow\ \mathord{}$$\delta$
$\mathord{\Delta}\Rightarrow\ \mathord{}$$\alpha$ $\mathord{\Delta}\Rightarrow\ \mathord{}$$\beta$ $\sqcap$-r $\mathord{\Delta}\Rightarrow\ \mathord{}$$\alpha\sqcap\beta$ |  |  $\mathord{\Delta,\alpha,\beta}\Rightarrow\ \mathord{}$$\delta$ $\sqcap$-l $\mathord{\Delta,\alpha\sqcap\beta}\Rightarrow\ \mathord{}$$\delta$
$\mathord{\Delta}\Rightarrow\ \mathord{}$$\alpha$ $\sqcup_{1}$-r $\mathord{\Delta}\Rightarrow\ \mathord{}$$\alpha\sqcup\beta$ |  |  $\mathord{\Delta,\alpha}\Rightarrow\ \mathord{}$$\delta$ $\mathord{\Delta,\beta}\Rightarrow\ \mathord{}$$\delta$ $\sqcup$-l $\mathord{\Delta,\alpha\sqcup\beta}\Rightarrow\ \mathord{}$$\delta$
$\mathord{\Delta,\alpha}\Rightarrow\ \mathord{}$$\beta$ p-$\exists$ $\mathord{\forall R.\Delta,\exists R.\alpha}\Rightarrow\ \mathord{}$$\exists R.\beta$ |  |  $\mathord{\Delta}\Rightarrow\ \mathord{}$$\alpha$ p-$\forall$ $\mathord{\forall R.\Delta}\Rightarrow\ \mathord{}$$\forall R.\alpha$
$\mathord{\Delta}\Rightarrow\ \mathord{}$$\delta$ p-N $\mathord{x\colon\Delta}\Rightarrow\ \mathord{}$$x\colon\delta$ |  |
Figure 2: The System $\textsf{SC}_{iALC}$: logical rules

###### Theorem 1

The sequent calculus described in Fig. 2 is sound and complete for TBox
reasoning, that is $\Theta,\emptyset\models C$ if and only if
$\Theta\Rightarrow C$ is derivable with the rules of Figure 2.

The completeness of our system is proved relative to the axiomatization of
$i\mathcal{ALC}$, shown in Figure 1. The proof is presented in Section 2.

The soundness of the system is proved directly from the semantics of
$i\mathcal{ALC}$ including the ABOX, that is, including nominals. The
semantics of a sequent is defined by the satisfaction relation, as shown in
Definition 2. The sequent $\Theta,\Gamma\Rightarrow\ \delta$ is valid if and
only if $\Theta,\Gamma\models\gamma$. Soundness is proved by showing that each
sequent rule preserves the validity of the sequent and that the initial
sequent is valid. This proof is presented in Section 3.

We note that although we have here fixed some inaccuracies in the presentation
of the $i\mathcal{ALC}$ semantics in [4], the system presented here is
basically the same, excepted that here the propositional rules are presented
without nominals. Given that, the soundness of the system proved in [4] can be
still considered valid without further problems. Note also that the proof of
soundness provides in Section 3 is regarded the full language of
$i\mathcal{ALC}$. It considers nominals and assertion on nominals
relationship, that is it concerns ABOX and TBOX. The proof of completeness is
for the TBOX only. A proof of completeness for ABOX can be done by the method
of canonical models. For the purposes of this article, we choose to show the
relative completeness proof with the sake of showing a simpler proof
concerning TBOX.

##  2 The completeness of $\textsf{SC}_{iALC}$ system

We show the relative completeness of $\textsf{SC}_{iALC}$ regarding the
axiomatic presentation of $i\mathcal{ALC}$ presented in Figure 1. To prove the
completeness of $\textsf{SC}_{iALC}$ it is sufficient to derive in
$\textsf{SC}_{iALC}$ the axioms 1–5 of $i\mathcal{ALC}$. It is clear that all
substitution instances of IPL theorems can also be proved in
$\textsf{SC}_{iALC}$ using only propositional rules. The MP rule is a derived
rule from the $\textsf{SC}_{iALC}$ using the cut rule. The Nec rule is the
p-$\forall$ rule in the system with $\Delta$ empty. In the first two proofs
below do not use nominals for given better intuition of the reader about the
use of rules with and without nominals.

Axiom 1:

$\mathord{\alpha}\Rightarrow\ \mathord{}$$\alpha$ $\mathord{\beta}\Rightarrow\
\mathord{}$$\beta$ $\sqsubseteq$-l
$\mathord{\alpha\sqsubseteq\beta,\alpha}\Rightarrow\ \mathord{}$$\beta$
p-$\exists$ $\mathord{\forall R.(\alpha\sqsubseteq\beta),\exists
R.\alpha}\Rightarrow\ \mathord{}$$\exists R.\beta$ $\sqsubseteq$-r
$\mathord{\forall R.(\alpha\sqsubseteq\beta)}\Rightarrow\ \mathord{}$$\exists
R.\alpha\sqsubseteq\exists R.\beta$

Axiom 2:

$\mathord{\alpha}\Rightarrow\ \mathord{}$$\alpha$ $\mathord{\beta}\Rightarrow\
\mathord{}$$\beta$ $\sqsubseteq$-l
$\mathord{\alpha\sqsubseteq\beta,\alpha}\Rightarrow\ \mathord{}$$\beta$
p-$\forall$ $\mathord{\forall R.(\alpha\sqsubseteq\beta),\forall
R.\alpha}\Rightarrow\ \mathord{}$$\forall R.\beta$ $\sqsubseteq$-r
$\mathord{\forall R.(\alpha\sqsubseteq\beta)}\Rightarrow\ \mathord{}$$\forall
R.\alpha\sqsubseteq\forall R.\beta$

Axiom 3:

$\mathord{xRy,y:\bot}\Rightarrow\ \mathord{}$$x:\bot$ $\exists$-l
$\mathord{x:\exists R.\bot}\Rightarrow\ \mathord{}$$x:\bot$ $\sqsubseteq$-r
$\mathord{}\Rightarrow\ \mathord{}$$x:(\exists R.\bot\sqsubseteq\bot)$

Axiom 4:

$\mathord{x:\exists R.\alpha}\Rightarrow\ \mathord{}$$x:\exists R.\alpha$
$\sqcup_{1}$-r $\mathord{x:\exists R.\alpha}\Rightarrow\
\mathord{}$$x:(\exists R.\alpha\sqcup\exists R.\beta)$ $\mathord{x:\exists
R.\beta}\Rightarrow\ \mathord{}$$x:\exists R.\beta$ $\sqcup_{2}$-r
$\mathord{x:\exists R.\beta}\Rightarrow\ \mathord{}$$x:(\exists
R.\alpha\sqcup\exists R.\beta)$ $\sqcup$-l $\mathord{x:\exists
R.(\alpha\sqcup\beta)}\Rightarrow\ \mathord{}$$x:(\exists
R.\alpha\sqcup\exists R.\beta)$

Axiom 5:

$xRy,y:\alpha\Rightarrow\ y:\alpha$ $xRy,y:\alpha\Rightarrow\ xRy$ $\exists$-r
$xRy,y:\alpha\Rightarrow\ {\color[rgb]{1,0,0}x:}\exists R.\alpha$
$xRy,y:\alpha,y:\beta,\forall R.\beta\Rightarrow\ y:\beta$ $\forall$-l
$xRy,y:\alpha,{\color[rgb]{1,0,0}x:}\forall R.\beta\Rightarrow\ y:\beta$
$\sqsubseteq$-l $x:(\exists R.\alpha\sqsubseteq\forall
R.\beta),xRy,y:\alpha\Rightarrow\ y:\beta$ $\forall$-r $x:(\exists
R.\alpha\sqsubseteq\forall R.\beta),xRy\Rightarrow\
y:(\alpha\sqsubseteq\beta)$ $\forall$-r $x:(\exists R.\alpha\sqsubseteq\forall
R.\beta)\Rightarrow\ x:\forall R.(\alpha\sqsubseteq\beta)$ $\sqsubseteq$-r
$\Rightarrow\ x:[(\exists R.\alpha\sqsubseteq\forall
R.\beta)\sqsubseteq\forall R.(\alpha\sqsubseteq\beta)]$

##  3 Soundness of $\textsf{SC}_{iALC}$ system

In this section we prove that.

###### Proposition 1

If $\Theta,\Gamma\Rightarrow\ \delta$ is provable in $\textsf{SC}_{iALC}$ then
$\Theta,\Gamma\models\gamma$.

Proof: We prove that each sequent rule preserves the validity of the sequent
and that the initial sequents are valid. The definition of a valid sequent
($\Theta,\Gamma\models\gamma$) is presented in Definition 2.

The validity of the axioms is trivial. We first observe that any application
of the rules $\sqsubseteq$-r, $\sqsubseteq$-l,$\sqcap$-r,$\sqcap$-l,
$\sqcup_{1}$-r,$\sqcup_{2}$-r, $\sqcup$-l of $\textsf{SC}_{iALC}$ where the
sequents do not have any nominal, neither in $\Theta$ nor in $\Gamma$, is
sound regarded intuitionistic propositional logic kripke semantics, to which
the validity definition above collapses whenever there is no nominal in the
sequents. Thus, in this proof we concentrate in the case where there are
nominals. We first observe that the nominal version of $\sqsubseteq$-r, the
validity of the premises includes

$\forall(Nom(\Gamma,\delta)).\forall\vec{z}\succeq Nom(\Gamma,\delta).({\cal
I},\vec{z}\models\Gamma\Rightarrow{\cal I},\vec{z}\models\delta)$

This means that $\Gamma$ holds in any worlds $\vec{z}\succeq\vec{x}$ for the
vector $\vec{x}$ of nominals occurring in $\Gamma$. This includes the outer
nominal $x_{i}$ in $\delta$ (if any). In this case the semantics of
$\sqsubseteq$ is preserved, since $\vec{z}$ includes $z_{i}\succeq x_{i}$.
With the sake of a more detailed analysis, we consider the following instance:

$\mathord{x:\alpha_{1},y:\alpha_{2}}\Rightarrow\ \mathord{}$$x:\beta$
$\sqsubseteq$-r $\mathord{\alpha_{1}}\Rightarrow\
\mathord{}$$x:\alpha_{2}\sqsubseteq\beta$

Consider an $i\mathcal{ALC}$ structure ${\cal I}=\langle{\cal
U},\preceq,R^{\cal I}\ldots,C^{\cal I}\rangle$ In this case, for any ${\cal
I}$ and any $z_{1},z_{2}\in{\cal U}^{\cal I}$ if $z_{1}\succeq x^{\cal I}$,
$z_{1}\succeq y^{\cal I}$, such that, ${\cal I},z_{i}\models\alpha_{1}$ and
${\cal I},z_{i}\models\alpha_{2}$, we have that ${\cal I},z_{i}\models
x:\beta$, since the premise is valid, by hypothesis. In this case, by the
semantics of $\sqsubseteq$ we have ${\cal I},z_{i}\models
x:\alpha_{1}\sqsubseteq\beta$. The conclusion of the rule is valid too.

The argument shown above for the $\sqsubseteq$-r rule is analogous for the
nominal versions of $\sqsubseteq$-r, $\sqsubseteq$-l,$\sqcap$-r,$\sqcap$-l,
$\sqcup_{1}$-r,$\sqcup_{2}$-r, $\sqcup$-l. Consider the rule $\forall$-r.

$\mathord{\Delta,xRy}\Rightarrow\ \mathord{}$$y\colon\alpha$ $\forall$-r
$\mathord{\Delta}\Rightarrow\ \mathord{}$$x\colon\forall R.\alpha$

Since the premise is valid we have that if $\forall z_{x}\succeq x^{\cal I}$,
$\forall z_{y}\succeq y^{\cal I}$, $(z_{x},z_{y})\in R^{\cal I}$ then $\forall
z_{y}\succeq y^{\cal I}.{\cal I},z_{y}\models\gamma$. This entails that
$x^{\cal I}\in(\forall R.\gamma)^{\cal I}$, for $x^{\cal I}\succeq x^{\cal
I}$. We observe that by the restriction on the rule application, $y$ does not
occur in $\Delta$, it only occurs in $xRy$ and $y:\alpha$. The truth of these
formulas are subsumed by $\forall R.\gamma$. The conclusion does not need to
consider them any more. The conclusion is valid too. Another way to see its
soundness is to prove that if $xRy\Rightarrow y:\alpha$ is valid, then so is
$\Rightarrow x:\forall R.\alpha$. This can be show by the following reasoning:

$\forall x^{\cal I}\forall y^{\cal I}\forall z_{x}\forall z_{y}(z_{x}\succeq
x^{\cal I}\rightarrow(z_{y}\succeq y^{\cal I}\rightarrow((z_{x},z_{y})\in
R^{\cal I}\rightarrow{\cal I},z_{y}\models y:\alpha)))$

that is the same as:

$\forall x^{\cal I}\forall y^{\cal I}\forall z_{x}\forall z_{y}(z_{x}\succeq
x^{\cal I}\rightarrow(z_{y}\succeq y^{\cal I}\rightarrow((z_{x},z_{y})\in
R^{\cal I}\rightarrow{\cal I},y^{\cal I}\models\alpha)))$

Using the fact that $\forall y^{\cal I}(y^{\cal I}\succeq y^{\cal I})$, we
obtain:

$\forall x^{\cal I}\forall z_{x}(z_{x}\succeq x^{\cal I}\rightarrow\forall
y^{\cal I}((z_{x},y^{\cal I})\in R^{\cal I}\rightarrow{\cal I},y^{\cal
I}\models\alpha))$

The above condition states that $\Rightarrow x:\forall R.\alpha$ is valid.

$\forall x^{\cal I}\forall y^{\cal I}\forall z_{x}\forall z_{y}(z_{x}\succeq
x^{\cal I}\rightarrow(z_{y}\succeq y^{\cal I}\rightarrow((z_{x},z_{y})\in
R^{\cal I}\rightarrow{\cal I},z_{y}\models y:\alpha)))$

Consider the rule $\forall$-l:

$\mathord{\Delta,x\colon\forall R.\alpha,y\colon\alpha,xRy}\Rightarrow\
\mathord{}$$\delta$ $\forall$-l $\mathord{\Delta,x\colon\forall
R.\alpha,xRy}\Rightarrow\ \mathord{}$$\delta$

As in the $\forall$-r case, we analyze the simplest validity preservation: if
$x:\forall R.\alpha\land xRy$ is valid, then so is $x:\forall R.\alpha\land
y:\alpha\land xRy$. The first condition is:

$\forall x^{\cal I}\forall y^{\cal I}\forall z_{x}(z_{x}\succeq x^{\cal
I}\rightarrow\forall z_{y}(z_{y}\succeq y^{\cal I}\rightarrow\\\ (({\cal
I},z_{y}\models x:\forall R.\alpha)\land({\cal I},z_{y}\models x:\forall
R.\alpha)\land((z_{x},z_{y})\in R^{\cal I})\rightarrow\\\ ({\cal
I},z_{y}\models y:\alpha)\land({\cal I},z_{x}\models y:\alpha))))$ (2)

Using $z_{y}=y^{\cal I}$, eliminating $z_{x}$ from the term, and, using the
fact that ${\cal I},z_{y}\models y:\alpha$ is valid, iff, ${\cal I},y^{\cal
I}\models\alpha$ , we obtain

$\forall x^{\cal I}\forall y^{\cal I}\forall z_{x}(z_{x}\succeq x^{\cal
I}\rightarrow\forall z_{y}(z_{y}\succeq y^{\cal I}\rightarrow\\\ (({\cal
I},z_{y}\models x:\forall R.\alpha)\land({\cal I},z_{y}\models x:\forall
R.\alpha)\land((z_{x},z_{y})\in R^{\cal I})\rightarrow({\cal
I},y\models\alpha))))$ (3)

Consider the semantics of $\exists R.\alpha$:

$(\exists R.\alpha)^{\cal I}=_{df}\\{x\mid\exists y\in{\cal U}^{\cal
I}.(x,y)\in R^{\cal I}\mbox{ and }y\in\alpha^{\cal I}\\}$

and the following rule:

$\mathord{\Delta}\Rightarrow\ \mathord{}$$xRy$ $\mathord{\Delta}\Rightarrow\
\mathord{}$$y\colon\alpha$ $\exists$-r $\mathord{\Delta}\Rightarrow\
\mathord{}$$x\colon\exists R.\alpha$

We can see that the premises of the rule entails the conclusion. The premises
correspond to the following conditions:

$\forall x^{\cal I}\forall y^{\cal I}\forall z_{x}(z_{x}\succeq x^{\cal
I}\rightarrow\forall z_{y}(z_{y}\succeq y^{\cal I}\rightarrow((z_{x},z_{y})\in
R^{\cal I})))$

and

$\forall y^{\cal I}\forall z_{y}(z_{y}\succeq y^{\cal I}\rightarrow(({\cal
I},z_{y}\models y:\alpha)))$

Instantiating in both conditions $z_{y}=y^{\cal I}$ and $z_{x}=x^{\cal I}$,
this yields $(x^{\cal I},y^{\cal I})\in R^{\cal I}$, such that ${\cal
I},y^{\cal I}\models\alpha$, so ${\cal I},z_{x}\models x^{\cal I}:\exists
R.\alpha$. Thus, $\exists$-r is sound. The soundness of $\exists$-l is
analogous to $\forall$-l.

Finally, it is worth noting that, for each rule, we can derive the soundness
of its non-nominal version from the proof of soundness of its nominal version.
For instance, the soundness of the nominal version of rule $\sqcup$-l depends
on the diamond conditions F1 and F2. The soundness of its non-nomimal version,
is a consequence of the soundness of the nominal version.

The rules below have their soundness proved as a consequence of the following
reasonings in first-order intuitionistic logic that are used for deriving the
semantics of the conclusions from the semantics of the premises:

(p-$\exists$)

$\forall x(A(x)\land B(x)\rightarrow C(x))\models\forall xA(x)\land\exists
xB(x)\rightarrow\exists xC(x)$;

(p-$\forall$)

$(A(x)\models B(x))$ implies $\forall y(R(y,x)\rightarrow A(x))\models\forall
y(R(y,x)\rightarrow B(x))$;

(p-N)

if $A\models B$ then for every Kripke model ${\cal I}$ and world $x^{\cal I}$,
if ${\cal I},x^{\cal I}\models A$ then ${\cal I},x^{\cal I}\models B$.

$\mathord{\Delta,\alpha}\Rightarrow\ \mathord{}$$\beta$ p-$\exists$ $\mathord{\forall R.\Delta,\exists R.\alpha}\Rightarrow\ \mathord{}$$\exists R.\beta$ |  $\mathord{\Delta}\Rightarrow\ \mathord{}$$\delta$ p-N $\mathord{x\colon\Delta}\Rightarrow\ \mathord{}$$x\colon\delta$
---|---

## References

  * [1] T. Braüner and Valéria de Paiva.  Intuitionistic hybrid logic.  JAL, 4(3):231–255, 2006.
  * [2] Samuel R Buss.  Handbook of proof theory.  Elsevier, 1998.
  * [3] Valeria de Paiva.  Constructive description logics:what, why and how.  In Context Representation and Reasoning, 2006.
  * [4] Valeria de Paiva, Edward Hermann Hausler, and Alexandre Rademaker.  Constructive description logic: Hybrid-style.  In Proc. HyLo’2010, 2010.
  * [5] G. Fischer-Servi.  Axiomatizations for some intuitionistic modal logics.  Rendiconti del Seminario Matematico Università e Politecnico di Torino, 42, 1984.
  * [6] J.Y. Girard, P. Taylor, and Y. Lafont.  Proofs and Types.  Cambridge Tracts in Theoretical Computer Science 7. Cambridge University Press, 1989.
  * [7] Edward H. Haeusler, Valeria de Paiva, and Alexandre Rademaker.  Intuitionistic description logic and legal reasoning.  In Proceedings of International Workshop Data, Logic and Inconsistency with DEXA 2011, 2011.
  * [8] Edward Hermann Haeusler, Valeria de Paiva, and Alexandre Rademaker.  Intuitionistic logic and legal ontologies.  In JURIX 2010: The Twenty-Third Annual Conference on Legal Knowledge and Information Systems, Frontiers in Artificial Intelligence and Applications, pages 155–158, Liverpool, UK, 2010. IOS Press.
  * [9] Edward Hermann Haeusler, Valeria de Paiva, and Alexandre Rademaker.  Using intuitionistic logic as a basis for legal ontologies.  In Proceedings of the 4th Workshop on Legal Ontologies and Artificial Intelligence Techniques, pages 69–76, Fiesole, Florence, Italy, 2010\. European University Institute.
  * [10] Edward Hermann Haeusler, Valeria De Paiva, and Alexandre Rademaker.  Using intuitionistic logic as a basis for legal ontologies.  Informatica e Diritto, 1(2), 2010.  also published at Proceedings of the 4th Workshop on Legal Ontologies and Artificial Intelligence Techniques, Fiesole, Florence, Italy.
  * [11] Michael Mendler and Stephan Scheele.  Towards constructive DL for abstraction and refinement.  JAR, 44(3):207–243, 2010.  Proc. 21st International DL Workshop.
  * [12] Sara Negri and Jan Von Plato.  Structural proof theory.  Cambridge University Press, 2008.
  * [13] Gordon Plotkin and Colin Stirling.  A framework for intuitionistic modal logics: extended abstract.  In Proceedings of the 1986 conference on Theoretical aspects of reasoning about knowledge, TARK ’86, pages 399–406, San Francisco, CA, USA, 1986\. Morgan Kaufmann Publishers Inc.
  * [14] Alex Simpson.  The Proof Theory and Semantics of Intuitionistic Modal Logic.  PhD thesis, University of Edinburgh, December 1993.
  * [15] Gaisi Takeuti.  Proof theory.  Courier Dover Publications, 2013.