Abdelhadi Belfadel
email: abdelhadi.belfadel@gmail.com

Jannik Laval
email: jannik.laval@univ-lyon2.fr

Chantal Cherifi

Nejib

Chantal Bonner Cherifi
email: chantal.bonnercherifi@univ-lyon2.fr

Nejib Moalla
email: nejib.moalla@univ-lyon2.fr

Architecture-based Software Discovery and Reuse

Keywords: Enterprise architecture, Capability profile, Requirements engineering, Service reuse, Software reuse

come

Introduction

Modernizing or designing a new business process by reusing the functionality of existing software can be of great benefit to organizations. Leveraging previous developments and considering internal company solutions enriched with external ones, can help facilitate the development of complex systems at controlled costs while maintaining delivery times.

When developing software, the first thing to do is to understand and describe in a precise way the problem that the software must solve. Requirements for a targeted system describe what the system should do, what the services it should provide, and what quality or constraints it must have to make it attractive and acceptable to the owner [START_REF] Robertson | Mastering the requirements process: Getting requirements right (3rd Edition)[END_REF]. These requirements reflect the needs of customers for a system. The process of analyzing, eliciting, and checking these services and constraints is called requirements engineering [START_REF] Sommerville | Software engineering 9[END_REF].

To maximize the reuse opportunities for companies, a component view with a concise evaluation model of software components (that describe in detail the capabilities of software) provides an overview of existing solutions and facilitates the discovery, selection, and decision to reuse [START_REF] Belfadel | Towards software reuse through an enterprise architecture-based software capability profile[END_REF]. This, combined with an organization of the different artifacts (an artifact is a more granular architectural work product that describes an architecture from a specific viewpoint. Examples include a class diagram, a server specification, a list of architectural requirements...) resulting from this evaluation model, aligned with a requirement engineering approach, aims to reduce the complexity when searching and selecting software components to reuse. In addition, focusing on service-oriented solutions, many opportunities for reuse of functionality will arise, resulting in more efficient use of existing resources.

To reduce the complexity of the description of software components that result from the evaluation model and to present the required detail of information at each level of its exploitation, enterprise architecture is of great value. Enterprise Architecture (EA) is the definition and representation of a highlevel view of IT systems and enterprises' business processes. By considering an enterprise architecture-based approach, it is possible to organize the different artifacts in a way that enables an analysis of the reuse possibilities for an organization and ensure the feasibility of a targeted system or project. The insights or information provided by an enterprise architecture is needed, on the one hand, to determine, from a business perspective, the needs, and priorities for change [START_REF] Gosselt | A maturity model based roadmap for implementing togaf[END_REF] and, on the other hand, to organize the various components and technical artifacts and assess how an organization can exploit them.

With reference to this context, this research is an extended work of an already published work in [START_REF] Belfadel | Semantic software capability profile based on enterprise architecture for software reuse[END_REF]. The latter was focused on the design of a software capability profile implemented as a semantic model to gather description of the capabilities of existing solutions from several perspectives (organizational, business, technical and technological aspects). For the sake of readability, the proposed model and contributions published in [START_REF] Belfadel | Semantic software capability profile based on enterprise architecture for software reuse[END_REF] are presented in the following sections, as well as the new contributions related to the exploitation of the capability profiles through the alignment of a requirements engineering approach and an enterprise architecture method. As discussed earlier, the objective of this research work is to leverage the model already published in [START_REF] Belfadel | Semantic software capability profile based on enterprise architecture for software reuse[END_REF] to address stakeholder requirements and efficiently reuse existing solutions, by investigating the highest functional and non-functional compatibility of existing software capability profiles with stakeholder's desired features to be implemented. The expected result from this work is an exploitation process of the software capability profiles, based on the Architecture Development Method from TOGAF [START_REF] Hussain | The Open Group Architecture Framework TOGAF™ Version 9[END_REF], aligned to a requirements engineering approach implemented using Volere Specification [START_REF] Robertson | Mastering the requirements process: Getting requirements right (3rd Edition)[END_REF]. However, the problem we faced is how to align requirements and architecture artifacts in an engineering cycle, to help in the refinement of requirements and select the best candidate components to serve as building blocks in a new system?

To respond to this research problem, this paper is organized as follows: Section 2 focuses on the related work. We focus afterward on the principal building blocks of the proposed solution and present first the Enterprise Architecture Capability Profile (EACP) in section 3. Section 4 presents a concrete use case scenario on which this approach has been applied, and that serves as an example throughout the description of the exploitation process in section 5. Section 6 presents an implementation of the proposed approach. Section 7 discusses our work and finally a conclusion is drawn in Section 8.

Related Work

Requirements Engineering in Software Development Process and Service Reuse

Classical techniques for software solution specification are structured analysis and object-oriented techniques [START_REF] Roel | Requirements engineering: Problem analysis and solution specification[END_REF]. The view of requirement engineering as solution specification is taken by the IEEE 830 standard [START_REF] Ansi | Ieee. ieee guide to software requirements specifications[END_REF] and by other authors on requirements [START_REF] Robertson | Mastering the requirements process: Getting requirements right (3rd Edition)[END_REF] [START_REF] Ma Davis | Software requirements[END_REF]. In this view, and as mentioned by [START_REF] Roel | Requirements engineering: Problem analysis and solution specification[END_REF], a requirements specification consists of a specification of the context where the system operates, desired system functions, the semantic definition of these functions, and quality attributes of the functions.

Several research works and methods ( [START_REF] Syed Waqas | Process to enhance the quality of software requirement specification document[END_REF], [START_REF] Ahmad | Impact minimization of requirements change in software project through requirements classification[END_REF] or [START_REF] Abeer Abdulaziz Alsanad | A domain ontology for software requirements change management in global software development environment[END_REF]) exist in the literature to enhance software requirement specifications and for feature selection. [START_REF] Robertson | Mastering the requirements process: Getting requirements right (3rd Edition)[END_REF] propose Volere as a basis for a requirement specification. It is a result of many years of practice, consulting, and research in requirement engineering and business analysis. Volere provides template sections for each of the requirement types appropriate to today's software systems. [START_REF] Xu | Re2sep: A twophases pattern-based paradigm for software service engineering[END_REF] propose a paradigm for software service engineering to reuse services for developing new applications more rapidly with the aim to satisfy individualized customer requirements. The proposed approach uses service context as a mediating facility to match a service requirement with a service solution. The requirements are defined by the targeted business functionality, service performance, and value. However, no details about the service pattern description or repository, the requirement template nor implementation of the approach are proposed. [START_REF] Chen | A method for service-oriented personalized requirements analysis[END_REF] propose a method that allows users of services to express their requirements. The authors propose a meta-model for elements required in service consumption such as process, goal, or role. The proposed method helps to discover errors and conflicts during requirement refinement. [START_REF] Zachos | Discovering web services to specify more complete system requirements[END_REF] propose a service selection algorithm based on textual requirements expressed by the service consumer. The service selection is based on a discovery algorithm, that uses XQuery and WordNet and focuses on the disambiguation and completeness of the requirements and retrieving discovered services from the UDDI registry. There is additional ontology-based research work such as [START_REF] Verlaine | Towards conceptual foundations of requirements engineering for services[END_REF], where the authors took the CORE Ontology (for Core Ontology for Requirements) [START_REF] Ivan | A core ontology for requirements[END_REF] for requirement elicitation, and established a relationship with the concepts of Web Service Modeling Ontology (WSMO) [START_REF] Roman | Web service modeling ontology[END_REF].

Knowledge Management and Service Repositories for Service Reuse

Research on repositories for effective and useful management and discovery of services for service-oriented paradigm has recently earned significant impulse. Some specifications as UDDI [START_REF] Curbera | Unraveling the web services web: an introduction to soap, wsdl, and uddi[END_REF] or ebXML Registry [START_REF] Breininger | The ebxml registry repository version 3.0. 1[END_REF] has provided primary support to register, discover and integrate services. Due to limited capabilities offered by existing registry specifications for services discovery, some research works in the literature aim at improving service repositories with ontologybased discovery facilities. Later, semantic models have been proposed to enrich the service registry with semantic annotations, combined with matchmaking algorithms to match service capabilities.

Based on the systematic analysis of relevant research works regarding service discovery with consideration of our needs, Table 1 classifies the related service registry and discovery works published between 2002 and 2019 according to the following criteria: C1) Organizational level: exploitation based on the identification of the stakeholders, business problems, goals, and objectives of the targeted project. C2) Functional level: exploitation based on service interfaces, the business functions, and related inputs and outputs. C3) Technical level: exploitation based on the identification of relevant technical requirements, interoperability requirements, and technology constraints. C4) Technology level: exploitation based on the identification of the platforms and infrastructure. C5) Non-functional properties (QoS, Security...). C6) Exploitation based on a Requirements Engineering Process (it involves all the mentioned levels)

Out of Table 1, we notice that several research works considered the functional level and QoS to manage service repository and matchmaking, but few of them considered the other levels such as the organizational level, the technical or technology level. We notice also that few research works considered the exploitation of the service registry in a software engineering cycle using a requirement engineering process to manage the user requirements for service discovery and matchmaking. Software architecture helps to manage the complexity of software by providing an abstraction of the system. The requirements engineering process drives the architecture actions, whereas decisions made in the architectural phase can affect the achievement of initial requirements and thus change them. We should go through these two fundamental activities namely requirement engineering and software architecting during the engineering process. These activities should evolve together to offer support to the developer or architect for formalizing the requirements and architectural artifacts to enable software and service discovery and reuse. There is, however, no structured solution (as depicted in Table 1) on how to perform the co-development of requirements and architecture actions to select the suitable software or services to reuse for the development of new business software.

Service Repository and Discovery C1 C2 C3 C4 C5 C6 [START_REF] Paolucci | Semantic matching of web services capabilities[END_REF], [START_REF] Wu | Similarity-based web service matchmaking[END_REF], [START_REF] Sabou | Towards semantically enhanced web service repositories[END_REF], [START_REF] Yu | A semantically enhanced service repository for user-centric service discovery and management[END_REF], [START_REF] Haniewicz | Local controlled vocabulary for modern web service description[END_REF], [START_REF] Hog | Adaptable web service registry for publishing profile annotation description[END_REF], [START_REF] Yoo | Ontology based keyword dictionary server for semantic service discovery[END_REF], [START_REF] Jonas | A description and retrieval model for web services including extended semantic and commercial attributes[END_REF], [START_REF] Narock | A provenance-based approach to semantic web service description and discovery[END_REF], [START_REF] Moradyan | A query ontology to facilitate web service discovery[END_REF], [START_REF] Ben | Towards a semantic search engine for open source software[END_REF], [START_REF] Kavitha | Towards a novel conceptual framework for analyzing code clones to assist in software development and software reuse[END_REF] [START_REF] Goncharuk | A case study on pragmatic software reuse[END_REF] + +

[15] + + + [START_REF] Loskyll | Semantic service discovery and orchestration for manufacturing processes[END_REF] + [START_REF] Seba | Web service matchmaking by subgraph matching[END_REF], [START_REF] Aabhas V Paliwal | Semantics-based automated service discovery[END_REF], [START_REF] Xue | Restful web service matching based on wadl[END_REF] + [START_REF] Rathore | An arsm approach using pcb-qos classification for web services: a multi-perspective view[END_REF], [START_REF] Becha | Prioritizing consumer-centric nfps in service selection[END_REF], [START_REF] Amandeep | Software reuse analytics using integrated random forest and gradient boosting machine learning algorithm[END_REF] + (+) [START_REF] Ángel Rodríguez-García | Ontology-based annotation and retrieval of services in the cloud[END_REF], [START_REF] Kapitsaki | Annotating web service sections with combined classification[END_REF], [START_REF] Niranjan | Dynamic search and selection of web services[END_REF] + [START_REF] Li | An ontology-based process description and reasoning approach for service discovery[END_REF], [START_REF] Matsuda | Configuration of a production control system through cooperation of software units using their capability profiles in the cloud environment[END_REF] + (+) [START_REF] Alarcon | Rest web service description for graph-based service discovery[END_REF] + + [START_REF] Elshater | godiscovery: Web service discovery made efficient[END_REF] + + [START_REF] Boissel-Dallier | Mediation information system engineering based on hybrid service composition mechanism[END_REF] + (+) [START_REF] Khanfir | Quality and context awareness intention web service ontology[END_REF] + + + [START_REF] Sophea Chhun | Qos ontology for service selection and reuse[END_REF] + + (+) [START_REF] Purohit | Web service selection using semantic matching[END_REF] + [START_REF] Elgazzar | Daas: Cloud-based mobile web service discovery[END_REF], [START_REF] Zeshan | Ontology-based service discovery framework for dynamic environments[END_REF] + + + [START_REF] Mu | An ontology-based collaborative business service selection: contributing to automatic building of collaborative business process[END_REF] + + (+)

Table 1 Service repository and discovery for reuse

Scientific relevance and discussion

From the state-of-the-art on service-oriented software reuse, we analyzed that currently ad-hoc methods are still used to identify the most suitable serviceoriented software or artifacts to reuse, and a methodology or standardized process enabling this is still missing. Moreover, the description, the capability, or qualification of this software are lacking wider view qualification taking into consideration the business, operational and technical views of the software and their related services [START_REF] Belfadel | Semantic software capability profile based on enterprise architecture for software reuse[END_REF]. In addition, no solution has been provided to fit the requirements engineering along with the impact of architecture on requirements when dealing with the identification of the most suitable components and avoiding the misevaluation during the selection phase. Therefore, enhancing the capability description of the software and its related services in different levels of service description, along with its exploitation based on requirement engineering and architecting actions is a big challenge. This analysis highlighted the need for an Enterprise Architecture-based methodology for describing and classifying different artifacts to be available as building blocks for reuse in future projects.

From the above analysis, we propose the following research directions: (i) Improve software and related service capability profile to bring value-in-use of the qualified feature for an organization that is interested in reuse; (ii) Shape a mechanism to identify the most suitable software with specific features or functionalities helping to overcome the use of ad-hoc methods; (iii) Improve the reuse of service-oriented solutions by considering a process that includes requirements engineering and enterprise architecture for formalizing the requirements.

Qualification Model -Software Capability Profile

To bring the value-in-use of existing software and facilitate the discovery and reuse, we present in this section the meta-model of the Software Capability Profile (see Figure 1) and its related EACP Ontology that is presented in detail in [START_REF] Belfadel | Semantic software capability profile based on enterprise architecture for software reuse[END_REF] and depicted in Figure 2. The meta-model is inspired mainly from TO-GAF [START_REF] Hussain | The Open Group Architecture Framework TOGAF™ Version 9[END_REF], ISO 16100 [START_REF]2009 industrial automation systems and integration -manufacturing software capability profiling for interoperability -part 1: Framework[END_REF], Microsoft Application Architecture Guide [START_REF]Microsoft Patterns and Practices Team. Microsoft® Application Architecture Guide, 2nd Edition (Patterns and Practices)[END_REF] and ISO 25010 [START_REF]2011 systems and software engineering -systems and software quality requirements and evaluation (square) -system and software quality models[END_REF]. It aims to gather functional and non-functional specifications; the organizational impact of an organizations' software; and it links the business services to their related physical components to offer a wider view qualification and improve the reuse when developing a new business application. The proposed meta-model is composed of 6 packages. i) Organization package: Composed by the organizational unit, with its related business goals and objectives that guided the development of existing software. ii) Architecture Building Blocks package: This entity is constructed according to the life-cycle creation of Architecture Building Blocks (ABBs) based on the ADM Method. An ABB describes the business problem for which this component was developed for, its implementation specification, standards used, the stakeholders concerned. It provides other details such as the operational vision of the component, the definition of the business function of the ABB, its attributes and constraints, data and application interoperability requirements and designtime quality attributes. iii) Solution Building Blocks package: SBBs represent the physical equivalent of ABBs and describe the components exposed by software. The SBB is linked to the exposed service or API for instance over the web in case of a REST-based application. This latter is defined by the URI, the HTTP method needed to get access to the resource, the related parameters and the serialization used in communication (for instance JSON). It defines run-time and transversal quality attributes which might be updated according to the defined frequency for each attribute. iv) Application package: Describes the technical requirements of the service-oriented software in general with its exposed components (for instance REST services). It also describes the execution environments on which the application is running. v) Business Process package: This package is used in the exploitation phase and represents the "tobe" business application to realize. vi) Requirements package: This package is used in the exploitation phase and represents the requirements elicitation process, helping to guide the developer or the architect during the engineering life-cycle. The requirements are elicited in each phase of the ADM, going from the definition of project driver to the definition of the use cases and requirements in different levels. The resulting EACP profile instances are saved in a semantic repository called in this context the Enterprise Architecture Knowledge Repository (EAKR repository) as an ontology instance. Regarding the design effort of the EACP Ontology, we identified from state-of-the-art solutions some existing ontologies to reuse. We have selected those that cover some of our needs and that are well-defined, consistent, and reused in other projects. We selected Basic Formal Ontology (BFO) which is a top-level ontology and four domain ontologies, namely Ontology Web Language for Services (OWL-S) [START_REF] Martin | Bringing semantics to web services: The owl-s approach[END_REF], The Open Group Architecture Framework ontology (TOGAF-Ontology) [START_REF] Gerber | Towards the formalisation of the togaf content metamodel using ontologies[END_REF], BPMN 2.0 Ontology [START_REF] Rospocher | An ontology for the business process modelling notation[END_REF] and Information Artifact Ontology (IAO) [START_REF] Ceusters | An information artifact ontology perspective on data collections and associated representational artifacts[END_REF]. Third, we managed the selected foundational and domain ontologies, by integrating and extending in Fig. 2 Basic pattern of the main classes and relationships in the EACP ontology a coherent way the different ontologies into the targeted EACP ontology using the Protégé Ontology Editor. Finally, we evaluated the consistency of the resulted model using the Fact++ reasoner. An extract of the related Ontology to EAKR repository is presented in Figure 2.

The scope of this paper does not concern the presentation of the qualification model and the design of its ontology mentioned above and presented in [START_REF] Belfadel | Semantic software capability profile based on enterprise architecture for software reuse[END_REF], however, the elements presented above are enough for the understanding of the exploitation phase that will follow.

Use Case Scenario

This section presents the use case that will serve as an example for the description of the following exploitation process. This use case scenario involves two companies. The first company is specialized in plastic manufacturing, and the second in metal manufacturing. Both companies have significant expertise in engineering and transforming plastic and metal, respectively, parts using several technologies. Their key business issue is the difficulty to detect the Fig. 3 Screenshots of the targeted business application most appropriate business collaboration opportunities among common customer projects. Starting from a Computer-Aided Design (CAD) description of customer projects, the companies' consortium needs to quickly detect the set of projects that they are enabled to produce. The proposed use case aims to accelerate and maintain a collaboration channel in two complementary business domains. The objectives are to reduce project quotation costs and reduce the delay of customer quote treatment.

Currently, clients send product requests to one of the companies in the form of CAD/PDF files. Then, the chosen company decomposes all the project's features (e.g. parts, dimensions, type of surface, and type of raw material) to understand customer needs to verify the feasibility of the product and to determine the relevance of the business opportunity in terms of return on investment. After the decomposition and if there is a need for subcontracting (especially for multi-physical and complex products), the two companies will carry out a succession of negotiations, explore several ways to reach the client's requirements, and submit their best offer to the client. For this purpose, we derive from this use case all needed requirements that we need to discover existing technical services that allow reducing cost and development time. In what follows, we present how the developer goes through an architecture and requirement elicitation process to discover existing services and develop the needed business application. We present an example of the inputs needed in each phase of the exploitation process. A screenshot of the developed prototype is presented in Figure 3.

Exploitation Process

To design a new business application reusing technical services from the EAKR, the architect or developer goes through a requirement elicitation process. This Fig. 4 Exploitation Plan process depicted in Figure 4 is structured in several phases starting with the architectural vision, going through the business architecture, data, application, and technology architecture phase, leading to the generation of an implemented BPMN which uses the qualified services if a match is confirmed.

In the following sub-sections, we describe the actions to realize in each phase, enriched with a concrete example from the use case scenario to strengthen the understanding. Templates in JSON format are also proposed to formalize the architecture artifacts and requirement specifications in each phase.

Phase A: Architecture vision

The objective of this phase is to develop a high-level vision of the business value to be delivered as a result of the project. This phase is mainly focused on gathering the business goals and related objectives of the targeted project.

Other architecture artifacts are used to structure the project drivers, such as the identification of stakeholders, definition of the organizational model of the company, and KPIs enabling to evaluate the targeted business application.

Based on the architectural artifacts of phase A (see Figure 5 for the exhaustive list -column ADM artifacts), we fetch requirement patterns (see Figure 5 for the exhaustive list from Volere specification -column Requirements) produced during previous projects to guide and support the developer for the upcoming requirement definition. If a template is found, it is presented to the developer. In addition to the architecture artifacts, the developer formalizes his requirements by defining the project drivers such as the business actors, the client, and the customer if applicable. These inputs help to consolidate the elicitation phase and redesign his requirements before going further in the process. All the artifacts once validated are saved in the EAKR to be reused as requirements templates in the future exploitation process.

Fig. 7 Phase B: alignment of architecture and requirements artifacts Figure 6 illustrates an example from the use case with some proposed architecture artifacts and requirements for phase A. The main inputs are the definition of business goals and objectives of the targeted system, along with stakeholders that define people who have an interest in the targeted system and whose inputs are needed to build the product.

Phase B: Business Architecture

The objective of this phase is to develop the target business architecture that describes how the enterprise needs to operate to achieve the business goals previously defined and responds to stakeholder concerns. This phase focuses on the business side and supports the developer or architect to prepare all required inputs which are presented in Figure 7.

The most important architectural artifact in this phase is the high-level business scenario. This is designed using BPMN which is a standard language for business process modeling. This first high-level modeling is designed using ArchiMate 1 which is recognized as a standard for EA modeling by the Open Group [START_REF] Josey | An introduction to the archimate® 3.0 specification[END_REF] and that supports business process modeling. This high-level modeling helps to define the business-entity relationship to know which entities are needed for every business action or behavior.

This business model is enriched with other architectural artifacts (see Figure 7 for the exhaustive list -column ADM artifacts) such as the actor catalog updated with their related roles, and the definition of the architecture requirements specification which form a major component of an implementation contract and provides quantitative statements as required in ADM Phase B outputs. It requires the definition of the implementation specifications to guide the development work, implementation standards in case the implementation should follow some specific standard. Figure 8 depicts the model of some architecture artifacts managed during this phase and shows an example of the proposed template for some of these architecture artifacts.

Once these elements are defined, a request is sent to the EAKR to fetch requirement templates of phase B produced during the last projects to be reused. The aim is to guide the developer to define the project constraints and the functional requirements as depicted in Figure 7 and inspired from Volere specification (column Requirement). The resulted templates from the request (if any) present the scope of previous projects sharing the same context, the existing business events connected to the actual business scenario, the use cases of the project or solution, and a set of functional requirements related to the selected use cases and their type, i.e service type component related to an SBB or user task activity if it is a user action. Figure 9 depicts the model of the different artifacts that may result from the EAKR and shows an example of the proposed template for some of these artifacts.

These resulting templates are presented to the developer to guide him during this phase B for the consolidation and refinement of his requirements. It helps to offer support for defining and consolidating the use-cases and related Fig. 9 Example of requirement artifacts managed during phase B and related model functional specifications. The proposed template is inspired by the Atomic Requirement Template which is proposed by [START_REF] Robertson | Mastering the requirements process: Getting requirements right (3rd Edition)[END_REF] and depicted in Figure 10. This phase B ends with well formalized, testable, and categorized as user or service task functional requirements.

Phase C: Information Systems Architecture -Data Architecture

The objective of Phase C is to develop the targeted information system architecture. It involves a combination of data and application architecture. There- The Data architecture phase enhances the definition of the relationship between data entities and targeted business functions previously defined in phase B. We have already depicted in Figure 9 the models that enable to link data entities associated with each business function. Then, the needed action in this phase is to define the properties of each business entity involved in the business functions using relevant data models such as the Class Diagram in the Unified Modeling Language (UML). To this end, we propose templates based on the proposed models for the definition and formalization of the data entities involved in a business function. An example related to the use case is depicted in Figure 12. The left side of the figure depicts the definition of a class model, and the right-side links an entity with its attributes to a specific business function where the entity is used.

Additional architecture requirements specifications are as well formalized such as Data Interoperability or Technology Architecture Constraints (see Figure 11 for the exhaustive list -column ADM artifacts). These constraints have the same description template as for requirements. The data interoperability requirement is needed to formalize specific needs for security policies as for example input validation or for data format and serialization. Regarding the During this phase, architecture artifacts and requirements are defined at the same time because we are reaching the low-level description regarding the business application to develop. Based on these inputs, we fetch and map in the EAKR the ABBs and business functions using the defined data entities, and which are compliant with the constraints if defined (see Figure 13-left column for an ABB template example). The related SBBs and their corresponding technical components are gathered to highlight potential problems of integration and are presented in the proposed template depicted in Figure 13-right column. The related models of ABB, SBB and application package have already been described in section 3 and in [START_REF] Belfadel | Semantic software capability profile based on enterprise architecture for software reuse[END_REF]. This phase deals with the application architecture artifacts and the corresponding requirements. (see Figure 14 for the exhaustive list of the artifacts). The developer or architect is guided to define the technical requirements in the same template as for the atomic requirement (see Figure 15-left side for an example). Technology or infrastructure constraints and application interoperability requirements are either defined in this phase. Those constraints are added to previous ones to fetch for SBBs and related applications in the EAKR. The resulting SBBs and related application (middle and right side of Figure 15) offer the first overview of existing applications and related technical services (in the case of service-oriented solutions) to reuse. These solutions fit the requirements and constraints from a functional, technical, and technology constraint side. Up to this requirement level, a first version of the targeted business application based on BPMN 2.0 is generated. The user and service tasks are generated and a link between service tasks and a set of existing services is performed based on the elements defined during previous phases (related to selected SBBs). This first solution reflects the prototype to realize, aiming to resolve and meet the business need expressed during this elicitation process.

Phase D: Technology Architecture

The last phase D is about the technology architecture artifacts (see Figure 16 for the exhaustive list of the artifacts). The objective of this last phase is to define the basis of the implementation work. As part of phase D, the developer or architect needs to consider what relevant resources are available in the EAKR repository to ensure that the target system will meet some or all the requirements and constraints. It is important to recognize that in practice it will be rarely possible to find and reuse components that reach 100% coverage of all defined requirements and constraints. During the previous phase C, technical and technological constraints are formalized. These latter are considered during this phase D when matching the final SBBs, enriched with non-functional properties defining the Quality of Service needed from the existing services.

The model of non-functional requirement is based on the atomic requirement model. An example of the definition of this non-functional requirement is depicted in Figure 17. The resulted SBBs, if a match is confirmed, reflects strongly the defined requirements and constraints. This helps to implement the business process already produced during the last phase with the final SBBs, and related services with their service endpoints to support the business application. The resulted SBBs are ranked as already defined by [START_REF] Benfenatki | Linked usdl extension for describing business services and users' requirements in a cloud context[END_REF] for QoS ranking, reflecting the non-functional specifications before selecting the final SBB and generating an implemented business process. The result of this rank- ing process is used during the generation of the implemented BPMN, where for each business function (only service tasks), we assign the first ranked SBB to the related task (see Figure 18 for an example). In the next section, we present the implementation of a prototype of this exploitation process developed as a Web Application.

Framework Implementation

We implemented the exploitation process as a Web Application as depicted in Figure 19. The source code is available at Github repository2 . The video of this technical presentation is available here3 and the of the entire use case is available here4 . We selected AngularJS [START_REF] Green | AngularJS[END_REF] as a Web Framework that enables the development of single-page applications following the MVC (Model-View-Controller) pattern for the front-end environment, and NodeJS Framework [START_REF] Cantelon | Node. js in action[END_REF] which is a popular platform for building server-side Web Applications written in Javascript. Regarding the EAKR repository, we deployed the EACP Ontology along with example of qualified open-source solutions from vf-OS 5and FITMAN project6 in Apache Jena Fuseki [START_REF] Jena | Fuseki: serving rdf data over http[END_REF] (see Figure 20).

In the following subsections, we describe how a developer or architect can interact with this application in each phase, what inputs are required (based on the use case presented earlier in this paper), how information is presented, and how validation occurs.

Note that in the case where no artifact was found in the repository with a perfect match, we used string similarity based on Dice's coefficient. Several open-source JavaScript packages exist. We selected the string-similarity pack- age that is publicly offered in GitHub repository 7 . We fixed the threshold to 90%, which could be modified to get flexible results.

Phase A: Architecture Vision

In this phase, one of the artifacts to provide is about the business goals and associated objectives of the targeted project. The offered design possibility is to upload the inputs designed in ArchiMate using the motivation extension. Figure 19 depicts an example from the proposed use case of the motivation diagram. An export in XML format is needed to import it to the EACP Web Application to parse it and retrieve the needed inputs for phase A. Figure 19 depicts phase A of the Web application. The first column is the architecture and requirements elicitation process that guides the developer to consolidate and validate their requirements during this phase. The second column displays the actual phase state and the progression rate of the process. The developer can as well add other stakeholders not mentioned in the motivation diagram to be considered for the next actions.

Once the motivation diagram is uploaded to the framework, a parsing of the XML source file is realized to retrieve the defined business goals and objectives. Based on these inputs, a request is sent to the EAKR (see an example of a SPARQL request in Figure 20) to fetch existing requirement templates guiding the developer during this requirement elicitation phase. Since it is the first instance of this process, we are not supposed to get any template. However, and for illustrative reasons, we defined one template that shares the same business goal to have an example of a template to reuse for defining and consolidating the required requirements for this phase. As we may notice in Figure 19, the requirements needed are the definition of the business context, the client and the customer of the system which is not applicable in this context, and the users that will interact with the targeted system. The retrieved templates are presented on the "EAKR Templates Requirement" side. The process progression column is updated, and the application now is waiting for the validation of the requirements to redirect the developer to phase B of the exploitation process.

Phase B: Business Architecture

Based on the ArchiMate Business-Entity Relationship diagram, the developer uploads the designed diagram to the architecture artifacts user interface. This latter is parsed to retrieve the actors, the business processes, and related data entities involved in each business process or use case. These inputs are considered during the requirement pattern search in the EAKR repository and retrieved using the process depicted in section 5.

The requirements specification of phase B deals with the functional requirements and constraints of the project. Based on the use case list and their related data entities, we fetch the previous project that has been saved to the EAKR based on a string similarity. These existing requirements help to offer support for defining and consolidating the use-cases and functional specifications close to the actual context, the business events connected to the actual Fig. 21 EACP Web Application -Phase B : Requirement Specification business scenario and a set of functional requirements related to the selected use cases and their type (i.e service type component related to an SBB or user task activity if it is a user action). In the case of our business scenario, no template has been found but for illustrative reasons, we initialized requirement templates that correspond to the actual business scenario to be reused.

In this phase, there is a possibility to enrich the functional specifications by adding required constraints or architecture requirements specifications such as the specification of implementation or usage of a specific standard for the future development of the functional requirements. In the context of this proposed scenario, we link an implementation standard to the functional requirement "Visualize CAD file" as depicted in Figure 21.

Phase C: Data and Application Architecture

The Data architecture phase enhances the definition of the relationship between data entities and targeted business functions previously defined in phase B. Then, the next needed action is to define the properties of each business data involved in the business functions using relevant data models such as the Class Diagram in Unified Modeling Language (UML) that is serialized to retrieve the entities with their related attributes.

Based on these inputs, the application fetches and maps in the EAKR the business functions with the architecture building blocks using the defined data entities, and which respects the interoperability and infrastructure constraints as defined in section 5.3. This latter matches the defined functional requirements with business functions defined in the ABB model. ABBs that Fig. 22 EACP Web Application -Phase C : Requirement Specification correspond to the conditions are selected with their related SBB and corresponding applications. The objective is to highlight potential problems of integration in case any selected ABB presents data interoperability constraint which is different from the defined constraint in this phase C. Regarding the Application Architecture phase, the developer is guided to define the technical requirement using the same template as for the functional requirements. Technology or infrastructure constraint is either defined. Those constraints are added to previous ones to select the SBBs as described in section 5. For instance, in this use case scenario, we define a technical requirement related to the targeted business function "Visualize CAD File". Indeed, we target an SBB which manages the CAD Objects with a specific file extension "STL extension", and that is based on the JavaScript library Three.js. Then the action "Fetch ABBs" triggers the selection of the targeted ABBs and related SBBs in the EAKR that respect the defined technical requirement for each business function along with the technology constraints if defined. The result of this action is depicted in Figure 22.

To this level, these inputs enable to download a first version of the targeted business application based on BPMN 2.0 specification. Based on the functional requirements defined in phase B which are composed by user and service tasks, we generate an XML template (see Figure 18).

Phase D: Technology Architecture

During the previous phase, technical and technological constraints are formalized. These latter are considered when matching the final SBBs, enriched in this phase with non-functional properties defining the Quality of Service Fig. 23 EACP Web Application -Phase D : Requirement Specification needed from the existing services. This to consider what relevant resources are available in the EAKR repository to ensure that the target system will meet the requirements and constraints. In the proposed use case scenario, we define an example for the QoS which is depicted in Figure 23 (NFR List). We set the average instance time metric as a non-functional requirement applicable for all the targeted technical services. After validation, SBBs are ranked based on the defined QoS threshold values.

For each business function, we select the first SBB resulted from the ranking process as a building block to reuse for the implementation of the targeted business application. As a final result, we get a last version of an implemented BPMN with the related service endpoints of the solution building blocks.

Discussion

In this work, we propose an Enterprise Architecture Capability Profile specifically designed for service-oriented software enabling the qualification, the discovery, reuse, and sustainability for new business applications development. We demonstrate how the proposed approach can assist developers or architects in the qualification process using the semantic Enterprise Architecture Knowledge Repository, based on a proposed meta-model inspired mainly from TOGAF and ISO 16100 Standard and formalized using semantic web techniques. This helps to offer a wider view qualification process that deals with the two perspectives of services which are the business perspective which brings value-in-use of the qualified feature for an organization that is interested in reuse, and the technical side along with a quality of service of the feature encapsulated by the software service. An exploitation methodology is defined to overcome the use of ad-hoc methods to identify the most suitable compo-nents or artifacts to reuse. The proposed solution is designed based on the alignment of architecting actions with a requirement engineering process, and evolve together helping to investigate the highest functional compatibility of the desired functionalities and their related constraints.

As discussed in [START_REF] Eeles | Capturing architectural requirements[END_REF], on some projects, architectural requirements can be significantly more important than their domain-specific equivalents (as for instance, if we are designing a business application with a specific high availability as implementation constraint, the "up-time" metric would be with a high importance). Regarding the proposed exploitation methodology, it carries the validation of the requirements and drives the design of the foundations (i.e., architecture) and the requirement definition of the business application we are building. This means at least, we offer the necessary structure for defining and validating architectural artifacts and requirement specifications, and at best, propose templates and artifacts of previous projects or qualified solutions for recycling and reuse to meet the business need.

Regarding the exploitation process, as you may notice at run-time, the process finds few results because no previous project with its related requirements has been already introduced and capitalized. Also, it depends on the number of qualified solutions and related services considered as architecture and solution building blocks in the EAKR Repository. Continuous qualification is needed to maximize the exploitation and must be realized frequently to take full advantage of this proposed methodology.

Conclusion

In this work, we defined the Enterprise Architecture Capability Profile that describes the business, operational and technical aspects for service-oriented software. It is designed based on an Enterprise Architecture Framework (TO-GAF) and the best practices related to the implementation of ISO 16100 standard concepts. An exploitation methodology of the designed capability profile is proposed and based on the alignment of a requirements engineering process with the Architecture Development Method from TOGAF. These latter evolve together to investigate the highest functional and technical compatibility of the desired functionalities and related constraints, respond to end-user requirements, and efficiently reuse the qualified solutions. Finally, we provided an implementation with an industrial use case to demonstrate the effectiveness of this approach. Concepts presented in this research work have been implemented as open-source prototypes based on Node JS and Java platforms. These prototypes cover the entire exploitation process that leads to the targeted ready-to-use business application. and innovation programme under grant agreement no. 723710. The content of this paper does not reflect the official opinion of the European Union. Responsibility for the information and views expressed in this paper lies entirely with the authors.

Fig. 1

 1 Fig. 1 Proposed meta-model

Fig. 5 Fig. 6

 56 Fig. 5 Phase A: alignment of architecture and requirements artifacts

1Fig. 8

 8 Fig. 8 Example of architecture artifacts managed during phase B and related model

Fig. 10

 10 Fig. 10 Phase B: requirements template selection

Fig. 11

 11 Fig. 11 Phase C -Data Architecture: alignment of architecture and requirement artifacts

Fig. 12

 12 Fig. 12 Data Architecture artifacts example for Phase C

Fig. 14

 14 Fig. 14 Phase C -Application Architecture: alignment of architecture and requirement artifacts

Fig. 16

 16 Fig. 16 Phase D: Alignment of Architecture and Requirements artifacts

  Fig. 17Phase D: Technology architecture artifacts template example

Fig. 18

 18 Fig. 18 Example of an implemented BPMN resulted from Phase D

Fig. 19 EACP

 19 Fig. 19 EACP Web Application -Phase A : Architecture Artifacts

https://github.com/AbdBelf/EacpFramework

https://bul.univ-lyon2.fr/index.php/s/xsAMwEoYIbRYbLh

https://bul.univ-lyon2.fr/index.php/s/EfoSLyZwkHYbT9t

www.vf-OS.eu

http://www.fiware4industry.com

https://www.npmjs.com/package/string-similarity

Acknowledgment

This paper presents work developed in the scope of the project vf-OS. This project has received funding from the European Union's Horizon 2020 research


Gilles Dowek
email: gilles.dowek@polytechnique.edu

From proof theory to theories theory

In the last decades, several objects such as grammars, economical agents, laws of physics... have been defined as algorithms. In particular, after Brouwer, Heyting, and Kolomogorov, mathematical proofs have been defined as algorithms. In this paper, we show that mathematical theories can be also be defined as algorithms and that this definition has some advantages over the usual definition of theories as sets of axioms.

The logic and the theories When constructing a proof, we use rules that are specific to the objects the proof speaks about and others that are ontologically neutral. We call the rules of the first kind theoretical rules and those of the second logical rules.

The position of the border delimiting the logic from the theories is not always clear and, for instance, it can be discussed if the notion of set belongs to the realm of logic or to that of a specific theory. It seems that the dominant point of view at the end of the XIX th and at the beginning of the XX th century-Frege, Whitehead and Russell, ...-was that this notion of set, or of concept, was logical. But Russell's paradox seems to have finally ruined this point of view: as we must give up full comprehension, and either restrict comprehension to specific propositions, as in Zermelo set theory, or add a type system as in the Principia Mathematica, there are too many ways to do so-with or without the replacement axiom, with or without transfinite types-hence the notion of set is theoretical. We may speculate that, even if full comprehension had not been contradictory, this idea that the notion of set is ontologically neutral would have been finally given up, as even with full comprehension, there still would have been choices to be made for the set existence axioms: first because comprehension depends on the choice of a language, then because other set existence axioms, such as the axiom of choice may be added.

This understanding of the theoretical nature of the notion of set has lead, at the end of the twenties, to a separation of set theory from predicate logic and to the constitution of predicate logic as an autonomous object. As a corollary, it has been assumed that any theory should be expressed as a set of axioms in predicate logic. As we shall see, and this will be the main thesis of this paper, this corollary is far from being necessary.

From a historical point of view

The constitution of predicate logic as an autonomous object, independent of any particular theory, and the simplicity of this formalism, compared to any particular theory such as geometry, arithmetic, or set theory, has lead to the development of a branch of proof theory that focuses on predicate logic. A central result in this branch of proof theory is the cut elimination theorem: if a sequent Γ ⊢ A has a proof, it also has a cut-free proof, both in natural deduction and in sequent calculus.

Once we have a notion of proof of a sequent in predicate logic, we may define a notion of proof of a sequent in a theory-i.e. a set of axioms-T , and say that a proof of the sequent Γ ⊢ A in the theory T is a proof in predicate logic of a sequent Γ, T ′ ⊢ A, where T ′ is a finite subset of T . And from results about proofs in predicate logic, we may deduce results about proofs in arbitrary theories. For instance, a cut elimination theorem: if a sequent Γ ⊢ A has a proof in a theory T , it has a cut free proof in this same theory.

Yet, although such results do have some content, they often are disappointing: they do not say as much as we could expect. For instance, the cut free proofs of a sequent ⊢ A in predicate logic always end with an introduction rule, but this in not the case for the cut free proofs in a theory T . Thus, while a corollary of the cut elimination theorem for predicate logic is that there is no proof of the sequent ⊢ ⊥ in predicate logic, this corollary does not extend to arbitrary theories. And, indeed, there are contradictory theories.

Thus, this definition of a cut free proof of a sequent Γ ⊢ A in a theory T as a cut free proof of a sequent Γ, T ′ ⊢ A for some finite subset T ′ of T is not satisfactory, as the existence of such cut free proofs does not imply the consistency of the theory. In the same way, it does not imply the disjunction or the witness property for constructive proofs.

Thus, this approach to proof theory focused on predicate logic has been unable to handle theories in a satisfactory way. This may be a sign that the definition of the notion of theory as a set of axioms is too general: not much can be said about a too large class of objects and a more restrictive notion of theory might allow to say more about theories.

From a historical point of view, proof theory has side stepped this problem in at least three ways. First, some results, such as cut elimination theorems, have been proven for specific theories, for instance arithmetic. Virtually, any set of axioms yields a new branch of proof theory. Then, the separation between the logic and the theories has been criticized and extended logics have been considered. Typical examples are second-order logic, higher-order logic, Intuitionistic type theory [START_REF] Martin-Löf | Intuitionistic type theory[END_REF], the Calculus of constructions [START_REF] Coquand | The Calculus of constructions[END_REF], ... Finally, the idea that the proofs studied by proof theory are proof of mathematical theorems, and thus require a theory, has be given up and proofs have been studied for for their own sake. A typical example is linear logic [START_REF] Girard | Linear logic[END_REF].

The thesis we shall develop in this paper is that there is another possible way to go for proof theory: modify the notion of theory so that it can be properly handled, without focusing on a single theory, such as arithmetic, and without introducing logics beyond predicate logic, such as second-order logic. This way leads to a branch of proof theory that may be called the theory of theories.

Some technical problems with axioms

We have seen that the cut elimination theorem for predicate logic implies that there is no proof of the sequent ⊢ ⊥ in predicate logic, but that this result does not extend to an arbitrary theory. Let us now consider a more evolved example.

A consequence of the cut elimination theorem is that a bottom up proof search in sequent calculus is complete, even if it is restricted to cut free proofs. In the search for a proof of the sequent ⊢ ⊥, no rule of the cut free sequent calculus applies-except structural rules in some versions of the sequent calculus-and the search fails in finite time. In contrast, the search for a cut free proof of the sequent ⊢ ⊥ in the theory ∀x (P (x) ⇔ P (f (x))), i.e. for a cut free proof of the sequent ∀x (P (x) ⇔ P (f (x))) ⊢ ⊥ in predicate logic, generates an infinite search space. Thus, although the cut elimination theorem allows to reduce the size of the search space, by restricting the search to cut free proofs, it does not allow to reduce it enough so that the search for a proof of a contradiction in the theory ∀x (P (x) ⇔ P (f (x))) fails in finite time. This proof search method "does not know" [START_REF] Dowek | What do we know when we know that a theory is consistent? R. Nieuwenhuis[END_REF] that this theory is consistent and indeed the cut elimination theorem for predicate logic does not imply, per se, the consistency of any non-empty set of axioms.

In order to design a complete proof search method for this theory, that fails in finite time when searching for a proof of ⊢ ⊥, we may attempt to prove a cut elimination theorem, specialized for this theory, that implies its consistency, in the same way as the cut elimination theorem for arithmetic implies the consistency of arithmetic.

However, when attempting to follow this path, the first problem we face is not to prove this cut elimination theorem, it is to state it: to define a notion of cut specialized for this theory. Indeed, although there is an ad hoc notion of cut associated to the axioms of arithmetic-a sequence where a proposition is proven by induction and then used in a particular case-there is no known way to associate a notion of cut to an arbitrary set of axioms.

Among the tools used in proof theory, only one generalizes smoothly from predicate logic to arbitrary sets of axioms: the notion of model. Indeed, not only the definition of the notion of model extends from predicate logic to arbitrary sets of axioms, but the completeness theorem also does. In this respect, there is a clear contrast between the notion of model and that of cut. And the definition of the notion of theory as a set of axioms appears to be tailored for the notion of model and not for that of cut.

Two partial solutions

There are several cases where this problem of the definition of the notion of cut associated to a theory has been addressed and where partial solutions have been proposed. When enumerating these cases, we also have to include cases where a proof search method has been proven complete. Indeed, as shown by Olivier Hermant [START_REF] Hermant | Resolution modulo as the cut-free fragment of sequent calculus modulo[END_REF], the completeness of a proof search method is often not only a consequence of a cut elimination theorem, but it is also equivalent to such a theorem.

Let us start with a slightly artificial example: that of definitions. If we want to use a new proposition symbol P as an abbreviation for a proposition A ∧ B, we can either keep the same language and consider each occurrence of the symbol P as a notational variant for A ∧ B, or extend the language with the symbol P and add the axiom P ⇔ (A ∧ B). Obviously, the same propositions can be proven in both cases and from the cut elimination theorem for predicate logic, we should be able to derive the consistency of the empty theory, and hence that of the theory P ⇔ (A∧B). In the same way, from the cut elimination theorem for predicate logic, we should be able to derive the completeness of a proof search method that first uses the axiom P ⇔ (A∧B) to replace all the occurrences of P by A ∧ B in the proposition to be proven and then searches for a cut free proof of the obtained proposition.

A direct cut elimination proof for this theory can be given following an idea of Dag Prawitz [START_REF] Prawitz | Natural deduction. A Proof-Theoretical Study[END_REF]. In constructive natural deduction, we can replace the axiom P ⇔ (A ∧ B) by two theoretical deduction rules

Γ ⊢ A ∧ B fold Γ ⊢ P and Γ ⊢ P unfold Γ ⊢ A ∧ B
and extend the notion of cut in such a way that the sequence of a fold rule and an unfold rule is a cut. Cut elimination can be proven for this theory and like in predicate logic, a cut free proof always end with a introduction rule-considering the fold rule as an introduction rule and the unfold rule as an elimination rule. Thus, all the corollaries of cut elimination that are based on the fact that the last rule of a cut free proof is an introduction rule, such as consistency, the disjunction property, the witness property, ... generalize.

Of course, there is nothing specific to the proposition A∧B in this example and we can do the same thing with any theory of the form P 1 ⇔ A 1 , ..., P n ⇔ A n where P 1 , ..., P n are proposition symbols that do not occur in A 1 , ..., A n . This class of theories is quite small and it is fair to say that all these theories are trivial. Yet, we may notice that a notion of cut has been defined for a class of theories that contains more than just one theory. Besides this quite artificial example of definitions, this idea of using theoretical deduction rules has been investigated by Dag Prawitz [START_REF] Prawitz | Natural deduction. A Proof-Theoretical Study[END_REF], Marcel Crabbé [START_REF] Crabbé | Non-normalisation de la théorie de Zermelo[END_REF][START_REF] Crabbé | Stratification and cut-elimination[END_REF], Lars Hallnäs [START_REF] Hallnäs | On normalization of proofs in set theory[END_REF], Jan Ekman [START_REF] Ekman | Normal proofs in set theory[END_REF], Sara Negri and Jan von Plato [START_REF] Negri | Structural proof theory[END_REF], ... More precisely, the fold and unfold rules can be used each time we have a theory of the form ∀(P 1 ⇔ A 1 ), ..., ∀(P n ⇔ A n ) where P 1 , ..., P n are arbitrary atomic propositions. In particular, this can be applied successfully to set theory where, for instance, the axiom ∀x∀y (x ∈ P(y) ⇔ ∀z (z ∈ x ⇒ z ∈ y)) can be replaced by two rules

Γ ⊢ ∀z (z ∈ x ⇒ z ∈ y) fold Γ ⊢ x ∈ P(y) and Γ ⊢ x ∈ P(y) unfold Γ ⊢ ∀z (z ∈ x ⇒ z ∈ y)
A remark due to Marcel Crabbé [START_REF] Crabbé | Non-normalisation de la théorie de Zermelo[END_REF] is that there are theories for which cut elimination does not hold. For instance with the rules

Γ ⊢ P ⇒ Q fold Γ ⊢ P and Γ ⊢ P unfold Γ ⊢ P ⇒ Q
we have a proof of Q but no cut free proof of Q. Yet, whether or not cut elimination holds, the notion of cut can be defined and the cut elimination problem can be stated for all these theories.

A second example comes from an attempt to handle equality in automated theorem proving. It has been remarked for long that considering equality axioms such as ∀x∀y∀z (x + (y + z) = (x + y) + z)

together with the axioms of equality generates a very large search space, even when this search is restricted to cut free proofs. For instance, attempting to prove the proposition

P ((a + b) + ((c + d) + e)) ⇒ P (((a + (b + c)) + d) + e)
we may move brackets left and right in many ways, using the associativity axiom and the axioms of equality, before reaching a proposition that has the form A ⇒ A. An idea, that goes back to Max Newman [START_REF] Newman | On theories with a combinatorial definition of "equivalence[END_REF], but that has been fully developed by Donald Knuth and Peter Bendix [START_REF] Knuth | Simple word problems in universal algebras[END_REF], is to replace the associativity axiom by the rewrite rule

+ c) + d) + e)
that is provable without the associativity axiom. Yet, even if the rewrite system is confluent and terminating, normalizing propositions at all times is not sufficient to get rid of the associativity axiom. Indeed, the proposition

∃x (P (a + x) ⇒ P ((a + b) + c))
is provable using the associativity axiom, but its normal form, i.e. the proposition itself, is not provable without the associativity axiom. In particular, the propositions P (a + x) and P ((a + b) + c) are not unifiable, i.e. there is no substitution of the variable x that makes these two propositions identical. The explanation is that, in the proof of this proposition, we must first substitute the term b + c for the variable x and then rewrite the proposition P (a + (b + c)) ⇒ P ((a + b) + c) to P ((a + b) + c) ⇒ P ((a + b) + c) before we reach a proposition of the form A ⇒ A. To design a complete proof search method, the unification algorithm must be replaced by an algorithm that searches for a substitution that does not make the two propositions equal, but let them have the same normal form. Such an algorithm is called an equational unification algorithm modulo associativity. And Gordon Plotkin [START_REF] Plotkin | Building-in equational theories[END_REF] has proven that when unification is replaced by equational unification modulo associativity, the associativity axiom can be dropped without jeopardizing the completeness of the proof search method.

This proof search method is much more efficient than the method that searches for a cut free proof in predicate logic using the associativity axiom and the axioms of equality. In particular, the search for a cut free proof of the sequent ⊢ ⊥ with equational unification fails in finite time, unlike the search of a cut free proof of the sequent ⊢ ⊥, using the associativity axiom and the axioms of equality.

When formulated, not in a proof search setting, but in a purely proof theoretical one, Plotkin's idea boils down to that that two propositions such as P (a + (b + c)) and P ((a + b) + c) that have the same normal form, should be identified. We have called Deduction modulo [START_REF] Dowek | Theorem proving modulo[END_REF][START_REF] Dowek | Proof normalization modulo[END_REF] this idea to reason modulo a congruence on propositions-i.e. an equivalence relation that is compatible with all the symbols of the language. Then, the need to replace unification by equational unification is simply a consequence of the fact that when unifying two propositions P and Q, we must find a substitution σ such that σP and σQ are identical, modulo the congruence. The possibility to drop the associativity axiom is just a consequence of the fact that this axiom is equivalent, modulo associativity, to the proposition ∀x∀y∀z ((x + y) + z = (x + y) + z) that is a consequence of the axiom ∀x (x = x). Finally, the completeness of proof search modulo associativity is a consequence of the fact that, when terms are identified modulo associativity in predicate logic, cut elimination is preserved because cut elimination ignores the inner structure of atomic propositions. Thus, a cut in Deduction modulo is just a sequence formed with an introduction rules and an elimination rule, like in predicate logic, the only difference being that these rules are applied modulo a congruence.

This remark generalizes to all equational theories, i.e. to all the theories whose axioms have the form ∀ (t = u) and we get this way a cut elimination theorem for a class of theories that contains more than one theory and from this cut elimination theorem, we can rationally reconstruct the proof search methods for equational theories designed by Gordon Plotkin.

Deduction modulo

Deduction modulo is thus a tool that permits to associate a notion of cut to any equational theory.

But this notion of cut also subsumes that introduced with the fold and unfold rules. Indeed, if we start with a theory formed with the axioms ∀ (P 1 ⇔ A 1 ), ..., ∀ (P n ⇔ A n ), instead of replacing these axioms by theoretical deduction rules, we can replace them by rewrite rules P 1 -→ A 1 , ..., P n -→ A n that rewrite propositions directly-and not only terms that occur in propositions-and consider the congruence defined with these rules. We obtain this way a notion of cut that is equivalent to the notion of cut introduced with the fold and unfold rules: not all theories have the cut elimination property, but a theory has the cut elimination property in one case if and only if it has this property in the other. Although it is not difficult to prove, this result is not completely trivial because Deduction modulo allows some deep inferences-a rewrite rules can be used at any place in a proposition, while the fold and unfold rules allow shallow inferences only, i.e. rewriting at the root, and this is essential for the cut elimination to work with the fold and unfold rules.

By an abuse of language, when Deduction modulo a congruence has the cut elimination property, we sometimes say that the congruence itself has the cut elimination property.

Thus, Deduction modulo is framework where a theory is not defined as a set of axioms but as a set of rewrite rules and this framework unifies the notions of cut defined by Dag Prawitz and by Gordon Plotkin.

From axioms to algorithms

An important question about Deduction modulo is how strong the congruence can be. For instance, can we take a congruence such that A is congruent to ⊤ if A is a theorem of arithmetic, in which case each proof of each theorem is a proof of all theorems? This seems to be a bad idea, for at least two reasons. First, the decidability of proof checking requires that of the congruence. Then, for the cut free proofs to end with an introduction rule, the congruence must be non-confusing, i.e. when two non-atomic propositions are congruent, they must have the same head symbol and their sub-parts must be congruent. For instance, if both propositions are conjunctions, A ∧ B and A ′ ∧ B ′ , A must be congruent to A ′ and B to B ′ .

Both properties are fulfilled when the congruence is defined by a confluent and terminating rewrite system where the left hand side of each rule is either a term or an atomic proposition, such as P (0) -→ ∀x P (x). But, we sometimes consider cases where the congruence is defined by a rewrite system that is not terminating, for instance if it contains the rule x + y -→ y + x or the rule P -→ P ⇒ Q. Nevertheless, the congruence defined this way may still be decidable and non-confusing.

Cut elimination is a third property that may be required in the definition of the notion of theory.

As the rewrite rules define a decidable congruence, we may say that they define an algorithm. And indeed, we know that the rewrite rules that replace the axioms of the addition 0 + y -→ y S(x) + y -→ S(x + y) define an algorithm for addition. Thus, Deduction modulo is also a way to separate the deduction part from the computation part in proofs. This idea, formulated here in the general setting of predicate logic had already been investigated in some specific systems such as Intuitionistic type theory [START_REF] Martin-Löf | Intuitionistic type theory[END_REF] and the Calculus of constructions [START_REF] Coquand | The Calculus of constructions[END_REF], where a decidable definitional equality is distinguished from the usual propositional equality. Also, the idea of transforming theorems into rewrite rules has been used by Robert S. Boyer and J. Strother Moore in the theorem prover ACL [START_REF] Boyer | A theorem prover for a computational logic[END_REF].

But the novelty of Deduction modulo is that rewrite rules are used as a substitute for axioms and that provability with rewrite rules is proven to be equivalent to provability with axioms. Thus, the rewrite rules are used to express the theory, while the theory is not distinguished from the logic in Intuitionistic type theory, in the Calculus of constructions or in the Boyer-Moore logic.

Thus, it seems that Deduction modulo gives an original answer to the question "What is a theory ?" and this answer is "An algorithm".

This answer is part of a general trend, in the last decades, to answer "An algorithm" to various questions, such as "What is a grammar ?", "What is an economical agent ?", "What is a law of physics ?", "What is a proof ?", ... and this answer may be given to more questions in a near future, e.g. to the question "What is a cell ?"

It must be noticed, however, that the idea that a proof is an algorithm, the Brouwer-Heyting-Kolomogorov interpretation of proofs, may have somehow been an obstacle to our understanding that a theory also is an algorithm. The success of the algorithmic interpretation of proofs seems to have implicitly promoted the idea that this algorithmic interpretation of proofs was the link between the notion of algorithm and that of proof, making it more difficult to remark this other link.

But in the same way computer scientists know that a program expresses an algorithm and that the algorithm used to check that is program is correctly typed is another algorithm, it seems that proofs are algorithms and that their correctness criterion is parametrized by another algorithm: the theory.

Extended logics

This new answer to the question "What is a theory?" gives the possibility to define a general notion of cut for all the theories defined in this way and to prove general cut elimination results that apply to large classes of theories.

It gives the possibility to avoid two of the strategies mentioned above to side step the inability of proof theory of predicate logic to handle theories in a satisfactory way: introduce extended logics, such as second-order or higher-order logic, and focus on particular theories, such as arithmetic.

Second-order and higher-order logics have been studied thoughtfully in the second half of the XX th century. Higher-order logic has a special notion of model and a special completeness theorem [START_REF] Henkin | Completeness in the theory of types[END_REF], a special cut elimination theorem [START_REF] Girard | Une extension de l'interprétation de Gödel à l'analyse, et son application à l'élimination des coupures dans l'analyse et la théorie des types[END_REF], special proof search algorithms [START_REF] Andrews | Resolution in type theory[END_REF][START_REF] Huet | A mechanisation of type theory[END_REF], even a special notion of substitution and a special Skolem theorem [START_REF] Miller | A Compact representation of proofs[END_REF].

The history of the notion of higher-order substitution in itself could have lead to Deduction modulo. Before the modern view that substituting the term λx (Q(f (x))) for the variable P in the proposition (P 0) yields the proposition (λx (Q(f (x))) 0), that is provably equivalent to Q(f (0)), using some conversion axioms, this substitution yielded directly the proposition Q(f (0)). Thus, normalization was included in substitution operation.

Then, the substitution operation was simplified to an operation that is almost the substitution of predicate logic, and conversion axioms were introduced in the formulation of higher-order logic given by Alonzo Church [START_REF] Church | A formulation of the simple theory of types[END_REF]. Shortly after, the idea of incorporating these axioms in the unification algorithm was proposed by Peter Andrews [START_REF] Andrews | Resolution in type theory[END_REF] and this yielded higher-order unification [START_REF] Huet | A unification algorithm for typed λ-calculus[END_REF]. Although Andrews' idea seems to be independent from Plotkin's, higher-order unification is equational unification modulo beta-conversion.

Finally, in Deduction modulo, the conversion axioms are included in the congruence and unification is performed modulo this congruence.

The story is just slightly more complex because besides separating substitution from conversion, Church's formulation of higher-order logic introduces a symbol λ that binds a variable, thus the substitution operation in this logic must handle binders. In the same way, besides being equational, higher-order unification is also nominal [START_REF] Ch | Nominal unification[END_REF], i.e. it involves terms containing binders.

Yet, lambda bound variables can be eliminated from higher-order logic, for instance using combinators or de Bruijn indices and explicit substitutions and the last idiosyncrasy of higher-order logic, the absence of separation between terms and propositions can be avoided by introducing a "unary copula" ε transforming a term of type o into a propositions. This way, higher-order logic can be defined as a theory in Deduction modulo [START_REF] Dowek | HOL-lambda-sigma: an intentional firstorder expression of higher-order logic[END_REF], and in this case it is better to call it Simple type theory, to stress its theoretical nature. We avoid this way the need of a special notion of model, a special completeness theorem, a special cut elimination theorem [START_REF] Dowek | Proof normalization modulo[END_REF], special proof search algorithms [START_REF] Dowek | Theorem proving modulo[END_REF][START_REF] Dowek | Polarized resolution modulo[END_REF], a special notion of substitution and a special Skolem theorem [START_REF] Dowek | Skolemization in simple type theory: the logical and the theoretical points of view[END_REF]. Some formulations of second-order logic, such as the Functional second-order arithmetic of Jean-Louis Krivine and Michel Parigot [START_REF] Leivant | Reasoning about functional programs and complexity classes associated with type disciplines[END_REF][START_REF] Krivine | Programming with proofs[END_REF], even take more advantage of the notion of congruence when expressed as theories in Deduction modulo [START_REF] Dowek | Specifying programs with propositions and with congruences[END_REF].

All the theories expressed in Deduction modulo verify an extended subformula property, and so does higher-order logic. How is this compatible with the well-known failure of the sub-formula property for higher-order logic? First, we have to notice that, strictly speaking, the sub-formula property holds for propositional logic only. The notion of sub-formula has to be adjusted for the sub-formula property to hold for predicate logic: the set of subformulae of a proposition has to be defined as the smallest containing this proposition, that is closed by the sub-tree relation and also by substitution. This way, the proposition ∀x P (x) has an infinite number of sub-formulae as all the instances of the proposition P (x) are sub-formulae of the proposition ∀x P (x). In Deduction modulo, besides being closed by the sub-tree relation and substitution, this set must be closed by the congruence. Thus, if we have a rule P -→ Q ⇒ Q, the sub-formulae of the proposition P are P and Q. Using this definition, the set of sub-formulae of some propositions in higher-order logic contains all the propositions. This is what is usually called the failure of the sub-formula property for higher-order logic.

This ability of predicate logic to handle theories changes the organization of proof theory as a field of knowledge by giving back predicate logic a central place and reformulating in a wider setting the results specially developed for second-order and higher-order logic.

Particular theories

In the same way, the results developed for a particular theory, such as arithmetic are just consequences of general results, once these theories have been expressed as algorithms. And several theories have been expressed in this way, in particular arithmetic [START_REF] Dowek | Arithmetic as a theory modulo[END_REF][START_REF] Allali | Algorithmic equality in Heyting arithmetic modulo[END_REF] and some versions of set theory [START_REF] Dowek | Cut elimination for Zermelo's set theory[END_REF], although some other theories, such as geometry, have not been investigated yet.

The case of arithmetic is interesting as it shows how expressing a theory as an algorithm sheds a new light on this theory. There are two ways to express arithmetic in predicate logic, either, as Peano did, using a predicate N characterizing natural numbers, or not. That a natural number is either 0 or a successor is expressed in the first case by the proposition

∀x (N (x) ⇒ (x = 0 ∨ ∃y (N (y) ∧ x = S(y))))
and in the second by the proposition ∀x (x = 0 ∨ ∃y (x = S(y)))

This simpler formulation is usually preferred. Yet, the formulation of arithmetic in Deduction modulo does use the Peano predicate N . This formulation was originally considered as a first step, before we understood how to eliminate this predicate. Yet, it appears that this predicate cannot be eliminated. Indeed, the formulation of arithmetic without this predicate has a strange property: in the constructive case, it verifies the closed disjunction property but not the open one. That is, if a closed proposition of the form A ∨ B is provable, then either A or B is provable, but some open propositions of the form A∨B are provable, while neither A nor B is, e.g. x = 0∨∃y (x = S(y)). And any theory expressed in Deduction modulo that enjoys the cut elimination property verifies the full disjunction property. This means that not all sets of axioms can be transformed into a nonconfusing congruence that has the cut elimination property. And this is a strength, not a weakness, of Deduction modulo. Deduction modulo rules out some theories, e.g. contradictory theories, theories that do not verify the disjunction property in the constructive case, ... and the counterpart of this is that strong results can be proven about the theory that can be expressed in Deduction modulo, such as consistency or the disjunction property in the constructive case. The lack of strong results in the theory of theories when theories were defined as sets of axioms is a consequence of the fact that this notion of theory was too general, and not much can be said about a too large class of objects.

This remark raises an difficult but interesting question. What are the properties that a set of axioms must fulfill to be transformed into a nonconfusing congruence having the cut elimination property? A recent unpublished result of Guillaume Burel [5] suggests that, in the classical case, up to skolemization, consistency is a sufficient condition. In the constructive case, the problem is open. As all theories expressed by a non-confusing congruence that has the cut elimination property are consistent, and enjoy the disjunction and the witness property, these conditions are necessary for a theory to be expressed as a non confusing congruence that has the cut elimination property, and for instance, the axiom P ∨ Q and the axiom ∃x P (x) cannot. Whether these conditions are sufficient is open.

First chapter of a theory of theories

Deduction modulo has already lead to general cut elimination results [START_REF] Dowek | Proof normalization modulo[END_REF] that subsume cut elimination results for arithmetic and for higher-order logic. It also has lead to proof search algorithms that subsume both equational resolution and higher-order resolution [START_REF] Dowek | Theorem proving modulo[END_REF][START_REF] Dowek | Polarized resolution modulo[END_REF] and to the development of an extended notion of model, where two congruent propositions are interpreted by the same truth value, but not necessarily two provably equivalent propositions [START_REF] Dowek | Truth values algebras and proof normalization[END_REF]. It has also lead to a formulation of a lambda-calculus with dependent types called λΠ-modulo [START_REF] Cousineau | Embedding pure type systems in the lambda-Pi-calculus modulo[END_REF], that permits to express proofs in Deduction modulo as algorithms and that subsumes the Calculus of constructions and more generally all functional Pure type systems [START_REF] Barendregt | Lambda calculi with types[END_REF]. The important point with this calculus is that it completely de-correlates the issue of the functional interpretation of proofs from the problem of the choice of a theory. The functional interpretation of proofs is handled by the dependent types and the theory by the congruence. There is no special link between some typing disciplines-such as polymorphism-and some theories-such as the second-order comprehension scheme.

But, the most interesting about Deduction modulo is that it permits to formulate problems that could not be formulated when theories were defined as sets of axioms. In particular, we may seek for a characterization of the theories that have the cut elimination property or of those that have the proof normalization property. Olivier Hermant has given examples showing that cut elimination does not imply normalization [START_REF] Hermant | Méthodes sémantiques en Déduction modulo[END_REF]. Then, Denis Cousineau [START_REF] Cousineau | A completeness theorem for strong normalization in minimal Deduction modulo[END_REF] has given the first condition both sufficient and necessary for normalization. The fact that this condition is model theoretic suggests that the notion of normalization is also a model-theoretic notion.

This problem and the problem of the characterization of the theories that can be expressed in Deduction modulo are two among the main open problems in this area. Defining a nominal Deduction modulo, i.e. including function symbols that may bind variables is also an important one.

If we look at this theory of theories from outside, we see that some aspects that were minor in the proof theory of predicate logic become majors aspects: the link between the notion of cut and that of model, the link between proof theory and automated theorem proving, and also many-sorted predicate logic, as unlike axioms, rewrite rules are difficult to relativize, ... On the other hand, some topics that have been central in proof theory in the last decades become less central: the case of higher-order logic and the functional interpretation of proofs. These notions are not given up, but, like the notion of triangle in geometry, they just lose their central place by being included in a larger picture.

x

  + (y + z) -→ (x + y) + z that allows to transform the proposition P ((a + b) + ((c + d) + e)) into P ((((a + b) + c) + d) + e) but not vice-versa. If the rewrite rules form a terminating and confluent system, then two terms are provably equal if and only if they have the same normal form. Normalizing the proposition above yields the provably equivalent proposition P ((((a + b) + c) + d) + e) ⇒ P ((((a + b)