Valentin Vielzeuf
email: valentin.vielzeuf@orange.com

Stéphane Pateux
email: stephane.pateux@orange.com

Frédéric Jurie
email: frederic.jurie@unicaen.fr

Temporal Multimodal Fusion for Video Emotion Classification in the Wild

Keywords: Emotion Recognition, Multimodal Fusion, Recurrent Neural Network, Deep Learning

This paper addresses the question of emotion classification. The task consists in predicting emotion labels (taken among a set of possible labels) best describing the emotions contained in short video clips. Building on a standard framework -lying in describing videos by audio and visual features used by a supervised classifier to infer the labels -this paper investigates several novel directions. First of all, improved face descriptors based on 2D and 3D Convolutional Neural Networks are proposed. Second, the paper explores several fusion methods, temporal and multimodal, including a novel hierarchical method combining features and scores. In addition, we carefully reviewed the different stages of the pipeline and designed a CNN architecture adapted to the task; this is important as the size of the training set is small compared to the difficulty of the problem, making generalization difficult. The so-obtained model ranked 4th at the 2017 Emotion in the Wild challenge with the accuracy of 58.8 %.

INTRODUCTION AND RELATED WORK

Emotion recognition is a topic of broad and current interest, useful for many applications such as advertising [START_REF] Kołakowska | Emotion recognition and its application in software engineering[END_REF] or psychological disorders understanding [START_REF] Washington | A wearable social interaction aid for children with autism[END_REF]. It is also a topic of importance for research in other areas e.g., video summarization [START_REF] Xu | Heterogeneous knowledge transfer in video emotion recognition, attribution and summarization[END_REF] or face normalization (expression removal). Even if emotion recognition could appear to be an almost solved problem in laboratory controlled conditions, there are still many challenging issues in the case of videos recorded in the wild.

This paper focuses on the task of emotion classification in which each video clip has to be assigned to one and only one emotion, based on its audio/video content. The classes are usually the six basic emotions i.e., anger, disgust, fear, happiness, sadness and surprise, in addition to the neutral class, as in the Audio-video Emotion Recognition sub-task of the Emotion Recognition in the Wild Challenge [START_REF] Dhall | Collecting Large, Richly Annotated Facial-Expression Databases from Movies[END_REF]. More precisely, this paper presents our methodology, experiments as well as the results we obtained in the 2017 edition of the Emotion Recognition in the Wild Challenge [START_REF] Dhall | From Individual to Group-level Emotion Recognition: EmotiW 5.0[END_REF].

Emotion recognition has received a lot of attention in the scientific literature. One large part of this literature deals with the possible options for defining and representing emotions. If the use of discrete classes [31] such as joy, fear, angriness, etc. is the most * Also with Normandie Univ., UNICAEN, ENSICAEN, CNRS. straightforward way to do it, it can be more interesting to represent emotions by their degrees of arousal and valence, as proposed in [START_REF] Feldman | The structure of current affect: Controversies and emerging consensus[END_REF]. In the restricted case of facial expressions, action units can also be used, focusing on the activation of different parts of the face [START_REF] Ekman | Facial action coding system[END_REF]. Links can be made between these two representations: the discrete classes can be mapped into the arousal valence space [START_REF] Kossaifi | AFEW-VA database for valence and arousal estimation in-the-wild[END_REF] and can be deduced from the action units [START_REF] Khorrami | Do deep neural networks learn facial action units when doing expression recognition?[END_REF].

Another important part of the literature focuses on the ways to represent audio/video contents by features that can be subsequently used by classifiers. Early papers make use of (i) hand-crafted features such as Local Binary Patterns (LBP), Gabor features, discrete cosine transform for representing images, and Linear Predictive Coding coefficients (LPC), relative spectral transform -linear perceptual prediction (RASTA-PLP), modulation spectrum (ModSpec) or Enhanced AutoCorrelation (EAC) for audio, (ii) standard classifiers such as SVN or KNN for classification (see [START_REF] Kächele | Revisiting the EmotiW challenge: how wild is it really?[END_REF] for details). [START_REF] Yao | Capturing au-aware facial features and their latent relations for emotion recognition in the wild[END_REF], the winner of EmotiW'15, demonstrated the relevance of Action Units for the recognition of emotions. [START_REF] Baccouche | Spatio-Temporal Convolutional Sparse Auto-Encoder for Sequence Classification[END_REF] was among the first to propose to learn the features instead of using hand-crafted descriptors, relying on Deep Convolutional Networks. More recently, [START_REF] Fan | Video-based emotion recognition using cnn-rnn and c3d hybrid networks[END_REF], the winner of EmotiW'16, has introduced the C3D feature which is an efficient spatio-temporal representation of faces.

The literature on emotion recognition from audio/video contents also addresses the question of the fusion of the different modalities. A modality can be seen as one of the signals allowing to perceive the emotion. Among the recent methods for fusing several modalities, we can mention the use of two-stream ConvNets [START_REF] Simonyan | Two-Stream Convolutional Networks for Action Recognition in Videos[END_REF], ModDrop [START_REF] Neverova | Moddrop: adaptive multi-modal gesture recognition[END_REF] or Multiple Kernel Fusion [START_REF] Chen | Emotion recognition in the wild with feature fusion and multiple kernel learning[END_REF]. The most used modalities, in the context of emotion recognition, are face images and audio/speech, even if context seems also to be of tremendous importance [START_REF] Feldman | Context in emotion perception[END_REF]. For instance, the general understanding of the scene, even based on simple features describing the whole image, may help to discriminate between two candidate classes.

As most of the recent methods for emotion recognition are supervised and hence requires some training data, the availability of such resources is becoming more and more critical. Several challenges have collected useful data. The AVEC challenge [START_REF] Valstar | Avec 2016: Depression, mood, and emotion recognition workshop and challenge[END_REF] focuses on the use of several modalities to track arousal and valence in videos recorded in controlled conditions. The Emotionet challenge [START_REF] Benitez-Quiroz | EmotioNet Challenge: Recognition of facial expressions of emotion in the wild[END_REF] proposes a dataset of one million images annotated with action units and partially with discrete compound emotion classes. Finally, the Emotion in the Wild challenge [START_REF] Dhall | Emotiw 2016: Video and group-level emotion recognition challenges[END_REF] deals with the classification of short video clips into seven discrete classes. The videos are extracted from movies and TV shows recorded "in the wild". The ability to work with data recorded in realistic situations, including occlusions, poor illumination conditions, presence of several people or even scene breaks is indeed very important.

As aforementioned, this paper deals with our participation to the Emotion In the Wild 2017 (EmotiW) challenge. We build on the state-of-the-art pipeline of [START_REF] Fan | Video-based emotion recognition using cnn-rnn and c3d hybrid networks[END_REF] in which i) audio features are extracted with the OpenSmile toolkit [START_REF] Eyben | Opensmile: the munich versatile and fast open-source audio feature extractor[END_REF], ii) two video features are computed, one by the C3D descriptor, the other by the VGG16-Face model [START_REF] Omkar M Parkhi | Deep Face Recognition[END_REF] fine-tuned with FER2013 face emotion database and introduced into a LSTM network. Each one of these 3 features is processed by its own classifier, the output of the 3 classifiers being combined through late fusion. Starting from this pipeline, we propose to improve it in 3 different ways, which are the main contributions of our approach.

First, the recent literature suggests that late fusion might not be the optimal way to combine the different modalities (see e.g., [START_REF] Neverova | Moddrop: adaptive multi-modal gesture recognition[END_REF]). This paper investigates different directions, including an original hierarchical approach allowing to combine scores (late fusion) and features (early fusion) at different levels. It can be seen as a way to combine information at its optimal level of description (from features to scores). This representation addresses an important issue of fusion, which is to ensure the preservation of unimodal information while being able to exploit cross-modal information.

Second, we investigate several ways to better use the temporal information in the visual descriptors. Among several contributions, we propose a novel descriptor combining C3D and LSTM.

Third, it can be observed that the amount of training data (773 labeled short video clips) is rather small compared to the number of the parameters of standard deep models, considering the complexity and diversity of emotions. In this context, supervised methods are prone to over-fitting. We show in the paper how the effect of over-fitting can be reduced by carefully choosing the number of parameters of the model and favoring transfer learning whenever it is possible. The rest of the paper is organized as follows: a presentation of the proposed model is done in Section 2, detailing the different modalities and the fusion methods. Then Section 3 presents the experimental validation as well as the results obtained on the validation and test sets during the challenge.

PRESENTATION OF THE PROPOSED APPROACH

Figure 3 presents an overview of our approach, which is inspired by the one of [START_REF] Fan | Video-based emotion recognition using cnn-rnn and c3d hybrid networks[END_REF]. Modalities we consider are extracted from audio and video, associated with faces analyzed with two different models (2D CNN, C3D). The two main contributions are the temporal fusion and the novel C3D/LSTM descriptor. On overall, our method works as follows: on the one hand, the OpenSmile library [START_REF] Eyben | Opensmile: the munich versatile and fast open-source audio feature extractor[END_REF] is used to produce 1582 dimensional features used by a two-layer perceptron to predict classes as well as compact descriptors (279-d vectors) from audio. On the other hand, video classification is based on face analysis. After detecting the faces and normalizing their appearance, one set of features is computed with the VGG-16 model [START_REF] Omkar M Parkhi | Deep Face Recognition[END_REF] while another set of features is obtained by the C3D model [START_REF] Fan | Video-based emotion recognition using cnn-rnn and c3d hybrid networks[END_REF]. In both cases, 4096-d features are produced. Temporal fusion of these so-obtained descriptions is done across the frames of the sequences, producing per modality scores and compact descriptors (304 dimensional vectors). The 3 modalities (audio, VGG-faces and C3D-faces) are then combined using both the score predictions and the compact representations.

After explaining how the faces are detected and normalized, the rest of the section gives more details on how each modality is processed, and how the fusion is performed.

Face Detection and Alignment

The EmotiW challenge provides face detections for each frame of each video. However, we preferred not to use these annotations but to detect the faces ourselves. The motivation is twofold. First, we want to be able to process any given video and not only those of EmotiW (e.g., for adding external training data). Second, it is necessary to master the face alignment process for processing the For face detection, we use an internal detector provided by Orange Labs. We found out from our observations that this face detector detects more faces (20597 versus 19845 on the validation set) while having a lower false positive rate (179 false positives versus 908 on the validation set) than the one use to provide EmotiW annotations.

This detector is applied frame per frame. If one or several faces are detected, a tracking based on their relative positions allows to define several face tracks. In a second time, an alignment based on the landmarks [START_REF] Davis | Dlib-ml: A machine learning toolkit[END_REF] is done. We choose the longest face sequence in each video and finally apply a temporal smoothing of the positions of the faces to filter out jittering.

Figure 2 compares one of our normalized faces (after detection / alignment) with the one provided with the challenge data.

Audio features and classifier

The audio channel of each video is fed into the OpenSmile toolkit [START_REF] Eyben | Opensmile: the munich versatile and fast open-source audio feature extractor[END_REF] 1 , as most of the EmotiW competitors [START_REF] Dhall | Emotiw 2016: Video and group-level emotion recognition challenges[END_REF], to get a description vector of length 1582.

A commonly used approach for audio is then to learn a classifier on top of the OpenSmile features. Support Vector Machine [START_REF] Fan | Video-based emotion recognition using cnn-rnn and c3d hybrid networks[END_REF] [START_REF] Yao | Capturing au-aware facial features and their latent relations for emotion recognition in the wild[END_REF] seems to be the dominant choice for the classification, even if there are some other approaches like Random Forests [START_REF] Fan | Spatiotemporal Networks for Video Emotion Recognition[END_REF].

To be able to control more finely the dimensionality of the description vector (the one used later on during the fusion process), we learn a two-layer Perceptron with reLu activation on the OpenSmile description, using batch normalisation and dropout. During inference, we extract for each video a description vector of size 279 -the hidden layer of the perceptron -along with the softmax score.

Representing Faces with 2D Convolutional Neural Network

A current popular method (see e.g., [START_REF] Fan | Video-based emotion recognition using cnn-rnn and c3d hybrid networks[END_REF][START_REF] Kaya | Video-based emotion recognition in the wild using deep transfer learning and score fusion[END_REF]) for representing faces in the context of emotion recognition, especially in the EmotiW challenge, is to fine-tune a pre-trained 2D CNN such as the VGGface model [START_REF] Omkar M Parkhi | Deep Face Recognition[END_REF] on the images of an emotion images dataset (e.g., the FER 2013 dataset). Using a pre-trained model is a way to balance the relatively small size of the EmotiW dataset (AFEW dataset). The images of the FER 2013 dataset [START_REF] Goodfellow | Challenges in representation learning: A report on three machine learning contests[END_REF] are first processed by detecting and aligning the faces, following the procedure explained in Section 2.1. We then fine-tune the VGG-face model on FER 2013 dataset, using both the training and the public test set; during training we use data augmentation by jittering the scale, flipping and rotating the faces. The aim is to make the network more robust to small misalignment of the faces. We also apply a strong dropout on the last layer of the VGG (keeping only 5% of the nodes) to prevent over-fitting. We achieve a performance of 71.2% on the FER private test set, which is slightly higher than the previously published results [START_REF] Fan | Video-based emotion recognition using cnn-rnn and c3d hybrid networks[END_REF][START_REF] Goodfellow | Challenges in representation learning: A report on three machine learning contests[END_REF].

To assess the quality of the description given by this fine-tuned VGG model to emotion recognition, we first benchmarked it on the validation set of SFEW [START_REF] Dhall | Video and image based emotion recognition challenges in the wild: Emotiw 2015[END_REF], which is a dataset containing frames of the videos of AFEW (those used by the EmotiW challenge). We achieved a score of 45.2% without retraining the model on SFEW, while the state-of-the-art result [START_REF] Kim | Hierarchical committee of deep convolutional neural networks for robust facial expression recognition[END_REF] is 52.5%, using a committee of deep models, and the challenge baseline is of 39.7% [START_REF] Dhall | Video and image based emotion recognition challenges in the wild: Emotiw 2015[END_REF].

The face sequences detected in AFEW videos are resized to 224x224 and fed into the fine-tuned VGG-face model. We then extract the 4096 length fc6 layer, following the same pipeline as Fan et al. [START_REF] Fan | Spatiotemporal Networks for Video Emotion Recognition[END_REF][START_REF] Fan | Video-based emotion recognition using cnn-rnn and c3d hybrid networks[END_REF]. We also compute the softmax score for each frame.

Representing Faces with 3D Convolutional

Neural Network 3D convolutional neural networks have been shown to give good performance in the context of facial expressions recognition in video [START_REF] Baccouche | Sequential deep learning for human action recognition[END_REF][START_REF] Tran | Learning spatiotemporal features with 3d convolutional networks[END_REF]. Fan et al. [START_REF] Fan | Video-based emotion recognition using cnn-rnn and c3d hybrid networks[END_REF] fine-tuned a pre-trained 'sport1m' model on randomly chosen windows of 16 consecutive faces. During inference, the model is applied to the central frame of the video. One limitation of this approach is that, at test time, there is no guaranty that the best window for capturing the emotion is in the middle of the video. The same problem occurs during training: a large part of the windows (randomly) selected for training does not contain any emotion or does not contain the correct emotion. Indeed, videos are annotated as a whole but some frames can have different labels or, sometimes, no expression at all.

We address this limitation in the following way: we first finetune a C3D-sport1m model using all the windows of each video, optimizing the classification performance until the beginning of convergence. Then, to be able to learn more from the most meaningful windows than from the others, we weigh each window based on its scores. More precisely, for the i t h video and the j th window of this video, at epoch t, the weight w i, j is computed as:

w i, j = e -s i, j T (t ) (1)
where T (t) is a temperature parameter decreasing with epoch t and s i, j , the score of the window j of the video i. We then normalize the weight to ensure that for each video i, j w i, j = 1. A random grid search on the hyper-parameters, including the temperature descent, is made on the validation set. During inference, the face sequences detected in AFEW videos are resized to 112x112. We then split a video into several windows of 16 consecutive frames2 , with or without overlapping between the windows (as shown in Figure 4), and fed it into the weighted C3D. We then extract the second 4096-d fully connected layer and the last softmax layer of the C3D for each window of the videos.

The method we propose bears similarities with Multiple Instance Learning (MIL) [START_REF] Ali | Human action recognition in videos using kinematic features and multiple instance learning[END_REF]. Within the framework of MIL, each video can be considered as a bag of windows, with one single label. A straightforward way to apply MIL would be to train the C3D on each video as a bag of windows, and add a final layer for choosing the prediction as the one with the maximum score among all the scores of the batch. The loss would be then computed from this prediction. The weights defined in Eq.( 1) play this role by selecting iteratively the best scoring windows.

Per Modality Temporal Fusion

Both VGG and weighted C3D representations are applied to each frame of the videos, turning the videos into temporal sequences of visual descriptors. We will name the elements of those sequences as "descriptors", whether it is the description of a frame or of a window.

To classify these sequences of descriptors, we investigated several methods. The most straightforward one is to score each descriptor and to take the maximum of the softmax scores as the final prediction. Similarly, the maximum of the means of the softmax across time can also be considered.

To better take into account temporal dependencies between consecutive descriptors, another option is to use Long Short-Term Memory recurrent neural networks (LSTM) [START_REF] Baccouche | Sequential deep learning for human action recognition[END_REF][START_REF] Felix A Gers | Learning to forget: Continual prediction with LSTM[END_REF]. Unlike [START_REF] Fan | Spatiotemporal Networks for Video Emotion Recognition[END_REF][START_REF] Fan | Video-based emotion recognition using cnn-rnn and c3d hybrid networks[END_REF], we chose to use a variable length LSTM allowing us to take all the descriptors as inputs.

To prevent over-fitting, we also applied dropout to the LSTM cells and weight decay to the final fully connected layer. A random grid search on hyper-parameters is then applied for each one of these models.

Both VGG-LSTM and C3D-LSTM are used to give one description vector (output of the final fully connected layer of the LSTM) and one softmax score for each video.

The final VGG-LSTM architecture has 2230 hidden units for each LSTM-cell and a final fully connected layer with 297 hidden units. The maximal length of the input sequence is of 272 frames.

The final C3D-LSTM architecture has 1324 hidden units for each LSTM-cell and a final fully connected layer of 304 hidden units. The maximal length of the input sequence is of 34 windows (overlap of 8 frames) or 17 windows (no overlap).

Multimodal fusion

Last but not the least, the different modalities have to be efficiently combined to maximize the overall performance.

As explained in Section 1, two main fusion strategies can be used i.e. score fusion (late fusion), which consists in predicting the labels based on the predictions given by each modality, or features fusion (early fusion), which consists in taking as input the latent features vectors given by each modality and learning a classifier on the top of them.

During the last editions of the challenge, most of the papers focused on score fusion, using SVM [START_REF] Sarah | Emotion recognition in the wild from videos using images[END_REF], Multiple Kernel Fusion [START_REF] Chen | Emotion recognition in the wild with feature fusion and multiple kernel learning[END_REF] or weighted means [START_REF] Fan | Video-based emotion recognition using cnn-rnn and c3d hybrid networks[END_REF]. Differently, several authors tried to train audio and image modalities together (see e.g., [START_REF] Chao | Audio visual emotion recognition with temporal alignment and perception attention[END_REF]), combining early features and using soft attention mechanism, but they didn't achieve state-of-the-art performance. We propose an approach combining both.

The rest of the section describes the four different fusion methods we experimented with, including a novel method (denominated as score trees).

Baseline score fusion. We experimented with several standard score fusion, like majority voting, means of the scores, maximum of the scores and linear SVM.

Fully connected neural network with modality drop. We also experimented with the ModDrop method of Neverova et al. [START_REF] Neverova | Moddrop: adaptive multi-modal gesture recognition[END_REF]. It consists in applying dropout by modality, learning the crossmodality correlations while keeping unimodal information. [START_REF] Neverova | Moddrop: adaptive multi-modal gesture recognition[END_REF] reports state-of-the-art results on gesture recognition. We apply this method to our audio, C3D-LSTM and VGG-LSTM features, as shown in Figure 5. According to [START_REF] Neverova | Moddrop: adaptive multi-modal gesture recognition[END_REF], this is much better than simply feeding the concatenation of the modalities features into a fully connected neural network and letting the network learn a joint representation. Indeed, the fully connected model would be unable to preserve unimodal information during cross-modality learning.

An important step to make convergence possible with ModDrop is to first learn the fusion without cross-modality. For this reason, [START_REF] Neverova | Moddrop: adaptive multi-modal gesture recognition[END_REF] conditioned the weight matrix of the first layer so that the diagonal blocks are equal to zeros and released this constraint after a well-chosen number of iterations.

To warranty the preservation of the unimodal information, we explore an alternative method which turned out to be better: we apply an adapted weight decay, only on the non-diagonal blocks, and decreased its contribution to the loss through time. To be more formal, let n be the number of modalities, W 1 be the weights matrix of the first layer. It can be divided into n 2 weights block matrices W 1 k,l , modeling unimodal and intermodal contributions, with k and l, ranging over the number of modalities n. The first fully connected equation can be written as :

h 1 h 2 h 3 = W 1 1,1 W 1 1,2 W 1 1,3 W 1 2,1 W 1 2,2 W 1 2,3 W 1 3,1 W 1 3,2 W 1 3,3 M 1 M 2 M 3
Then, the term to add to the loss is simply (with γ md decreasing through the time):

γ md k l ||W 1 k,l || 2
Setting γ S D to very high values during the first iterations leads to zeroing non-diagonal block matrices. Lowering it later reintroduces progressively these coefficients. From our observation, this approach provided better convergence on the considered problem. Score trees. Our motivation is to combine the high-level information coming from the scores with the lower-level information coming from the features, all together. We did it by building what we call Score Trees (see Figure 6 for an illustration).

A fully connected classification neural network is applied separately to the features of the different modalities, outputting a vector of size 7. This vector is then concatenated with the scores of the two other modalities, to create a vector of size 21. A fully connected classification neural network is then fed with it and outputs a prediction vector of size 7. The aim is to make predictions with respect to the predictions coming from other modalities. Finally, these three new prediction vectors are concatenated and fed into a last fully connected classifier, which gives the overall scores. This method can be generalized to any number of modalities.

Weighted Mean. The weighted mean is the approach of the winners of the 2016 edition [START_REF] Fan | Video-based emotion recognition using cnn-rnn and c3d hybrid networks[END_REF]. It consists in weighting the score of each modality and sum them up.

The weights are chosen by cross validation on the validation set, selecting the ones giving the best performance.

We applied it on the VGG-LSTM, C3D-LSTM and audio models.

EXPERIMENTAL VALIDATION AND RESULTS

After introducing the AFEW dataset (the dataset of the challenge), this section presents the experimental validation of our method.

We first present experiments done on the modalities taken separately, and then present experiments on their fusion. We finally introduce the experiments done for the EmotiW'17 challenge and the performance we obtained.

The Acted Facial Emotion in the Wild dataset

Acted Facial Emotion in the Wild (AFEW) is the dataset used by the EmotiW challenge. The 2017 version of AFEW is composed of 773 training videos, 383 validation videos and 653 test videos. Each video is labeled with one emotion among: 'angry', 'disgust', 'fear', 'happy', 'sad', 'neutral' and 'surprise'. In addition to the video, cropped and aligned faces extracted by [START_REF] Xiong | Supervised descent method and its applications to face alignment[END_REF][START_REF] Zhu | Face detection, pose estimation, and landmark localization in the wild[END_REF] are also provided.

Another important specificity of this dataset is the class distribution of the Train/Val/Test subsets (as shown in Table 1). This difference can make the performance on the Test set different from the one of the Validation set, as some classes are more challenging than others.

External training data.

To enlarge the training set, we collected external data by selecting 380 video clips from our personal DVDs movie collection, after checking that there is no overlap between the selected movies and the ones of AFEW [START_REF] Dhall | Collecting Large, Richly Annotated Facial-Expression Databases from Movies[END_REF]. These movies were processed by the following pipeline: faces are first detected using our face detector (see Section the bounding boxes and timestamps are kept. We then extract candidates temporal windows of ten seconds around all of these time stamps and asked human annotators to select and annotate the most relevant ones. To ensure the quality of our annotations, we evaluated ourselves (as human beings) on the validation set. We reached a performance from 60 % to 80 % depending on the annotator, which is compatible with the figure of 60% observed by [START_REF] Kächele | Revisiting the EmotiW challenge: how wild is it really?[END_REF].

Experiments on Single Modalities

Each modality has been evaluated separately on the validation set of AFEW. The VGG-LSTM and C3D-LSTM modalities performs better than [START_REF] Dhall | Emotiw 2016: Video and group-level emotion recognition challenges[END_REF].

Regarding the VGG-LSTM and the C3D-LSTM, both unidirectional and bidirectional LSTM architectures [START_REF] Graves | Bidirectional LSTM networks for improved phoneme classification and recognition[END_REF] were evaluated, with one or two layers.

In several recent papers [START_REF] Baccouche | Spatio-Temporal Convolutional Sparse Auto-Encoder for Sequence Classification[END_REF][START_REF] Du | Hierarchical recurrent neural network for skeleton based action recognition[END_REF], bidirectional LSTM is claimed to be more efficient than the unidirectional one and could be seen as a way to augment the data. Nevertheless, in our case, we have observed that the bidirectional LSTM was prone to over-fitting on the training set and therefore does not perform well on the validation set. The same observation has been made when increasing the number of layers. The best performing architecture is in both cases a one-layer unidirectional LSTM.

VGG-LSTM.

The VGG model (without LSTM) has first been evaluated by taking the maximum of the scores over the sequences, giving the accuracy of 41.4% on the validation set.

Then the different LSTM architectures were tested and the best performance for each one is given in Table 2. We note a 3% improvement compared to Fan et al. [START_REF] Fan | Video-based emotion recognition using cnn-rnn and c3d hybrid networks[END_REF]. It can be explained by the fact that our model uses the whole sequences, feeding the model with more information. Data augmentation also helps.

C3D-LSTM.

We then experimented our method with the C3D modality alone. The performance is given in Table 3.

We observe that our implementation of C3D trained on random windows and evaluated on central windows is not as good as Fan et al. [START_REF] Fan | Video-based emotion recognition using cnn-rnn and c3d hybrid networks[END_REF]. The C3D trained on central windows performed better but is not state-of-the-art either.

Our proposed C3D (with LSTM) has been tested with and without overlapping between windows. To evaluate the weighted C3D, the prediction of the window with the maximal softmax score among the video is first taken. It performs better without overlapping, and we observe a lower difference between training and validation accuracy. It could be explained by the fact that the number of 39.7 % Table 3: C3D and C3D-LSTM performance on the validation set of AFEW.

windows is lower if there is no overlap, the choice between the windows is therefore easier. As a second observation, the use of LSTM with the weighted C3D leads to the highest scores.

At the end, it can be observed that our C3D descriptor performs significantly better than the one of [START_REF] Fan | Video-based emotion recognition using cnn-rnn and c3d hybrid networks[END_REF].

Audio.

The audio modality gave a performance of 36.5%, lower than the state-of-the-art method (39.8%) [START_REF] Fan | Spatiotemporal Networks for Video Emotion Recognition[END_REF]. The use of a perceptron classifier (worse than the SVM) nevertheless allowed us to use high-level audio features during fusion. The simple baseline fusion strategy (majority vote or means of the scores) does not perform as well as the VGG-LSTM modality alone.

Experiments on Fusion

The proposed methods (ModDrop and Score Tree) achieved promising results on the validation set, but are not as good as the simple weighted mean on the test set. This can be explained by the largest number of parameters used for the modDrop and the score tree, and by the fact that some parameters cross validated on the validation set.

The best performance obtained on the validation set has the accuracy of 52.2 % , which is significantly higher than the performance of the baseline algorithm provided by the organizers -based on computing LBPTOP descriptor and using a SVR -giving the accuracy of 38.81 % on the validation set [START_REF] Dhall | From Individual to Group-level Emotion Recognition: EmotiW 5.0[END_REF].

Our participation to the EmotiW'17 challenge

We submitted the method presented in this paper to the EmotiW'17 challenge. We submitted 7 runs which performance is given in Table 5).

The difference between the runs are as follows:

• Submission 2: ModDrop fusion of audio, VGG-LSTM and a LSTM-C3D with an 8-frame overlap. • Submission 3: addition of another LSTM-C3D, with no overlap, improving the performance on the test set as well as on the validation set. • Submission 4: fusion based on Score Trees, did not achieve a better accuracy on the test set, while observing a slight improvement on the validation set. • Submission 5: addition of one VGG-LSTM and two other LSTM-C3D, one with 8 frames overlap and one without. These new models were selected among the best results in our random grid search on hyper-parameters according to their potential complementarity degree, evaluated by measuring the dissimilarity between their confusion matrices. The fusion method is ModDrop. • Submission 6: weighted mean fusion of all the preceding modalities, giving a gain of 1 % on the test set, while losing one percent on the validation set, highlighting generalization issues. • Submission 7: our best submission, which is the same as the sixth for the method but with models trained on both training and validation sets. This improves the accuracy by 1.2 %. This improvement was also observed in the former editions of the challenge. Surprisingly, adding our own data didn't bring significant improvement (gain of less than one percent on the validation set). This could be explained by the fact that our annotations are not correlated enough with the AFEW annotation.

The proposed method has been ranked 4th in the competition. We observed that, this year, the improvement of the top accuracy compared to the previous editions is small (+1.1%), while from 2015 to 2016 the improvement was of +5.2 %. This might be explained by the fact that the methods are saturating, converging towards human performance (which is assumed to be around 60 %). However, the performance of top human annotators (whose accuracy is higher than 70 %) means there is still some room for improvement.

Submission

CONCLUSIONS

This paper proposes a multimodal approach for video emotion classification, combining VGG and C3D models as image descriptors and explores different temporal fusion architectures. Different multimodal fusion strategies have also been proposed and experimentally compared, both on the validation and on the test set of AFEW. At the EmotiW'17 challenge, the proposed method ranked 4th with the accuracy of 58.81 %, 1.5 % under the competition winners. One important observation from this competition is the discrepancy between the performance obtained on the test set and the one on the validation set: good performance on the validation set is not a warranty to good performance on the test set. Reducing the number of parameters in our models could help to limit overfitting. Using pre-trained fusion models and, moreover, gathering a larger set of data would also be a good way to face this problem. Finally, another interesting path for future work would be to add contextual information such as scene description, voice recognition or even movie type as an extra modality.

Figure 1 :

 1 Figure 1: The 7 emotions of the AFEW dataset: each row represents an emotion with a set of faces sampled across a representative video clip. Please note that if most of the video clips do contain faces, some of them don't.

Figure 2 :

 2 Figure 2: Comparison of the bounding boxes given by our detection/normalization procedure (color images) with those provided with the AFEW dataset (gray-scale images), on 4 random faces of AFEW. Our bounding boxes are slightly larger.

Figure 3 :

 3 Figure 3: Our model includes audio, VGG-LSTM and C3D-LSTM (with or without overlapping) modalities. Each modality gives its own feature vectors and scores, which can be fused using different methods. It can be noted that the dimensions of the features vectors are chosen to have balanced contributions between modalities, making a trade off between the number of parameters and the performance.

Figure 4 :

 4 Figure 4: In the case of 8 frames overlap, we can see that the 16-frame windows are sharing half of their faces.

Figure 5 :

 5 Figure5: Fully connected model with ModDrop. The three modalities are concatenated and a fully connected with mod-Drop is applied. The obtained hidden representation is then fed to a second regular fully connected layer, which will output the scores.

Figure 6 :

 6 Figure 6: The Score Tree architecture

Figure 7 :

 7 Figure 7: Confusion matrix obtained with the seventh submission. We can see that 'disgust' and 'surprise' classes are never predicted by our model, while the three dominant classes ('happy', 'neutral' and 'angry') are well recognized. The 'neutral' class has the largest number of false positives. It underlines the difficulty, even for humans, to draw the margin between presence and absence of emotion. Rows denote true classes, columns predicted classes.

Table 1 :

 1 2.1 for details), and AFEW 7.0: number of video sequences per class.

		Training	Validation	Test
	Angry	133 (17.2 %)	64 (16.7 %)	99 (15.2 %)
	Disgust	74 (9.6 %)	40 (10.4 %)	40 (6.1 %)
	Fear	81 (10.4 %)	46 (12 %)	70 (10.7 %)
	Happy	150 (19.4 %)	63 (16.4 %)	144 (22 %)
	Sad	117 (15.1 %)	61 (15.9 %)	80 (12.3 %)
	Neutral	144 (18.6 %)	63 (16.4 %)	191 (29.2 %)
	Surprise	74 (9.6 %)	46 (12 %)	29 (4.4 %)
	Total	773	383	653

Table 2 :

 2 VGG-LSTM performance on the validation set of AFEW.

	Method	Validation
		accuracy
	Maximum of the scores	41.4 %
	Unidirectional LSTM one layer	48.6 %
	Bidirectional LSTM one layer	46.7 %
	Unidirectional LSTM two layers	46.2 %
	Bidirectional LSTM two layers	45.2 %
	Fan et al. [18]	45.42 %
	Method	Validation
		accuracy
	C3D on central window	38.7 %
	C3D on random window	34 %
	Weighted C3D (no overlap)	42.1 %
	Weighted C3D (8 frames overlap)	40.5 %
	Weighted C3D (15 frames overlap)	40.1 %
	LSTM C3D (no overlap)	43.2 %
	LSTM C3D (8 frames overlap)	41.7 %
	Fan et al. [18]

Table 4

 4 summarizes the different experiments we made on fusion.

Table 4 :

 4 Performance of the different fusion methods on the validation and test sets.

	Fusion method	Validation	Test
		accuracy	accuracy
	Majority vote	49.3 %	_
	Mean	47.8 %	_
	ModDrop (sub.3)	52.2 %	56.66 %
	Score Tree (sub.4)	50.8 %	54.36 %
	Weighted mean (sub.6)	50.6 %	57.58 %

Table 5 :

 5 Performance of our submissions on the test set.

					Test Accuracy
	2				55.28 %
	3				56.66 %
	4				54.36 %
	5				56.51 %
	6				57.58 %
	7				58.81 %
		Angry	Disgust	Fear	Happy Neutral	Sad	Surprise
	Angry	74,5	0	3,1	3,1	18,4	1	0
	Disgust	20	0	5	15	40	20	0
	Fear	27,1	0	34,3	1,4	21,4	15,7	0
	Happy	6,9	0	0,7	82,6	6,3	3,5	0
	Neutral	8,3	0	2,1	5,7	69,9	14	0
	Sad	12,5	0	7,5	13,8	25	41,3	0
	Surprise	21,4	0	21,4	7,1	35,7	14,3	0

We use the emobase2010 configuration file.

The sequences with fewer than 16 frames were padded by themselves to reach a sufficient length.


Sorin Stratulat
email: sorin.stratulat@univ-lorraine.fr

Cyclic Proofs with Ordering Constraints

CLKID ω is a sequent-based cyclic inference system able to reason on first-order logic with inductive definitions. The current approach for verifying the soundness of CLKID ω proofs is based on expensive model-checking techniques leading to an explosion in the number of states. We propose proof strategies that guarantee the soundness of a class of CLKID ω proofs if some ordering and derivability constraints are satisfied. They are inspired from previous works about cyclic well-founded induction reasoning, known to provide effective sets of ordering constraints. A derivability constraint can be checked in linear time. Under certain conditions, one can build proofs that implicitly satisfy the ordering constraints.

Introduction

CLKID ω [START_REF] Brotherston | Sequent calculi for induction and infinite descent[END_REF] is the de facto standard sequent-based cyclic inference system for performing lazy induction reasoning on specifications based on first-order logic with inductive definitions (FOL ID ). The CLKID ω proofs are represented as finite derivation trees with nodes labelled by sequents. A particular feature is that cycles can be built by establishing connections between terminal and non-terminal nodes labelled with identical sequents. The soundness of CLKID ω proofs is entailed from some global trace condition by using Infinite Descent induction arguments [START_REF] Wirth | Descente infinie + Deduction[END_REF]. This condition requires that, for every infinite path in the cyclic derivation of a false sequent, all successive steps starting from some point are decreasing and certain steps occurring infinitely often are strictly decreasing w.r.t. some semantic ordering.

CLKID ω has been implemented in the Cyclist prover [START_REF] Brotherston | A generic cyclic theorem prover[END_REF]. Since the global trace condition is an ω-regular property, Cyclist can check it during the proof construction or post hoc as an inclusion between two Büchi automata by calling an external model checker. It turns out that the inclusion test may be costly. Indeed, for any proof P , the approach requires the construction of the automaton complementary to that accepting strings over infinite progressing traces in P , based on a complementation method for Büchi automata as described in [START_REF] Kupferman | Weak alternating automata are not that weak[END_REF]. The method ensures that, for every automaton with n states, the generated complementary automaton has at least 2 O(n log n) states [START_REF] Michel | Complementation is more difficult with automata on infinite words[END_REF]. In case of failure of the inclusion test, previous proof steps should be reconsidered, requiring that existing connections be broken, proof steps cancelled or different inference rules applied. Hence, it may happen that the test be executed several times during the proof construction. For the proofs of the toy examples from [START_REF] Brotherston | A generic cyclic theorem prover[END_REF], the percentage of time taken by the soundness check include values from 0% to 44%.

Example 1.1. The 'P and Q' example [START_REF] Wirth | Descente infinie + Deduction[END_REF] is specified in [START_REF] Brotherston | A generic cyclic theorem prover[END_REF] using the following mutually dependent inductive predicates P and Q defined over naturals:

⇒ P (0) (1) P (x) ∧ Q(x, s(x)) ⇒ P (s(x)) (2) ⇒ Q(x, 0) (3) P (x) ∧ Q(x, y) ⇒ Q(x, s(y)) (4)
where 0 and s are the usual constructor symbols for naturals. Let N define the set of naturals by the productions:

⇒ N (0) (5) N (x) ⇒ N (s(x)) (6)
According to Table 1 from [START_REF] Brotherston | A generic cyclic theorem prover[END_REF], Cyclist can prove the sequent N (x), N (y) Q(x, y) in about half a second, by building a proof tree with only 13 nodes. The validation process required 181 calls to the external model checker, among which 171 calls are failing. 31% of the time is spent on the soundness check.

On the other hand, a different approach based on ordering constraints has been proposed in [START_REF] Stratulat | A unified view of induction reasoning for first-order logic[END_REF][START_REF] Stratulat | Mechanically certifying formula-based Noetherian induction reasoning[END_REF] for performing cyclic well-founded induction to check inductive consequences of conditional specifications. The proofs generated by this approach are normalized to sets of tree derivations and represented as directed graphs (for short, digraphs) allowing some terminal nodes to be connected to root nodes. The minimal cycles resulting by following the arrows in the digraph are denoted as cyclic lists of paths leading a root to a terminal node in the same tree derivation. The ordering constraints for checking the proof soundness involve only comparisons between instances of root formulas. Their number is given by the number of paths from the minimal cycles and does not depend on the length of these paths. Cyclic well-founded induction proofs have been validated in [START_REF] Stratulat | Structural vs. cyclic induction: a report on some experiments with Coq[END_REF] by certifying environments as Coq [START_REF]The Coq development team[END_REF].

This approach is rather general and helps to define reductive inference systems [START_REF] Bronsard | Induction using term orderings[END_REF][START_REF] Stratulat | A unified view of induction reasoning for first-order logic[END_REF], as those based on implicit induction [START_REF] Bouhoula | Implicit induction in conditional theories[END_REF]. They can build automatically proof derivations whose soundness is implicitly guaranteed by the proof method, hence no validation steps are required. Lacking the inconvenients presented by the on-the-fly/post-hoc soundness tests or backtracking steps, they allow for an effective proof generation and help to deal with industrial-size applications [START_REF] Barthe | Validation of the JavaCard platform with implicit induction techniques[END_REF][START_REF] Rusinowitch | Mechanical verification of an ideal incremental ABR conformance algorithm[END_REF].

This paper, structured in four sections, presents an effective solution to validate the global trace condition for proofs generated with CLKID ω N , a restricted version of CLKID ω using ordering constraints, in the same line as for cyclic wellfounded induction proofs. Section 2 is a quick presentation to the logical framework based on FOL ID and an introduction to CLKID ω N . In Section 3, we define proof strategies that guarantee the global trace condition for CLKID ω N proofs satisfying a set of ordering and derivability constraints. An ordering constraint consists of a comparison between two sequents, defined as a multiset extension of an ordering < a over literals. It can be decided in polynomial time in the size of the sequents if the < a -relations can also be decided in polynomial time. The derivability constraints can be checked in linear time provided that the 'history' of some atoms from the compared sequents is preserved. We took as running example the conjecture from Example 6 of [START_REF] Brotherston | A generic cyclic theorem prover[END_REF], whose proof required the maximal time percentage for the soundness check. We provide a CLKID ω N proof of it and show that its soundness check needs only two ordering constraints. A link with the reductive reasoning techniques is established; as a proof of concept, we define proof strategies that can build a reductive proof of N (x), N (y) Q(x, y) and show that the ordering constraints are implicitly satisfied. The conclusions and future work are given in the last section.

The logical framework

The logical setting relies on FOL ID with equality, as presented, e.g., in [START_REF] Brotherston | Sequent Calculus Proof Systems for Inductive Definitions[END_REF][START_REF] Brotherston | Sequent calculi for induction and infinite descent[END_REF].

Syntax. Let Σ be a (countable) language built on a finite alphabet of arityfixed function symbols F and predicate symbols, and V an enumerable set of variables. Each predicate symbol is either inductive (i.e., defined by axioms as below) or ordinary (i.e., not inductive). Terms and formulas are defined as usual. (t 1 , . . . , t n ) denotes a vector of terms and P (t 1 , . . . , t n ) an inductive atom, where P is an inductive predicate symbol and t 1 , . . . , t n are terms. ≡ represents the syntactic equality. A substitution σ is a finite non-empty set of mappings of distinct variables to terms n i=1 {x i → t i }, also denoted as {x → t}, where x ≡ (x 1 , . . . , x n ) and t ≡ (t 1 , . . . , t n ). t[σ] denotes the instance of a term t built with the substitution σ; we also say that t[σ] matches t. Similarly, we can apply substitutions and build instances for atoms, formulas and (multi)sets of formulas. F V (S) denotes the set of free variables from the set of formulas S.

Each inductive predicate symbol P is defined by a finite inductive definition set of productions (axioms) consisting of implication formulas of the form

( h m=1 Q m (u m ) ∧ l m=1 P im (t m )) ⇒ P (t), (7)
where h, l, i 1 , . . . , i l are naturals and Q 1 , . . . , Q h (resp., P i1 , . . . , P i l ) are ordinary (resp., inductive) predicate symbols. ( 7) is an unconditional production if h = 0 and l = 0. If not, ( 7) is a conditional production and

h m=1 Q m (u m ) ∧ l m=1 P im (t m
) is its condition. Φ denotes the set of productions defining each inductive predicate symbol.

Orderings. Let (E, ≤) be a non-empty poset. The strict part of the partial order ≤, referred to as ordering, is denoted by <. A binary relation R is stable under substitutions if whenever s R t then (s[σ]) R (t[σ]), for every substitution σ and terms/formulas s and t. Given two finite multisets A and B of elements from E, we say that < < is the multiset extension of < and write B < < A if there are two finite multisets X and Y such that B = (A -X) Y , X = ∅ and ∀y ∈ Y , ∃x ∈ X, y < x holds, where (resp., -) is the union (resp., difference) on multisets. In practice, X (resp., Y ) is A (resp., B) after having deleted pairwisely the common elements.

The CLKID ω N inference system. CLKID ω N consists of a finite set of inference rules that process sequents [START_REF] Gentzen | Untersuchungen über das logische Schließen[END_REF] of the form Γ ∆, where Γ and ∆ are finite multisets of first-order formulas and referred to as antecedents and succedents, respectively. An inference rule transforms a sequent, called conclusion, into a

Γ Q1(u1)[σ], ∆ . . . Γ Q h (u h )[σ], ∆ Γ Pi 1 (t1)[σ], ∆ . . . Γ Pi l (t l )[σ], ∆ (R.( 7
)) Γ P (t ), ∆
The case rule is a left-introduction operation for inductive predicate symbols:

case distinctions (Case P ) Γ, P (s 1 , . . . , s n ) ∆ Every production of the form [START_REF] Brotherston | Sequent Calculus Proof Systems for Inductive Definitions[END_REF] for which t ≡ (t 1 , . . . , t n ) produces the case distinction

Γ, s 1 = t 1 , . . . , s n = t n , Q 1 (u 1 ), . . . , Q h (u h ), P i1 (t 1 ), . . . , P i l (t l ) ∆ (8)
Each variable y from ( 7) is fresh w.r.t. the free variables from the conclusion of the rule (y can be renamed to a fresh variable, otherwise). P i1 (t 1 ), . . . , P i l (t l ) are case descendants of P (s 1 , . . . , s n ).

CLKID ω N pre-proof trees. A derivation tree for some sequent S is built by successively applying inference rules starting from S. The terminal nodes in the tree can be either leaves or buds. A leaf is labelled by a sequent that is the conclusion of a 0-premise inference rule. A bud is every node labelled by a sequent that is the conclusion of no rule. For each bud, there is a companion, i.e., an internal node having the same sequent labelling. If a companion is annotated by some sign (e.g., † or * ), then the buds related to it are uniquely annotated by that sign followed by a number. Definition 2.1 (pre-proof tree, induction function for tree). The pair (D, R) denotes a pre-proof tree of some sequent S, where D is a finite derivation tree whose root is labelled by S and R is a defined induction function assigning a companion to every bud in D.

Example 2.2. A CLKID

ω N pre-proof tree of N (x), N (y) R(x, y) is (R.( 9
)) N y R(0, y) (R.(9)) R(0, 0) N x R(x , 0) ( †1) (Subst) N x R(x , 0) (R.( 10
)) N x R(sx , 0) (Case N ) N x R(x , 0) ( †) (R.( 10
)) N x R(sx , 0) N x, N y R(x, y) ( * 1) (Subst) N ssx , N y R(ssx , y ) (Cut) N x , N y R(ssx , y ) (R.( 11
)) N x , N y R(sx , sy ) (Case N ) N x , N y R(sx , y) (Case N ) N x, N y R(x, y) ( * )
where the inductive predicate R is defined, as in [START_REF] Brotherston | A generic cyclic theorem prover[END_REF], by the productions

⇒ R(0, y) (9) R(x, 0) ⇒ R(sx, 0) (10) R(ssx, y) ⇒ R(sx, sy) (11)
For lack of horizontal space, we have unambiguously omitted the parentheses and commas when denoting some natural and atom N (t), i.e., s(t) (resp., N (t))

becomes st (resp., N t), where t is the notation of t without parentheses. This alternative notation will be used in the following, when necessary.

The double line means that (= L) was applied on each premise of (Case). The (Cut) premise N x N ssx is suppressed on the right-hand branch as in Example 6 of [START_REF] Brotherston | A generic cyclic theorem prover[END_REF]. The principal formula for each (Case) application is underlined. Finally, the induction function R is defined such that the companion of the bud denoted by ( * 1) (resp., ( †1)) is ( * ) (resp., ( †)).

Semantics. The semantics for FOL ID with equality is defined as in [START_REF] Brotherston | Sequent calculi for induction and infinite descent[END_REF]. Prefixed points of a monotone operator issued from Φ [START_REF] Aczel | An introduction to inductive definitions[END_REF] help to interpret inductive predicates. A standard model for (Σ, Φ) is a first-order structure defined by the least prefixed point, approached by an iteratively built approximant sequence.

Definition 2.3 (validity of a sequent).

Let M be a standard model for (Σ, Φ), Γ ∆ a sequent and ρ a valuation which interprets in M the free variables from the sequent. We write

Γ |= M ρ ∆ if whenever G holds in M using ρ, for all G ∈ Γ , there is some D ∈ ∆ that holds in M using ρ. We say that Γ ∆ is M -true if Γ |= M ρ ∆, for every ρ. When M is implicit from the context, true is used instead of M -true.
A rule is sound, or preserves the validity, if its conclusion is true whenever its premises are true. Hence, the conclusion of every 0-premise sound rule is true.

Theorem 2.4. The CLKID ω N inference rules are sound. Definition 2.5 (sound pre-proof tree). A pre-proof tree of a sequent S is sound if S is true.

Checking the soundness of pre-proofs

Not every pre-proof tree is sound. A very simple example of unsound pre-proof tree can be built for every false sequent S by firstly adding a copy of some antecedent formula using (contrL) then deleting it using (W k). Since the resulting sequent is identical to S, its node is a bud. This finishes the pre-proof tree.

We intend to apply an approach similar to that used for building well-founded (Noetherian) induction-based proofs [START_REF] Stratulat | A unified view of induction reasoning for first-order logic[END_REF] to check the soundness of pre-proof trees. In this setting, a cycle is uniformly represented as a set of paths from root companions to bud nodes. When a node of the pre-proof tree plays the role of bud and companion, it is duplicated by some transformation operation such that the roles are played separately by each copy. The normalization process consists in the exhaustive application of the transformation operations that convert a pre-proof tree to a set of pre-proof trees, for short pre-proof tree-sets.

In this section, we briefly explain the transformation operations and show how to build digraphs from pre-proof tree-sets. Then, we prove that a pre-proof tree is sound if the minimal cycles from the digraph of the pre-proof tree-set resulting from its normalization satisfy certain ordering and derivability constraints. Finally, we present some strategies for directly building sound pre-proof tree-sets.

Defining the checking criteria

The first transformation operation applies on an internal node labeled by some premise of (Subst):

. . . Γ ∆ (Subst) Γ [σ] ∆[σ] . . . produces Γ ∆ ( * 1) (Subst) Γ [σ] ∆[σ] . . . . . . Γ ∆ ( * ) (new tree)
The node is duplicated; one of its copies is detached together with the subtree derivation rooted by the node to become a new tree derivation. The two occurrences of the duplicated bud establish a new relation bud-companion by extending the definition of the induction function for trees to sets of trees.

The second transformation rule is performed on a non-root companion of n -1 (n > 1) buds and annotated by ( * ), of the form

. . . Γ ∆ ( * ) . . . to give Γ ∆ ( * n) . . . . . . Γ ∆ ( * ) (new tree)
The companion ( * ) is duplicated such that the subtree derivation rooted by it becomes a new pre-proof tree and the copy of ( * ) becomes a bud annotated by ( * n). A new relation bud-companion is created between ( * n) and ( * ).

Example 3.1. The application of the second transformation on the companion annotated by ( †) in the pre-proof tree given in Example 2.2 generates a normalized pre-proof tree-set, as shown in Fig. 3.

(R.(9)) N y R(0, y) N x R(x , 0) ( †1) (R.( 10
)) N x R(sx , 0) N x, N y R(x, y) ( * ) (Subst) N ssx , N y R(ssx , y ) (Cut) N x , N y R(ssx , y ) (R.( 11
)) N x , N y R(sx , sy ) (Case N ) N x , N y R(sx , y) (Case N ) N x, N y R(x, y) ( * ) (R.(9)) R(0, 0) N x R(x , 0) ( †) (Subst) N x R(x , 0) (R.( 10
)) N x R(sx , 0) (Case N ) N x R(x , 0) ( †)
Fig. 3: The normalized pre-proof tree-set.

Definition 3.2 (pre-proof tree-set, induction function for tree-set). The pair (MD, MR) denotes a pre-proof tree-set, where MD is a multiset of preproof trees and MR is a defined induction function assigning a companion to every bud from MD.

Lemma 3.3. The normalization process terminates.

Lemma 3.4. Let (MD, MR) be the pre-proof tree-set obtained by the normalization of some pre-proof tree of a sequent S. Then, M D i) has a pre-proof tree rooted by a node labelled by S, and ii) is built from pre-proof trees for which the premises of all (Subst) rules are bud sequents.

Any pre-proof tree-set can also be represented as a digraph of sequents using nodes from its tree-set and arrows annotated with substitutions. Let S(N ) denote the sequent labelling N , for every node N . A solid arrow leads a node N 1 to a node N 2 if there is a rule applied on S(N 1 ) and S(N 2 ) is a premise of the rule. It is annotated with the identity substitution for S(N )(≡ Γ ∆), denoted by σ S(N ) id and defined as x∈F V (Γ ∪∆) {x → x}, if N is not a (= L)-node. When not ambiguous, the identity substitutions are omitted. If N is a (= L)-node whose principal formula is x = u, the arrow leaving N is annotated by the equality substitution {x → u}. On the other hand, a dashed arrow leads a bud B to its companion and is annotated with a substitution written in boldface. If S(B) is the premise of a (Subst) rule using the substitution θ, this substitution is θ. Otherwise, it is σ S(B) id . For convenience, the sequent Γ ∆ labelling a node N i in the digraph is indexed by i as Γ i ∆.

Example 3.5. Fig. 4 shows the digraph of the pre-proof tree-set from Fig. 3.

A path is a (potentially infinite) list of nodes built by following the arrows in the digraph. It is (Subst)-free if none of the sequents labelling its nodes is the premise of some (Subst)-rule.

Definition 3.6 (cumulative substitution). A (Subst)-free path [N 1 , . . . , N n ] (n > 0) is annotated by the cumulative substitution σ all id σ 1 • • • σ n-1
, where σ i is the substitution annotating the solid arrow leading N i to N i+1 , for each i ∈ [1..n -1], and σ all id is the overall identity substitution

∪ N ∈[N 1 ,...,N n ] {x → x | x ∈ F V (Γ ∪ ∆) and S(N ) ≡ Γ ∆}.
Example 3.7. The cumulative substitution for the (Subst)-free path [N 1 , N 3 , N 5 , N 6 , N 7 ] from Fig. 4 is {x → sx ; y → sy }, which is the composition of the overall identity substitution {x → x; y → y} with the substitutions {x → sx }, {y → sy }, and other identity substitutions.

The digraph P of a pre-proof tree-set (MD, MR) can be partitioned in a set of strongly connected components (SCCs). Some of them may have only one node. The SCCs with more than one node have at least one cycle, i.e., a path built along its nodes where the nodes are repeated. A minimal cycle does not contain other cycles. Definition 3.8 (n-cycle). Every minimal cycle in P can be represented as a n-cycle, defined as a finite circular list [N 1 1 , . . . , N p1 1 ], . . . , [N 1 n , . . . , N pn n ] of n (> 0) paths leading root nodes to buds such that

N 1 next(i) = MR(N pi i ), for any i ∈ [1..n], where next(i) = 1 + (i mod n).
The standard method for checking the soundness of pre-proof trees, e.g. [START_REF] Brotherston | Sequent calculi for induction and infinite descent[END_REF], is based on a 'proof by contradiction' approach. Let us assume that the root sequent of some pre-proof tree is false. It is sufficient to show that some global trace condition is satisfied for every infinite path in the pre-proof tree, built by visiting nodes labelled by false sequents if the root sequent is false. This condition stipulates that all successive steps starting from some point in the path are decreasing and certain steps occurring infinitely often are strictly decreasing w.r.t. some semantic ordering underlying ordinals. The trace is a list of inductive antecedent atoms (IAAs) of the sequents labelling the nodes from the path. Let P (t) be one of these atoms. Since P can be generated by a sequence of approximants (P γ ) γ≥0 , the measure value for P (t) used by this ordering is the smallest ordinal γ such that P γ (t) holds for some suitable interpretation. The well-foundedness property of the ordering contradicts the fact that the path is infinite.

The question of whether a pre-proof tree is sound is decidable (see e.g. Proposition 7.4 from [START_REF] Brotherston | Sequent calculi for induction and infinite descent[END_REF]), by using a decision procedure based on the automata-based complementation method. On the other hand, the computational and combinatorial complexity of the validation of the global trace condition can be reduced for pre-proof trees of certain structure, e.g., for those having trace manifolds [START_REF] Brotherston | Cyclic proofs for first-order logic with inductive definitions[END_REF][START_REF] Brotherston | Sequent Calculus Proof Systems for Inductive Definitions[END_REF].

The trace manifold condition can be checked only on pre-proof trees in cycle normal form, for which the companion of every bud B is also an ancestor of B. Any pre-proof tree can be transformed in a cycle normal form. Mainly, it is unfolded into an infinite pre-proof tree, then the infinite branches are folded to get an equivalent normalized pre-proof tree. An improved complexity bound can be achieved by an iterative 'untangling' process of the pre-proof tree. By Theorem 6.3.6 from [START_REF] Brotherston | Sequent Calculus Proof Systems for Inductive Definitions[END_REF], if a derivation tree has n nodes, the equivalent normalized derivation tree has no more than n 2 n/2 nodes.

In the same quest to reduce the complexity of the validation process, we adapt the approach for building well-founded induction proofs [START_REF] Stratulat | A unified view of induction reasoning for first-order logic[END_REF] to generate pre-proof trees that implicitly guarantee the validity of the global trace condition. For this, we denote by ≤ π a partial ordering defined over the set of instances of every sequent labelling root nodes from some SCC π with cycles. Its strict part is denoted by < π and its equivalence part by ∼ π . Contrary to [START_REF] Stratulat | A unified view of induction reasoning for first-order logic[END_REF], < π is not required to be well-founded. We assume that < π is built as the multiset extension of a 'stable under substitutions' ordering < a defined over IAAs and used to compare instances of the root sequents from π. Hence, < π is also stable under substitutions [START_REF] Baader | Term Rewriting and All That[END_REF]. We also assume that ∼ π is stable under substitutions. Like < π , < a does not need to be well-founded. For each node N in π and every instance S of S(N ), we denote by A S the measure value (weight) of S, represented as a multiset of IAAs of S and used in the comparisons of S with other sequent instances w.r.t. ≤ π .

Definition 5.4 of [START_REF] Brotherston | Sequent calculi for induction and infinite descent[END_REF] for a trace in a pre-proof tree can be adapted for a digraph P and simplified to take into account the restricted version of (= L). Definition 3.9 (trace). A trace following some (potentially infinite) path p in P, denoted by [N 1 , N 2 , . . .], is a sequence (τ i ) (i≥0) such that:

-τ i = P (t), where P (t) is an IAA of S(N i ); -if Γ i ∆ i is the conclusion of (Subst) then τ i = τ i+1 [ρ],
where ρ is the substitution associated with the rule instance;

-if Γ i , x = u ∆ i is the conclusion of (= L), then τ i+1 = τ i [{x → u}]; -if S(N i ) is the conclusion of a (Case)-rule, then either i) τ i+1 = τ i , or ii)
τ i is its principal formula and τ i+1 is a case descendant of τ i . In this case, i is called a progression point; if S(N i ) is the conclusion of any other rule, then τ i+1 = τ i .

We say that an IAA τ j derives from an IAA τ i using the trace (τ k ) (k≥0) if i < j. Given two arbitrary substitutions γ and δ, we also say that τ j [γ] derives from τ i [δ] using (τ k ) (k≥0) . Let π be a SCC from P and < a the 'stable under substitutions' ordering defined over the set of instances of the IAAs from the root sequents inside π. We can define < π as the multiset extension of < a that satisfies some derivability constraints. Definition 3.10 (< π -derivability). Let N i and N j be two nodes occurring in some path p from an SCC π, θ and δ two substitutions, and A S(N i )[θ] (resp., A S(N j )[δ] ) the multiset resulting from A S(N i )[θ] (resp., A S(N j )[δ] ) after the pairwise deletion of all common IAAs from A S(N i )[θ] and A S(N

j )[δ] . Then, S(N j )[δ] is < π -derivable from S(N i )[θ] along p if i) for each l ∈ A S(N j )[δ] , there exists l ∈ A S(N i )[θ]
such that l > a l and l derives from l using some trace following p, and ii) for each l ∈ A S(N

j )[δ] \A S(N j )[δ] , there is some l ∈ A S(N i )[θ] \A S(N i )[θ]
such that l ≡ l and l derives from l using some trace following p. Lemma 3.11. In Definition 3.10, for each IAA l from S(N j )[δ] there is an IAA l from S(N i )[θ] such that l derives from l using some trace following p.

We give below some useful properties of the < π -derivability relation. Lemma 3.12. S < π S if S is < π -derivable from S along some path p in π.

Lemma 3.13. The '< π -derivability' relation is stable under substitutions. It is also transitive, i.e., if S is < π -derivable from S along p and S is < π -derivable from S along p then S is < π -derivable from S along p, for some path p in π.

We are ready to introduce the ordering constraints that help to discharge induction hypotheses by n-cycles. .n], let θ c i be the cumulative substitution annotating [N 1 i , . . . , N f i ], where the IH-node

N f i is either i) N pi i if [N 1 i , . . . , N pi i ] is (Subst)-free, or ii) N pi-1 i , otherwise. The IHs S(N 1 j )[δ j ] (j ∈ [1..n]) are dis- charged by C if, ∀i ∈ [1..n], S(N pi i )[δ i ] is < π -derivable from S(N 1 i )[θ c i ] along [N 1 i , . . . , N pi i ]. Definition 3.
14 is well-formed; the cumulative substitution can be computed for the case ii) because, for each

i ∈ [1..n], [N 1 i , . . . , N pi-1 i
] is a (Subst)-free path, by following the claim ii) of Lemma 3.4. By construction, S(

N f i ) is the IH S(N 1 next(i) )[δ next(i) ], for all i ∈ [1..n].
For every IAA l of a sequent bud corresponding to some τ i from a trace (τ k ) (k≥0) following a path from some minimal cycle, we define the history of l as the subtrace (τ k ) (k<i) . If each such IAA stores its history during the proof construction, every derivability constraint can be decided in linear time w.r.t. the size of the history, by visiting one by one each element in the history. We define the measure value for any sequent instance of the form S(N 10 )[{x → t; . . .}] (resp., S(N 1 )[{x → t 1 ; y → t 2 ; . . .}]) as {N (t)} (resp., {N (t 2 )}). < π and < π are multiset extensions of an ordering < a over the IAAs of the form N (t) and whose measure value is {t}, for any term t. < a is the multiset extension of the 'stable under substitutions' rpo ordering [START_REF] Baader | Term Rewriting and All That[END_REF], denoted by < rpo and based on the symbol precedence establishing that 0 is smaller than s.

N x, N y 1 R(x, y) {x →0} w w {x →sx } ( ( N y 2 R(0, y) N x , N y 3 R(sx , y) {y →0} v v {y →sy } N x 10 R(x , 0) {x →0} y y {x →sx } N x 4 R(sx , 0) N x , N y 5 R(sx , sy ) 11 R(0, 0) N x 12 R(sx , 0) N x 9 R(x , 0) {x →x } {x →x } {x →x } g g N x , N y 6 R(ssx , y ) N x 13 R(x , 0) N ssx , N y 7 R(ssx , y ) N x 14 R(x , 0) {x →x } {x →x } {x →x } d d N x, N y 8 R(x,
Every IH from these 1-cycles is discharged. The IH S(N 10 )[{x → x }] is < π -derivable from S(N 10 )[{x → sx }] along the (Subst)-free path [N 10 , N 12 , N 13 , N 14 ], by using the trace [N x , N x , N x , N x ] for the IAA N x of S(N 10 ). Similarly, the IH S(N

1 )[{x → ssx ; y → y }] is < π - derivable from S(N 1 )[{x → sx ; y → sy }] along the (Subst)-free path [N 1 , N 3 , N 5 , N 6 , N 7 , N 8 ]
, by using the trace [N y, N y, N y , N y , N y , N y] for the IAA N y of S(N 1 ). The two comparisons hold as z < rpo sz, for every variable z.

Definition 3.16 (proof ).

A proof is every pre-proof tree-set whose digraph has only n-cycles that discharge their IHs. Theorem 3.17 (soundness). The root sequents from every proof are true.

Proof (Sketch). It follows the general structure of the soundness proof for some cyclic well-founded inference systems, e.g., see Theorem 5.11 from [START_REF] Stratulat | Mechanically certifying formula-based Noetherian induction reasoning[END_REF]. Mainly, we define a partial ordering < R over the root nodes from the digraph P of a proof such that, for every two distinct root nodes N 1 and N 2 , we have N 1 < R N 2 if i) N 1 and N 2 are not in the same SCC, and ii) N 1 can be joined from N 2 in P.

By contradiction, we assume that there exists a root node N such that S(N ) is false. A classical induction reasoning using < R allows to explore all possibilities for N to be considered as one of the root nodes from P. The most difficult case is when N is part of some SCC with cycles. A contradiction yields by showing that there exists a trace with an infinite number of progression points, using similar arguments as in the proof of Lemma 5.7 [START_REF] Brotherston | Sequent calculi for induction and infinite descent[END_REF] and witnessed by an infinite strictly decreasing sequence of ordinals, thanks to the <-derivability constraints. Theorem 3.17 is the key argument for proving that our approach allows indeed to verify pre-proof trees. Lemma 3.18. A pre-proof tree is sound if the pre-proof tree-set resulting from its normalization operation is a proof.

Validation costs. We analyse the worst-case time complexity for validating the soundness of a pre-proof tree of n nodes with p (< n) buds occurring in minimal cycles. The number of transformation operations during the normalization step is given by the sum of non-root companions and non-terminal (Subst)-nodes, which is smaller than 2n. The cost of a transformation operation, including the node duplication and the creation of a bud-companion relation, is assumed to be some constant c. Hence the cost of the transformation operations is smaller than 2nc. If c is the constant representing the cost for annotating a substitution, the cost for building the digraph of the normalized pre-proof tree-set is smaller than nc . The partition of a digraph in SCCs can be done in linear time [START_REF] Tarjan | Depth-first search and linear graph algorithms[END_REF].

If B denotes a bud occurring in a minimal cycle, the IH that instantiates S(B) is unique because B has only one companion and at most one companion can be the root of the tree including B. The number of <-derivability constraints is that of their buds, i.e., p. In the worst case, p is n -1. The validation cost of a <-derivability constraint is the sum of the costs of derivability and ordering constraints. The time complexity for checking whether an IAA l derives from another IAA l is linear w.r.t. the size of the history of l, which is a value smaller than n. The time complexity for checking a multiset extension relation is O(rq), where r and q are the number of IAAs from the measure value of the compared sequents. In the worst case, when all bud IAAs have their history of length n and p is n-1, the time complexity for checking the derivability constraints is O(n 2 k 2 ), where k is the maximal cardinality of a sequent's measure value. Similarly, the worst-case validation cost of the ordering constraints is polynomial in k, the maximal size of a literal and n, if the time complexity for comparing two IAAs is at most polynomial, for example by using a Knuth-Bendix ordering [START_REF] Baader | Term Rewriting and All That[END_REF].

Strategies for directly building proofs

Theorem 3.17 suggests that sequents can also be proved by directly building sound pre-proof tree-sets. For this purpose, we adapt the DRaCuLa strategy [START_REF] Stratulat | A unified view of induction reasoning for first-order logic[END_REF]. Mainly, the trees from a pre-proof tree-set are developed by applying the CLKID ω N rules, as usual, with the following exceptions:

when applying a (Subst)-rule, the premise becomes a bud sequent, as shown for the first transformation of the normalization procedure. The next step is to develop a new tree rooted by the companion of the bud; when a bud is about to be created, several scenarios may happen. As a preliminary step, if its companion is a non-root node the second transformation of the normalization procedure is applied. If the bud candidate is part of an n-cycle that discharges its IHs, the bud is created (scenario 1). If it is not yet the case, either i) the strategy tries to build an n-cycle, by developing parts from other trees (scenario 2), or ii) the n-cycle does not discharge its IHs (scenario 3); in this case, a backtracking step is required either to redefine the ordering at the SCC level, or to redo previous steps, or to continue to develop the proof by applying a CLKID ω N rule on the sequent labelling the bud candidate. For (scenario 1), not only the current bud candidate is created, but all the bud candidates from the n-cycle are built, hence simultaneous induction is performed.

Example 3.19. The above strategy can build the pre-proof tree from Example 2.2. The progression in its construction can be retraced by following the indexes of the sequents from the digraph in Fig. 4. This proof strategy uses heuristics based on ordering constraints, different from the iterative depth-first search heuristics used by Cyclist.

Example 3.20. One could have built a new bud of (*) from the pre-proof tree of Example 2.2, by developing ( †) such that N 0 is added as IAA, then (Subst) applied conveniently. The new 1-cycle from its digraph is part of the SCC π of the digraph from Example 3.15. However, it cannot discharge its IH because the induction ordering is now < π instead of < π .

Sound pre-proof trees can also be directly generated to satisfy implicitly the ordering constraints, similar to implicit induction proofs, by using a reductive proof strategy based on a unique induction ordering <. Such strategy guarantees that, for every two successive nodes N i and N i+1 from each path p, of the form [N 1 , . . . , N n ] and occurring in the definition of some minimal cycle of its digraph, and i ∈

[1..f -1], we have either A S(N i+1 )[θ c i+1 ] ≡ A S(N i )[θ c i ] or S(N i+1 )[θ c i+1 ] is <-derivable from S(N i )[θ c
i ] along p, where f is the index of the IH-node in [N 1 , . . . , N n ] and θ c j is the cumulative substitution for the path [N j , . . . , N f ] (j ∈ [1..f ]). The derivability constraints are satisfied if the syntactic equality relation is not satisfied at least once along p. Indeed, knowing that the <-derivability relation is transitive (Lemma 3.13), we have that S(N f ) is <-derivable from S(N 1 )[θ c 1 ] along p, as required. If the rule applied at step i is different from (= L), we have that θ c i ≡ θ c i+1 . In this case, it is sufficient to ensure instead that A S(N i+1 ) ≡ A S(N i ) or S(N i+1 ) is <-derivable from S(N i ) along p, due to the 'stability under substitutions' property of <-derivability (again Lemma 3.13). The proof strategy is reductive if the measure value for each sequent of the form Γ, N (t) P (t) (resp., Γ, N (t 1 ), N (t 2 ) Q(t 1 , t 2 ) is the multiset of IAAs {N (t), N (t)} (resp., {N (t 1 ), N (t 1 ), N (t 2 )}) and < is defined as the multiset extension of the ordering < a over IAAs from Example 3.15. It can be checked that the <-derivability constraints are satisfied, by taking into account that the unique SCC with cycles of the digraph associated to its normalized pre-proof tree-set is built from the union of two 1-cycles, [( * ), . . . , ( * 1)] and [( †), . . . , ( †1)], and one 2-cycle [( * ), . . . , ( †2)], [( †), . . . , copy of ( * )].

By Theorem 3.17, our approach allows to prove several conjectures simultaneously. This is a feature specific to formula-based Noetherian induction reasoning [START_REF] Stratulat | A unified view of induction reasoning for first-order logic[END_REF] as that employed by the implicit induction inference systems. It is particularly useful when the proofs of the conjectures are mutually dependent.

Example 3.22. The normalization step for the pre-proof tree from Example 3.21 can be avoided if the pre-proof trees of N x P x and N x, N y Qxy are developed simultaneously.

Conclusions and future work

We have presented a new method to validate a class of CLKID ω pre-proof trees by converting them to pre-proof tree-sets, then showing that the global trace condition is implicitly satisfied if some ordering and derivability constraints hold. Every infinite path p from a pre-proof tree normalized to a proof (tree-set) can be built by concatenating path segments from the definition of the minimal cycles of its proof. These constraints ensure that there is an infinitely progressing trace following some tail of p. Our approach allows more flexibility; a different induction ordering can be defined for each SCC with cycles from the digraph of the proof. This is not the case from the unique induction ordering defined over the buds of a pre-proof tree with trace manifolds [START_REF] Brotherston | Cyclic proofs for first-order logic with inductive definitions[END_REF][START_REF] Brotherston | Sequent Calculus Proof Systems for Inductive Definitions[END_REF]. Also, our approach does not require pre-proof trees to be in cycle normal form that are, in the worst case, exponentially bigger.

The soundness check can be done in polynomial time provided that the time complexity for comparing two IAAs is at most polynomial. We defined proof strategies ensuring that the number of ordering constraints equals that of the induction hypotheses that are really required in the proof. In practice, their number is generally small even for proofs concerning real-size applications. For example, every cyclic induction proof from [START_REF] Stratulat | A unified view of induction reasoning for first-order logic[END_REF] (see Table 1) includes at most 8 induction hypotheses and 4 minimal cycles.

The ordering constraints are implicitly satisfied by reductive proof strategies. In the future, we plan to define new (derived) rules and proof strategies that automatically generate more compact reductive proof derivations and provide a better control of the proof development. The main challenge of our approach remains to find the 'good' induction orderings.

Definition 3 .

 3 14 (induction hypothesis (IH), IH discharged by an n-cycle, IH-node). Let π be an SCC with cycles and C an n-cycle [N 1 1 , . . . , N p1 1 ], . . . , [N 1 n , . . . , N pn n ] from π. The instances S(N pj j )[δ j ] (j ∈ [1..n]) are called induction hypotheses (IHs), where δ j annotates the dashed arrow starting from N pj j in C. For all i ∈ [1.

Fig. 4 : 3 . 3 . 15 .

 43315 Fig. 4: The digraph of the pre-proof tree-set from Fig. 3. Example 3.15. The digraph from Fig. 4 has two SCCs with cycles. One of them, denoted by π, consists of the 1-cycle [N 10, N 12 , N 13 , N 14 ]. The other, denoted by π , is made of the 1-cycle [N 1 , N 3 , N 5 , N 6 , N 7 , N 8 ]. No cycle has the bud N 9 .We define the measure value for any sequent instance of the form S(N 10 )[{x → t; . . .}] (resp., S(N 1 )[{x → t 1 ; y → t 2 ; . . .}]) as {N (t)} (resp., {N (t 2 )}). < π and < π are multiset extensions of an ordering < a over the IAAs

Example 3 .

 3 21. As a proof of concept, we define the derived rule (DCase): S1 . . . Sn (DCase P ) Γ, P (x) ∆

(potentially empty) multiset of sequents, called premises; they are separated by a horizontal line followed by the name of the rule. Most of the CLKID ω N inference rules transform one (principal) formula from the conclusion. In this case, it is explicitly represented in the sequent. A more detailed presentation of the sequent calculus can be found elsewhere, e.g.,[START_REF] Negri | Structural Proof Theory[END_REF].Γ ∩ ∆ = ∅ (Ax) Γ ∆ Γ ∆ Γ ⊆ Γ, ∆ ⊆ ∆ (W k) Γ ∆ Γ F, ∆ Γ G, ∆ (∧R) Γ F ∧ G, ∆ Γ F, ∆ (¬L) Γ, ¬F ∆ Γ, F ∆ (¬R) Γ ¬F, ∆ Γ, F ∆ Γ, G ∆ (∨L) Γ, F ∨ G ∆ Γ F, G, ∆ (∨R) Γ F ∨ G, ∆ Γ, F, G ∆ (∧L) Γ, F ∧ G ∆ Γ F, F, ∆ (contrR) Γ F, ∆ Γ ∆ (Subst) Γ [θ] ∆[θ] Γ F, ∆ Γ, G ∆ (⇒ L) Γ, F ⇒ G ∆ Γ, F, F ∆ (contrL) Γ, F ∆ Γ, F [{x → t}] ∆ (∀L) Γ, ∀xF ∆ Γ F, ∆ x ∩ F V (Γ ∪ ∆) = ∅ (∀R) Γ ∀xF, ∆ Γ, F ∆ x ∩ F V (Γ ∪ ∆) = ∅ (∃L) Γ, ∃xF ∆ Γ F, ∆ Γ, F ∆ (Cut) Γ ∆ Γ F [{x → t}], ∆ (∃R) Γ ∃xF, ∆ Γ, F G, ∆ (⇒ R) Γ F ⇒ G, ∆Fig.1: Sequent-based rules for classical first-order logic.CLKID ω N consists of the rules displayed in Fig.1, the rules that process equalities from Fig.2, as well as the 'unfold' and 'case' rules. (= L) is an instance of the corresponding CLKID ω rule for which x can also be a non-variable term.(= R) Γ t = t, ∆ Γ [{x → u}] ∆[{x → u}]x is not a variable of u (= L) Γ, x = u ∆ Fig.2: Sequent-based rules for equality reasoning.The unfold rule unrolls the definition of the inductive symbol to transform some succedent atom of a sequent. We denote the unfolding of P (t ) with the production[START_REF] Brotherston | Sequent Calculus Proof Systems for Inductive Definitions[END_REF], when P (t ) ≡ P (t)[σ], by

as

S1

(= L) case distinction . . . Sn (= L) case distinction (Case P ) Γ, P (x), P (x) ∆ (contrL) Γ, P (x) ∆ where x is a vector of variables. We also define the (Bud) rule:

Different variants of the subsumption operation are widely employed by the current theorem provers, Cyclist being one of them.

By using the alternative notation without parentheses, a pre-proof of N x, N y Q(x, y) is built below by firstly trying to apply the unfold rules followed by (Bud), then (Del) and, finally, (DCase). (Del) is a restricted version of the (W k) rule that deletes the IAAs of the form N (t) if none of the inductive succedent atoms from the conclusion has t as argument. It can be noticed that the history of every IAA occurring in each premise of any rule r from the above rules but (Bud) has one of the IAAs from the conclusion of r.