Nicola Capuano
email: capuano@crmpa.unisa.it

Matteo Gaeta
email: gaeta@crmpa.unisa.it

Laura Pappacena Crmpa

An e-Learning Platform for SME Manager Upgrade and its Evolution Toward a Distributed Training Environment

Keywords: e-Learning, Web Services, Distributed Environments

The purpose of this paper is to describe the work in progress related to the customisation, the trial and the evaluation of an innovative e-learning platform for manager upgrade in Small and Medium Enterprises (SME) in the framework of an EC funded project named InTraServ and its forthcoming re-engineering process aimed to the adoption of distributed services in the framework of another EC funded project named Diogene. The present e-learning solution includes several state-of-the-art technologies and methodologies such as: metadata and ontologies for knowledge manipulation, fuzzy learner modelling, intelligent course tailoring, case based reasoning, business games and simulation tools. The proposed solution is based on the distribution of working tasks among content provider services, content discovery services, content brokering services, training services, curriculum vitae searching services and collaboration services.

INTRODUCTION

The managerial capacity paradigm argues that a firm's growth is limited by the speed at which it can expand its managerial capacity. This is generally true but it is more and more true for Small and Medium Enterprises (SME) that often don't have a well defined managerial structure causing, in many cases, strategic and decisional lacks that obstruct enterprise's growth.

The learning task for managers is then a critical element for the survival and the success of SME in the global competitive scenery. As quoted in [START_REF]Trials and Best Practice Addressing Advanced Solutions for On-the-Job Training in SMEs[END_REF] the key challenges to be addressed to satisfy SME training needs concern: distance, time and location (training must serve a dispersed group of learners where and when they require it), flexibility (training can be undertaken between work tasks), availability (training material can be easily located), immediacy (user can obtain quickly solutions to daily working problems).

Starting from these considerations, the EC funded project InTraServ [START_REF]InTraServ: Intelligent Training Service for Management Training in SMEs" FP5 IST Project[END_REF] arranged a completely innovative e-learning platform purposed to face and solve these and more issues. The InTraServ project is now approaching the experimentation phase in several SMEs from Italy, UK and Spain.

At the same time, a further EC funded project named Diogene [START_REF]Diogene: a Training Web Broker for ICT Professionals[END_REF] is in progress. Its purpose is to completely re-engineering the architecture of the InTraServ e-learning platform by applying a distributed computing paradigm based on Web Services. This will allow the distribution of training content on different servers, the integration with the forthcoming Semantic Web, the cooperation of different installations of the system, the possibility to create a training offer by combining resources offered by different providers, etc. In this sense it will be a step toward a GRID architecture.

The paper is organised as follows: the InTraServ project will be briefly described and its main features introduced (section 2). A sketch of the present system architecture will be then presented (section 3) and the new service oriented architecture we have in mind will be introduced (section 4). Some conclusions (section 5) and references will follow.

WHAT'S INTRASERV

InTraServ [START_REF]InTraServ: Intelligent Training Service for Management Training in SMEs" FP5 IST Project[END_REF] is an EC "Trial" project funded under the 5th Framework Programme whose purpose is to customise, try and evaluate an innovative Web-based intelligent e-learning solution for manager upgrade in real SME environments operating in different fields.

Using the InTraServ solution, it will be possible for a manager to take personalised training between working tasks (on-the-job), to evaluate the formal knowledge acquired and to transform it in practical knowledge by experimenting what learnt in simulated situations. When, finally, the manager will master such knowledge, he can apply it inside the organisation. Moreover, using InTraServ, a manager can be supported during his decision making process (just-in-time) by exploiting the CBR-based real case solver component.

The InTraServ e-learning platform is now ready and accessible through the InTraServ portal [START_REF]InTraServ: Intelligent Training Service for Management Training in SMEs" FP5 IST Project[END_REF]. It includes four courses (Business Decision, Marketing Management, Marketing Research and Management Control) in three languages (Italian, English and Spanish) and several Business Games (BGs). The following paragraphs describes briefly its innovative features with respect to commercial e-learning platforms presently available on the scene.

Metadata and Ontologies for Knowledge Management

All InTraServ learning material is organised in learning objects (LO) indexed through IMS compliant metadata [START_REF][END_REF] in order to let the system know what each one of them is about and how it can be used during the learning process.

To provide, also, information about LO relations and interdependency, InTraServ applies ontologies [START_REF] Fensel | Ontologies: a Silver Bullet for Knowledge Management and Electronic Commerce[END_REF] allowing to design abstract, simplified views of training domains. Within InTraServ, ontologies are used to define and relate concepts of a training domain with four kinds of relations: (is_part_of, requires, suggested order and explains) and, also, to link concepts to LOs [START_REF] Capuano | Personalised Intelligent Training on the Web: A Multi Agent Approach[END_REF], [START_REF] Capuano | ABITS: An Agent Based Intelligent Tutoring System for Distance Learning[END_REF].

Fuzzy Learner Modelling

InTraServ infers and maintains a learner model compliant with the IMS-LIP standard [START_REF][END_REF] composed by a cognitive state and a set learning preferences. The cognitive state stores, for each concept of a specified training domain, the knowledge degree reached by the learner represented as a set of fuzzy numbers [START_REF] Dubois | Fuzzy Sets and Systems -Theory and Applications[END_REF] (allowing, in this way, to manage uncertainty in the evaluation process).

Learning preferences, instead, include all information about learner cognitive abilities and perceptive capabilities i.e. to which typology of resources a specified learner is more receptive [START_REF] Capuano | Personalised Intelligent Training on the Web: A Multi Agent Approach[END_REF], [START_REF] Capuano | ABITS: An Agent Based Intelligent Tutoring System for Distance Learning[END_REF].

Intelligent Course Tailoring

An InTraServ course is composed by an user selected set of learning goals (key concepts that the learner has to learn) and by a learning path (a sequence of learning objects that has to be used to provide, to a specific learner, all necessary knowledge to fully understand chosen goals).

Different learners can require different paths to learn the same goals depending on their learner models. For this reason, InTraServ provides an automatic curriculum generation procedure: the learner can choose what to learn (goals) and let the system organise a personalised learning path for him. Such path can change dynamically during the learning process adapting to learner needs in relation to learner performed activities [START_REF] Capuano | Personalised Intelligent Training on the Web: A Multi Agent Approach[END_REF], [START_REF] Capuano | ABITS: An Agent Based Intelligent Tutoring System for Distance Learning[END_REF].

Case Based Reasoning

2nd International LeGE-WG Workshop on e-Learning and Grid Technologies : a fundamental challenge for Europe InTraServ gives learners the possibility to solve daily working problems by exploiting a CBR methodology [START_REF] Kolodner | Case-Based Reasoning[END_REF] i.e. through a sub-system able to solve new cases comparing the current problem with similar solved problems in a case base and ranking found solutions. Moreover, the system is able to extend its knowledge by interpreting a new solution in light of similar situations and abstracting out generalisations from experiences. The strength of this approach to problem solving is that the knowledge base is maintained as concrete problem descriptions. In this way the system maintenance could be made by a domain expert rather that by a system expert.

Business Games and Simulation Tools

An important InTraServ feature is the possibility to use a set of advanced simulation tools addressing the business decision process through a "what…if" approach. They refer to a particular learning process phase called "interactive phase": after a learner studied the theory related to a specific topic, he can use such tools to exercise about learned topics.

But a simulation exercise is quite different from a classical exercise: it is based on simulation models that allow concrete experience built up by experimentation and by modification of hypotheses that play a role inside the system under examination [START_REF] Albano | e-Learning e Apprendimento Manageriale[END_REF].

INTRASERV ARCHITECTURE: THE PRESENT

The main idea behind the InTraServ architecture is that any e-learning application should be supported by a general infrastructure that will put a set of common resources at everyone's disposal and, according to the specific needs of each training domain and application, by a set of further specific resources.

For this reason, the InTraServ architecture, despite that it was customised for the management training domain, is fully adaptable and extensible and can be the basis for the realisation of a virtually infinite set of specific e-learning platforms suitable for any needs, context and domain.

Moreover, the present architecture (see sketch in figure 1), thanks to a strong separation of tasks between different components, will be an optimum starting point to realise a distributed architecture as we will see in the next section. The Data layer stores all persistent information related to used data structures: Learning Objects, Metadata, Ontologies and Learner Models (see section 2).

The Infrastructure layer, instead, contains all general-purpose e-learning services as described below.

User Management Services: allow registration and logging and provide all user and groups management functions including profiles handling;

Learning Objects Management Services: provide all functions to manage LOs, Metadata and related Ontologies (including access rights handling) and to index and retrieve LOs basing on associated Metadata end Ontologies.

Collaboration Services: include synchronous (text and visual chat) and asynchronous (messaging system and threaded discussion forum) tools for collaboration between users.

The Extension layer, moreover, allows to add at any time new specific domain or context dependent services through the implementation of plug-ins compliant to system specifications. Three plug-ins have been included in the InTraServ Extension layer:

• the Case Based Reasoning (CBR) plug-in that is responsible for case bases reasoning functions (see 2.4); • the Agent Based Intelligent Tutoring System (ABITS) plug-in that is responsible for "intelligent" training functions (see 2.1, 2.2, 2.3 and [START_REF] Capuano | ABITS: An Agent Based Intelligent Tutoring System for Distance Learning[END_REF]); • the Business Games (BG) plug-in that allows to exploit business games as a particular type of LO (see 2.5).

Finally, the Self-Paced Training System layer includes the front-end related to an instance of the e-learning system (geared toward manager upgrading in SME in the case of the InTraServ project) and allows a filtered access to resources and services provided by the layers below. This layer is obtained via the customisation of a general Web Portal: a dynamic container of panels that give access to underlying services and resources.

The InTraServ e-learning platform has been entirely realised in the Microsoft .NET environment [START_REF] Macdonald | Microsoft .NET Distributed Applications: Integrating Web Services and Remoting[END_REF], using the ASP.NET language (for the front-end) and the C# language (for the back-end).

Main functions have been wrapped in Web Services in order to allow a standard invocation on the Web from external applications.

DIOGENE ARCHITECTURE: THE FUTURE

The InTraServ architecture is well structured and suitable for extensions with new services and easily customisable for new training contexts and domains. Nevertheless, it is quite monolithic: it doesn't allow the distribution of training content on different servers, the cooperation of different installations of the system, the possibility to combine training resources offered by different providers, etc.

For this and more reasons, in the framework of further project named Diogene, we completely re-thought the InTraServ architecture in order to allow the distribution of training resources based on Web Services.

Diogene [START_REF]Diogene: a Training Web Broker for ICT Professionals[END_REF] is an EC funded project aimed to design, implement and evaluate with real users an e-learning Web brokering environment for ICT individual training able to support learners during the whole cycle of the training, from the definition of objectives to the assessment of results through the construction of custom courses.

The e-learning system that will be realised under Diogene will use some InTraServ state-of-theart technologies like metadata and ontologies for knowledge manipulation, fuzzy learner modelling, intelligent course tailoring but, also, will include a set of innovative features like dynamic learning strategies, Semantic Web openness, Web services for Learning Object handling and IPR management, Curriculum Vitae generation, maintenance and searching facilities, free-lance teachers support and assisted Learning Objectives definition.

The architecture we have in mind for Diogene is sketched in figure 2. As it can be seen, it derives, partially from the InTraServ architecture in the distribution of tasks among component/services. -Content Provider Services. They are installed in content provider organisations and are used to host training content and provide a standard SOAP-based interface [START_REF] Macdonald | Microsoft .NET Distributed Applications: Integrating Web Services and Remoting[END_REF] to allow remote access to it. They provide search and retrieval functions on the local repository via metadatabased queries and are able to perform e-commerce transactions between users requesting content and the provider organisation itself to buy the access to content for limited periods of time. They are an extended version of the InTraServ Learning Objects Management Services.

-Content Discovery Services. They are able to extract training content directly from the Web of the present and of the future generation (Semantic Web). Through a keyword-based text categorisation algorithm they are able, where absent, to automatically extract metadata from textual learning objects and to link them to ontology concepts. Through a mixed approach based on keyword and ontologies, moreover, they are able to bypass compatibility problems between different ontological representations of the same domain. -CV Searching Services. They provide search engine capabilities on Learner Models Databases of registered Training Services in order to let third parties interested to hire certified staff to find qualified professional (with respect to privacy requirements). They will maintain, moreover, statistics of received requests in order to rank required competencies.

-Collaboration Services. They will support social interactions, mentoring and information exchange by providing users a set of collaborative synchronous and asynchronous facilities. It's obvious that the distributed architecture designed for Diogene presents several advantages with respect to the InTraServ centralised one.

The maintenance of Learning Objects on content provider servers allows content provider organizations to manage and organize content locally and, in the same time, to overcome property right related problems.

-The networking of different content provider servers filtered through content brokers allows to compose training offer aggregating content from different providers in order to best match user needs.

-The Web is full of training content and the forthcoming Semantic Web paradigm will make it semantically understandable by machines. Content Discovery Services exploit such power to find useful and freeware learning material and to make it available to the DTE.

-The collaboration between peers is of a paramount importance to improve the training experience. Collaboration Services are able to find on the whole DTE (rather then on a single installation of the training service) learners with similar interests and to put them in contact within a co-operative environment.

-Learner models contains useful data about the know-how of students and their acquired competencies: CV Searching Services are able to find qualified professionals all over the DTE and to put them in contact with hiring companies.

CONCLUSIONS

In this paper we described the e-learning platform realised under the framework of an EC funded project named InTraServ, its innovative features, its architecture and the evolution of such architecture toward a distributed services paradigm (more suitable for a GRID environment) in the context of another EC funded project named Diogene. After the end of Diogene, the next step will be to made the DTE GRID available.

FIGURE 1 .

 1 FIGURE 1. The InTraServ Architecture.

FIGURE 2 .

 2 FIGURE 2. The Diogene Architecture.

-

  Content Brokering Services. They are broker of training content. They maintain indexes of learning objects of registered Content Provider and Discovery Services and allow users to use metadata-and ontology-based queries to find the right provider with the right content. They include, also, some course tailoring capabilities (see 2.3) to generate ad-hoc courses by assembling content from registered Content Provider and Discovery Services. -Training Services. They are responsible for the delivery of courses and for the provision of course management and execution functions. They deal, moreover, with "intelligent" training functions like learner modelling, course tailoring, assisted objective definition and learning strategies upgrading. They don't maintain any local training content but strictly interact with Content Brokering Services or directly with Content Discovery and Provider Services to obtain and combine learning objects. They include and extend the InTraServ Self Paced Training System plus the User management Services and the ABITS plug-in.

  They will be able to automatically arrange groups among users of registered Training Services by individuating and grouping learners with similar needs and/or profiles. They are an extension of InTraServ Collaboration Services. The following figure depicts possible interactions between multiple instances of Diogene services hosted by different organisations. They will constitute the Distributed Training Environment (DTE) of Diogene.

FIGURE 3 .

 3 FIGURE 3. Interactions Among Diogene Services.

7 The

 7 An e-Learning Platform for SME Manager Upgrade and its Evolution Toward a Distributed Training Environment 2nd International LeGE-WG Workshop on e-Learning and Grid Technologies : a fundamental challenge for Europe InTraServ project started in December 2001 and will end in May 2003. The experimentation phase with about 20 managers of Italian, English and Spanish SME is now in course. Apart the InTraServ project, CRMPA decided to experiment the realised e-learning platform also in several Italian academic contexts (like the University of Salerno, of Roma3 and of Molise) in four different courses about computer science and mathematics as a support for teachers in their usual didactic activities. Such kind of experimentation will start in March 2003. The Diogene project, instead, started in April 2002 and will end in March 2004. The architecture design phase of Diogene is running toward its end and the implementation phase is recently started. A first prototype of the Diogene e-learning platform will be available in September 2003.

2nd International LeGE-WG Workshop on e-Learning and Grid Technologies : a fundamental challenge for Europe


Jasmin Christian Blanchette

Nicolas Peltier

Simon Robillard
email: simon.robillard@chalmers.se

Superposition with Datatypes and Codatatypes

come

Introduction

The ability to reason about inductive and coinductive datatypes has many applications in program verification, formalization of the metatheory of programming languages, and even formalization of mathematics. Inductive datatypes, or simply datatypes, consist of finite values freely generated from constructors. Coinductive datatypes, or codatatypes, additionally support infinite values. Non-freely generated (co)datatypes are also useful. All of these variants can be seen as members of a single unifying framework (Section 2).

It is well known that the first-order theory of datatypes cannot be finitely axiomatized. Distinctness, injectivity, and exhaustiveness of constructors are easy to axiomatize, but acyclicity is more subtle, and for induction we would need an axiom schema or a second-order axiom. Codatatypes are also problematic: Besides a coinduction principle that is dual to induction, they are characterized by the existence of all possible infinite values, corresponding intuitively to infinite ground terms. Both datatypes and codatatypes represent a challenge for automatic theorem provers.

Superposition [START_REF] Bachmair | Rewrite-based equational theorem proving with selection and simplification[END_REF] is a highly successful calculus for reasoning about first-order clauses and equality. There has been some work on extending superposition with induction [START_REF] Cruanes | Superposition with structural induction[END_REF][START_REF] Wand | Superposition: Types and Polymorphism[END_REF], including by Kersani and Peltier [START_REF] Kersani | Combining superposition and induction: A practical realization[END_REF], and on the axiomatization of datatypes, including by Kovács, Robillard, and Voronkov [START_REF] Kovács | Coming to terms with quantified reasoning[END_REF]. In this paper, we propose both axiomatizations and extensions of the superposition calculus to support freely and non-freely generated datatypes as well as codatatypes.

We first focus on a conservative extension of the theory with a finite number of firstorder axioms that capture the basic properties of constructors, acyclicity of datatype values, uniqueness of cyclic (ω-regular) codatatype values, and existence of all codatatype cyclic values (Section 3). These axioms admit nonstandard models; for example, for the Peano-style natural numbers freely generated by zero : nat and suc : nat → nat, we cannot exclude the familiar nonstandard models of arithmetic, in which arbitrarily many copies of Z may appear besides N. Similarly, the domains interpreting codatatypes are not guaranteed to contain all infinite acyclic values.

The axiomatization of codatatypes up to a suitable notion of nonstandard models constitutes the first theoretical contribution of this paper. Our second theoretical contribution is an extension of superposition with inference rules to reason about datatypes and codatatypes (Section 4). This is inspired by an acyclicity rule that Robillard presented at the Vampire 2017 workshop [START_REF] Robillard | An inference rule for the acyclicity property of term algebras[END_REF]. The main distinguishing feature of our rules is that they are (in combination with a few axioms) refutationally complete and their side conditions have some new order restrictions, helping prune the search space. On the other hand, our approach also requires a relaxation of the side conditions of the superposition rule: For clauses of the form c( s) ≈ t ∨ C, where c is a constructor and the first literal is maximal, inferences onto t must be performed, as in ordered paramodulation [START_REF] Bachmair | Orderings for equational proofs[END_REF]. In addition, we propose calculus extensions to reason about codatatypes.

Both the theory extension and the calculus extension are designed to be refutationally complete with respect to nonstandard models of datatypes and nonbranching codatatypes-codatatypes whose constructors have at most one corecursive argument (Section 5). Due to space restrictions, we can only briefly sketch the proof in this paper. We refer to our technical report [START_REF] Blanchette | Superposition with datatypes and codatatypes[END_REF] for detailed justifications and further explanations.

The calculus extension can be integrated into the given clause algorithm that forms the core of a prover's saturation loop (Section 6). The inference partners for the acyclicity and uniqueness rules can be located efficiently. We implemented both the axiomatic and the calculus approaches in the first-order prover Vampire [START_REF] Kovács | First-order theorem proving and Vampire[END_REF] and compare them empirically on Isabelle/HOL [START_REF] Nipkow | Isabelle/HOL: A Proof Assistant for Higher-Order Logic[END_REF] benchmarks and on crafted benchmarks (Section 7).

Syntax and Semantics

Our setting is a many-sorted first-order logic. We let τ, υ range over simple types (sorts), s, t, u, v range over terms, a, b, c, . . . range over function symbols, x, y, z range over variables, and C, D, E range over clauses. Literals are atoms of the form s ≈ t or ¬ s ≈ t, also written s ≈ t. Clauses are finite disjunctions of literals, viewed as multisets. Substitutions are written in postfix notation, with sσθ = (sσ)θ. The notation x represents a tuple (x 1 , . . . , x m ), and [m, n] denotes the set {m, m + 1, . . . , n}, where m ≤ n + 1.

A position p of type τ in t is a position in t such that t| p is of type τ. If s, t are terms and P is a set of positions of the same type as s in t, then t[s] P denotes the term obtained from t by replacing the subterms occurring at a position in P by s: t [1,n] , with P i = {q | i.q ∈ P} otherwise. Given two positions p and q, we write p < q if p is a proper prefix of q. Let Ctr be a distinguished set of function symbols, called constructors. We reserve the letters c, d, e for constructors. A constructor position in t is a position q in t such that for every p < q, the head symbol of t| p is a constructor. Definition 1. The set of constructor contexts of profile τ → υ is defined inductively as follows: (1) if t is a term of type υ, then t is a constructor context of profile τ → υ;

[s] P := s if ε ∈ P; t[s] P := t if P = ∅; and f(t 1 , . . . , t n )[s] P := f(t i [s] P i ) i∈
(2) if Γ 1 , . . . , Γ n are constructor contexts of profile τ → τ i and c :

τ 1 × • • • × τ n → υ is a constructor, then c(Γ 1 , . . . , Γ n ) is a constructor context of profile τ → υ; (3) the hole • is a constructor context of profile υ → υ.
Every constructor context can be written as Γ[•] P , where P is a set of constructor positions of the same type in Γ, denoting the positions of • in Γ. It is empty if ε ∈ P, and constant if P = ∅. We write Γ[•] p as an abbreviation for Γ[•] {p} , and we write Γ[t] P to denote the term obtained by replacing every position of P by the term t in the context Γ[•] P . Moreover, we write τ υ ("υ depends on τ") if there exists a constructor of profile

τ 1 × • • • × τ n → υ, with τ = τ i for some i ∈ [1, n], and τ ∼ υ if τ * υ and υ * τ.
The axioms and rules in this paper are parameterized by the following sets. Let T ind and T coind be disjoint sets of types, intended to model datatypes and codatatypes, respectively, and assume that the codomain of every constructor is in T ind ∪ T coind . Let Ctr inj ⊆ Ctr be a set of constructors, denoting injective constructors. Let be a binary symmetric and irreflexive relation among constructors; c d indicates that terms with head symbol c are always distinct from terms with head symbol d.

We introduce some properties of interpretations that are intended to capture some of the properties of (co)datatypes. An interpretation I satisfies

• Exh (exhaustiveness) iff, for every type τ ∈ T ind ∪ T coind , I |= m i=1 ∃ xi . x ≈ c i ( xi )
, where x is a variable of type τ, {c 1 , . . . , c m } is the set of constructors of codomain τ, and xi is a vector of pairwise distinct variables of the appropriate length and types;

• Inf (infiniteness) iff, for every type τ ∈ T ind ∪ T coind , the domain of τ is infinite; • Acy (acyclicity, for datatypes) iff, for every type τ ∈ T ind , for every nonempty constructor context Γ[•] p of type τ, where p is a position of type τ in Γ, we have x i ≈ y i . Most datatypes occurring in practice are recursive, so condition Inf is usually satisfied. In particular, it is the case for any freely generated (co)datatype τ with more than one constructor and such that τ + τ. Conditions Dst and Inj are defined by finite sets of axioms, but not conditions Acy and FP. In Section 3, we introduce conservative extensions of the considered formula so that conditions Acy and FP are satisfied. Then in Section 4, we replace some of these axioms by inference rules.

I |= Γ[x] p ≈ x,
We assume that τ ∼ υ whenever τ ∈ T ind and υ ∈ T coind . Intuitively, this condition means that a datatype cannot be defined by mutual recursion with a codatatype, which is a very natural restriction [START_REF] Blanchette | Truly modular (co)datatypes for Isabelle/HOL[END_REF]. If this condition does not hold, it is easy to see that there is no interpretation that satisfies both Acy and FP. On the other hand, we may have τ + υ or υ + τ with τ ∈ T ind and υ ∈ T coind . There may also exist types not belonging to T ind ∪ T coind , and the types in T ind ∪ T coind may depend on them. Finally, we assume that for each type τ, there exists a ground term t of type τ.

The axioms Exhaust for exhaustiveness, Dist for distinctness, and Inj for injectivity correspond to the formulas used to express the properties Exh, Dst, and Inj in Section 2. The other axioms are introduced below.

For all types τ ∼ υ, we introduce a predicate symbol sub τ υ on τ × υ together with the following axioms, where τ ∼ υ ∼ υ and c :

• • • × υ × • • • → υ is a constructor: Sub 1 : sub τ τ (x, x) Sub 2 : ¬ sub τ υ (x, y) ∨ sub τ υ (x, c(z, y, z )) NSub: ¬ sub υ τ (c(z, x, z ), x) if τ ∈ T ind Let Sub = Sub 1 ∧ Sub 2 .
The least fixpoint model of Sub is the usual subterm relation for constructor terms. The axiom NSub states that no term of a type in T ind may occur at a nonempty constructor position in itself.

Definition 2. An interpretation I is sub-minimal if it satisfies the equivalence sub(x, y) ⇐ ⇒ {∃z. y ≈ Γ[x] p | Γ[•]
p is a constructor context}, where z denotes the vector of variables in Γ that are distinct from x, y.

For every pair of types τ, υ ∈ T coind with τ ∼ υ, we introduce a type τ υ to denote contexts Γ[•] P of profile υ → τ. Let hole υ be a constant of type υ υ , denoting an empty context. All constructors c : We consider the following axioms, where υ ∈ T coind and x, y, x i , z i are pairwise distinct variables of the appropriate types: Comon and Lescanne [START_REF] Comon | Equational problems and disunification[END_REF] provide a decision procedure for equational formulas over finite and infinite trees, which correspond respectively to freely generated datatypes and codatatypes. It is based on a collection of equivalence-preserving transformation rules for eliminating quantifiers and normalizing the formulas. The set of formulas T = {Dist, Inj, Exhaust, Sub, NSub, App, Uniq, Cycl, Hole} forms the axiomatization of a conservative extension of the theory of (co)datatypes. We can thus derive a decision procedure for testing satisfiability of first-order sentences S containing only constructors symbols and the equality predicate in the above theory. By interleaving the steps of two fair saturation procedures of the superposition calculus, the first over S ∪ T and the second over ¬ S ∪ T , one of the two attempts is guaranteed to derive a refutation in finite time.

τ 1 × • • • × τ n → τ and types υ such that ∃i υ * τ i are asso- ciated with new n-ary constructors c υ : υ 1 × • • • × υ n → τ υ , where for every i ∈ [1, n], υ i = τ i υ if υ * τ i and υ i = τ i otherwise. Let app τ υ : τ υ × υ → τ, cyc υ : υ υ → υ,
App 1 : app τ υ (cst τ υ (x), y) ≈ x App 2 : app υ υ (hole υ , y) ≈ y App 3 : app τ υ ( c υ (x 1 , . . . , x n ), y) ≈ c(t 1 , . . . , t n ) if c : τ 1 × • • • × τ n → τ is a constructor and ∃i υ * τ i with t i = app τ i υ (x i , y) if υ * τ i and t i = x i otherwise Uniq: x ≈ hole υ ∨ y ≈ app υ υ (x, y) ∨ z ≈ app υ υ (x, z) ∨ y ≈ z Cycl: cyc υ (x) ≈ app υ υ (x, cyc υ (x)) Hole 1 : hole υ ≈ cst υ υ (x) Hole 2 : hole υ ≈ c υ (x 1 , . . . , x n ) if c : • • • → υ Let App = App 1 ∧ App 2 ∧ App 3 and Hole = Hole 1 ∧ Hole 2 . Example 3. Let c : τ 0 × υ → τ be a constructor, with υ * τ 0 . Then the profile of c υ is τ 0 υ × υ υ → τ υ . The term t := c υ (cst τ 0 υ (x), hole υ ) encodes the constructor context c(x, •). If a : υ, then app τ υ (t, a) = App c(x, a), where = App denotes equality modulo App (i.e., s = App t ⇐ ⇒ App |= s ≈ t).

Inference Rules

As an alternative to the above axiomatization, we propose an extension of the superposition calculus [START_REF] Bachmair | Rewrite-based equational theorem proving with selection and simplification[END_REF] with dedicated rules. Unless otherwise noted, the usual conventions of superposition apply. The standard notion of redundancy is used, with respect to the theory of equality. The notation s ≈ t indicates that the literal is maximal in its clause, after the substitution σ has been applied, and nothing is selected, or it is selected, whereas s ≈ t indicates that the literal is strictly maximal in its clause, after σ, and not selected. We let [¬] s ≈ t stand for either s ≈ t or s ≈ t.

Superposition. We denote by SP the usual rules of the superposition calculus with a slight relaxation: Superposition inside the nonmaximal term of an equation is allowed if the head of the maximal term is a constructor. This ensures that in the rewrite system built from saturated clause sets for defining a model, the right-hand side of every rule is irreducible if the head of the left-hand side is a constructor. Thus, our superposition rule is as follows:

u ≈ v ∨ D [¬] s[u ] ≈ t ∨ C Sup σ([¬] s[v] ≈ t ∨ D ∨ C) where σ = mgu {u ? = u }, u is not a variable, and σ(u) σ(v); moreover, σ(s[u ]) σ(t) if [¬] is ¬ or if the
head symbol of t is not a constructor. The equality resolution and equality factoring rules are the standard ones.

Infiniteness. The next rule captures infiniteness of (co)datatypes: Remark 9. If t is not a variable, the premise of Dist 1 is redundant after the rule is applied. Unifying t with c( x) can be useful when t is a variable. For example, from the clause c(x) ≈ x, we can derive by unifying x with d(ȳ), where d c.

n i=1 x ≈ t i ∨ C Inf C if x is a variable of a type τ ∈ T ind ∪ T coind and does not occur in C or t 1 , . . . , t n .
d( t ) ≈ u ∨ D c( s) ≈ u ∨ C Dist 2 (C ∨ D)σ if c d, σ = mgu {u ? = u }, c( s)σ
Injectivity. The injectivity property of constructors is also captured by two rules:

c(s 1 , . . . , s m ) ≈ t ∨ C Inj 1 (s i ≈ x i ∨ C)σ if i ∈ [1, m], c ∈ Ctr inj , σ = mgu {t ? = c(x 1 , . . . , x m )},
and x 1 , . . . , x m are fresh; and Acyclicity. The acyclicity rule attempts to detect constraints that would force a datatype value to be cyclic. The simplest example is a clause of the form Γ[s] ≈ s, where Γ is a nonempty constructor context. More generally, the clauses

c(s 1 , . . . , s m ) ≈ u ∨ D c(t 1 , . . . , t m ) ≈ u ∨ C Inj 2 (s i ≈ t i ∨ C ∨ D)σ if i ∈ [1, m], c ∈ Ctr inj , σ = mgu {u ? = u }, uσ c( s)σ,
s 1 ≈ Γ 1 [s 2 ] s 2 ≈ Γ 2 [s 3 ] • • • s n-1 ≈ Γ n-1 [s n ] s n ≈ Γ n [s 1 ] entail a constraint s 1 ≈ Γ 1 [Γ 2 [• • • [Γ n-1 [Γ n [s 1 ]]] • • • ]].
Moreover, the rule must support variables and nonunit clauses, and it should be finitely branching if we want to incorporate it in saturation-based provers-i.e., the set of clauses derivable from a given finite set of premises by a single rule should be finite. Finally, clauses of the form Γ[x] ≈ s ∨ C, where x occurs in C, are problematic, because there are infinitely many instantiations of x that can result in a cyclic constraint: s, c(s), c(c(s)), etc. To cope with all these subtleties, we first need to develop a considerable theoretical apparatus.

Definition 12. A chain built on a nonempty sequence of clauses (C 1 . . . , C n ) under condition D is a sequence (t 1 , . . . , t n+1 ) of terms satisfying the following conditions:

1. for every i ∈ [1, n], C i is of the form s i ≈ Γ i [s i+1 ] p i ∨ C i
, where p i is a nonempty constructor position in Γ i ; 2. there exists a substitution σ such that either σ is an mgu of E = {s i

? = s i | i ∈ [2, n]} or σ is an mgu of {s n+1 ? = s 1 } ∪ E; 3. t i = s i σ for i ∈ [1, n] and t n+1 = s n+1 σ; 4. D = n i=1 C i σ; 5. type(t 1 ) ∼ • • • ∼ type(t n+1 ); 6. (Γ i [s i+1 ] p i ≈ s i )σ is maximal in C i σ, and no negative literal is selected in C i σ; 7. s i σ Γ i [s i+1 ] p 1 σ, for i ∈ [1, n]; 8. for every i ∈ [2, n], s i is not a variable. The expression Γ 1 [• • • [Γ n [•] p n ] • • • ] p 1 σ is the chain's constructor context, σ is its mgu, and p 1 . • • • .p n is its constructor position. If t 1 = t n+1 , the sequence is called a cycle.
A chain is direct if t i = t j for all i, j ∈ [1, n + 1] with i = j and {i, j} = {1, n + 1}, and variable-ended if s n+1 is a variable. Remark 13. Conditions 5 to 8 are optional. They help prune the search space. Definition 14. A chain (t 1 , . . . , t n+1 ) built on a clause sequence (C 1 , . . . , C n ) is an extension of an acyclic chain (s 1 , . . . , s m+1 ) if n ≥ m, the latter chain is built on (C 1 , . . . , C m ), and the same literals and positions are considered in each clause C i in both chains.

Since chains can be arbitrarily long, we need to impose some additional conditions to prune them and ensure that the rules are finitely branching. Let Keep be a property of chains that fulfills the following requirements:

(i) if a chain t does not satisfy Keep, no extension of t satisfies Keep; (ii) for every finite clause set N, the set of chains built on a sequence of renamings of clauses in N and satisfying Keep is finite; (iii) for every cycle (t 1 , . . . , t n , t 1 ), there exists a chain (s 1 , . . . , s m ) with m ≤ n satisfying Keep such that for some k, the cycle (t 1+k , . . . , t n+k , t 1+k ) (with t i := t i-n if i > n) is an extension of (s 1 , . . . , s m ).

For example, Keep can be defined as the set of chains built on clauses C i that are pairwise distinct modulo renaming and such that C 1 is the most recently processed clause. This is the definition we use in our description of the extended saturation loop (Section 6) and in the implementation in Vampire.

Remark 15. Condition (i) is essential in practice, to ensure that the chains can be incrementally constructed in an efficient way, because it ensures that the construction can be stopped when a prefix not satisfying Keep is obtained. Condition (ii) ensures that the rule is finitely branching. Condition (iii) is essential for completeness. We also introduce the following optional simplification rule:

Γ n [• • • [Γ 1 [s ] P ] • • • ] P ≈ s ∨ C Compr (Γ 1 [s] P ≈ s ∨ C)σ
where s and s are terms of the same type τ ∈ T coind and P is a nonempty set of constructor position in Γ i , for i ∈ [1, n], such that ε ∈ P, and σ = mgu {s

? = s , Γ 1 ? = • • • ? = Γ n }.
Proposition 21 (Soundness of Compr). Let N be a clause set, and let I be a model of N satisfying FP. If D is derived from N by Compr, then I |= D.

Refutational Completeness

We establish the refutational completeness of the calculus presented in Section 4. This result ensures that the axioms for distinctness, injectivity, and acyclicity (NSub) may be omitted. The axiom Uniq may also be omitted in some cases, formally defined below. The axiom Sub is still needed since it is used in the completeness proof for Acycl.

If N is a clause set saturated under SP, then R N denotes the set of rewrite rules constructed as usual from N and → R N denotes the (one-step) reduction relation. We refer to the literature [START_REF] Bachmair | Rewrite-based equational theorem proving with selection and simplification[END_REF][START_REF] Nieuwenhuis | Paramodulation-based theorem proving[END_REF] for details about the construction of R N . The notation M N denotes the model of N defined by the congruence * ← → R N on ground terms. We first establish some results about the form of the rules in R N . The completeness proof for acyclicity requires further definitions and results. Definition 27. Let I be an interpretation and t be a term. A constructor context Γ[•] p is a minimal cyclicity witness for t and I if p is a position of the same type as t in Γ, I |= t ≈ Γ[t] p , and |q| ≥ |p| for every position q = ε and constructor context ∆[•] q such that I |= t ≈ ∆[t] q .

Proposition 28. Let (t 1 , . . . t n , t 1 ) be a cycle of constructor context Γ[•] p for a clause set N under condition D. If I |= N ∪ {¬ Dσ}, and Γ[•] p is a minimal cyclicity witness for t 1 σ and I, then (t 1 , . . . , t n , t 1 ) is direct.

Lemma 29. Let t : τ and s : υ be ground terms with τ ∼ υ. Let Γ[•] p be a ground constructor context of type τ, where p is a position of type υ in Γ. Let N be a clause set saturated under SP and Inf. Assume that t, s, and Γ| p are R N -irreducible, for every position p

≤ p. If M N |= Γ[s] p ≈ t, then R N contains n rules Γ i [a i+1 ] p i → R N a i , for i ∈ [1, n], with Γ[s] p = Γ 0 [Γ 1 [• • • [Γ n [a n+1 ] p n ] • • • ] p 1 ] p 0 , p 0 .p 1 . • • • .p n = p, a n+1 = s, and t = Γ 0 [a 1 ] p 0 .
Lemma 30 (Acyclicity). If Sub ⊆ N and N is saturated under SP, Acycl, and Inf, then M N satisfies condition Acy.

Remark 31. The Inf rule is needed for completeness. For example, it is clear that the clause x ≈ a ∨ x ≈ b contradicts acyclicity, but no contradiction can be derived without using Inf. The relaxation of the application conditions of Sup is also essential. Consider the set N = {a 1 ≈ c(a 2 ), a 2 ≈ a 3 , a 3 ≈ c(a 1 )}, with c(. . . ) a i+1 a i . It is clear that N is saturated without the relaxation, and N contradicts acyclicity, since N |= a 1 ≈ c(c(a 1 )). With the relaxation, Sup derives the clause a 2 ≈ c(a 1 ); then Acycl exploits the cycle (a 1 , a 2 , a 1 ) to derive .

For the Uniq rule, we provide a restricted completeness result, under the assumption that the considered constructor context contains at most one occurrence of •.

Lemma 32 (Uniqueness of Fixpoints). If App ⊆ N and N is saturated under SP, Uniq, and Inf, then

M N |= x ≈ Γ[x] r ∧ y ≈ Γ[y] r ⇒ x ≈ y for every constructor context of the form Γ[•] r of type τ ∈ T coind ,
where r is a nonempty position of type τ in Γ. Definition 33. A signature is coinductively nonbranching if for every constructor c :

τ 1 × • • • × τ n → τ such that τ ∈ T coind , there exists at most one i ∈ [1, n] such that τ i ∼ τ.
For example, the signature is coinductively nonbranching for infinite streams and possibly infinite lists, but not for infinite binary trees.

Corollary 34 (Fixpoints). Assume that the signature is coinductively nonbranching. If Cycl ∪ App ⊆ N and N is saturated under SP, Uniq, and Inf, then M N satisfies condition FP.

Saturation Procedure

The inference rules of the calculus presented in Section 4 are all finitely branching, provided that the eligibility criterion is applied for the Acycl and Uniq rules. As a result, saturation of a clause set can be carried out using standard saturation procedures. These generally work by maintaining a set of passive clauses that initially contains all the clauses to saturate and a set of active clauses that is initially empty. algorithm heuristically chooses a passive clause that becomes the given clause, moves it to the active clauses, and performs all possible inferences between it and the active clauses. Conclusions are added to the set of passive clauses, and the procedure is iterated until is derived, or until the set of passive clauses is empty.

To improve search, it is useful to distinguish between simplifying rules and generating rules. In simplifying rules, at least of one the premises is redundant with respect to the conclusion. The Inf rule is simplifying, as well as the Dist 1 and Inj 1 rules when the term t is not a variable, and the Acycl rule when there is only one premise and t 1 = t n .

In addition to the calculus, we propose the following simplifying rules to eliminate theory tautologies:

c( s) ≈ d( t ) ∨ C Dist - ∅ s ≈ Γ[s] ∨ C Acycl - ∅ where c d, Γ[•]
is a nonempty constructor context, and type(s) ∈ T ind . Moreover, the following rule applies injectivity of c ∈ Ctr inj to simplify literals:

c(s 1 , . . . , s n ) ≈ c(t 1 , . . . , t n ) ∨ C Inj - n i=1 s i ≈ t i ∨ C
The soundness of Inj -follows from c's being a function symbol, but since it is also injective, the premise is redundant with respect to the theory. We conjecture that the addition of these simplification rules preserves refutational completeness.

If all constructors are free (i.e., Ctr inj = Ctr and c d holds for all distinct constructors c and d), by applying the above rules eagerly, we also guarantee that in any literal [¬]s ≈ t in an active clause, at most one of s or t has a constructor for head symbol, as (dis)equalities between constructor terms will have been simplified directly after clause generation. This invariant enables a few optimizations in the implementation of the generating rules, notably during the detection of chains.

The relaxation of the application conditions of the Sup rule increases the number of clauses it must generate and may hence be detrimental to the search. We can reduce the incidence of this scenario by choosing a term order that considers constructors as smaller than non-constructors. For path orders, we can choose a symbol precedence such that f c for all non-constructor symbols f and constructors c.

To implement the Acycl and Uniq rules, we must be able to efficiently detect eligible chains among the set of active clauses. Testing all subsets of the active clauses is impractical, and the detection of a chain requires the computation of an mgu over a set of equations, instead of a single equation. We present a procedure that takes the given clause C 1 as input and applies the two rules to all subsets of clauses containing C 1 and upon which an eligible chain can be built. There are three cases in which the rules must be applied: when the chain is a cycle, when it is variable-ended and has length 1, and when there exists an extension of the chain that violates Keep. The procedure relies on a data structure that provides a nextLinks(s ) operation, where s is a term. For each literal s ≈ t in an active clause C such that s is unifiable with s under an mgu σ and sσ tσ, the operation returns the tuple (C, σ, T ), where T is the set of terms under nonempty constructor positions in t. This operation can be using term indexing techniques already found in state-of-the-art provers [START_REF] Robillard | An inference rule for the acyclicity property of term algebras[END_REF]Section 5.1].

The procedure considerGiven(C 1 ) applies the rule Acycl or Uniq to all subsets of actives clauses that contain the given clause C 1 and form an eligible chain:

Procedure considerGiven(C 1 ) is for s 2 such that C 1 = s 1 ≈ Γ[s 2 ] ∨ D 1 do extendChain(s 1 , s 2 , {}, {C 1 }) Procedure extendChain(s 1 , s i , θ, Ch) is if s 1 θ = s i θ

Evaluation

We implemented the calculus presented above in the first-order theorem prover Vampire [START_REF] Kovács | First-order theorem proving and Vampire[END_REF]. Our source code is publicly available. 1 The new rules are added to the existing calculus, which includes other sound rules and a sophisticated redundancy elimination mechanism. Vampire can process input files in SMT-LIB [START_REF] Barrett | The SMT-LIB standard: Version 2.7[END_REF] format and recognizes both the declare-datatypes command and the nonstandard declare-codatatypes command. These commands trigger the addition of relevant axioms or the activation of inference rules, according to user-specified options. This implementation is an extension of previous work done in Vampire [START_REF] Kovács | Coming to terms with quantified reasoning[END_REF]. The behavior of this older implementation can be replicated by enabling only the simplification rules of the calculus and adding the axioms Dist, Inj, Exhaust, Sub, and NSub to the initial clause set. We evaluated the implementation on 4170 problems that were used previously by Reynolds and Blanchette [START_REF] Reynolds | A decision procedure for (co)datatypes in SMT solvers[END_REF] to evaluate CVC4. These were generated by translating Isabelle problem to SMT-LIB using the Sledgehammer bridge [START_REF] Paulson | Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers[END_REF] and on synthetic problems that exercise the properties of cyclic values. Both benchmark sets and detailed results are available online. 2All the experiments in this section were carried out on a cluster on which each node is equipped with two quad-core Intel processors running at 2.4 GHz, with 24 GB of memory. A 60 s time limit per problem was enforced. We used a single basic saturation strategy relying on the DISCOUNT saturation algorithm. The calculus was parameterized by a Knuth-Bendix term order, unless otherwise noted. This simple approach provides a homogeneous basis on which to compare the performance of the different parameters. It typically solves fewer problems than the portfolio approach commonly with Vampire, in which several different strategies are tried in short time slices. We first compare the performance of three configurations of the prover on the Isabelle problems. The first configuration corresponds to the axiomatic approach presented in Section 3: the axioms Dist, Inj, Exhaust, Sub, NSub, App, Uniq, Cycl, and Hole are added to the set of clauses to saturate, and only standard inferences rules are used by the prover. Superposition need not rewrite the nonmaximal side of an equation.

The second configuration implements part of the calculus presented in Section 4. Only the axioms Exhaust, Sub, NSub, App, Uniq, Cycl, and Hole are added to the clauses, and the rules Dist 1 , Dist 2 , Inj 1 , and Inj 2 are used during the search, in addition to the simplification rules described in Section 6. The side conditions of Sup are also relaxed. The rules Acycl and Uniq are not used; instead, reasoning on the properties of cyclic terms is based on axioms.

The third configuration uses all the rules described in Section 4. Only the axioms Sub and App are added, on which the Acycl and Uniq rules depend, and the axioms Cycl and Exhaust. This configuration is the only one which does not ensure refutational completeness, since Uniq is incomplete with respect to the uniqueness of fixpoints for branching codatatypes.

The first two configurations both solved 1114 problems and the third one solved 1113 problems; 1116 problems are solved by at least one configuration. These homogeneous results do not reveal significant differences between the approaches. To assess the role of the acyclicity property of datatypes and the properties of codatatype fixpoints in the benchmarks, we also tested a system that did not include any axioms and rules related to these properties. With such an incomplete system, we found that 12 problems could not be solved. This is roughly in line with the results of Reynolds and Blanchette using CVC4 on the same problems [START_REF] Reynolds | A decision procedure for (co)datatypes in SMT solvers[END_REF]. No new problems were solved by this configuration, suggesting that reasoning about properties of cyclic terms does not lead to worse performance even when these properties are not needed for refutation.

We also tested variants of the last two configurations in which the calculus was parameterized by a lexicographic path order, to assess whether this term order could improve the performance when used with the relaxed superposition rule. These configurations solved a total of 1104 problems, including 5 new problems.

Since properties of cyclic values are seldom used in the Isabelle benchmarks, we crafted a set of (refutable) problems to assess the performance of the rules Acycl and Uniq. For a term s and a nonconstant context Γ[•], let exchain(s, Γ[•]) denote any sentence ∃s 2 , . . .

s n ∀t 1 , . . . t m . s ≈ Γ 1 [s 2 ] ∧ • • • ∧ s n ≈ Γ n [s],
where t 1 , . . . , t m all occur in Γ and such that Γ

1 [. . . [Γ n [•]] . . . ] = Γ[•]. The formula ∃s. exchain(s, Γ[•])
, where type(s) ∈ T ind , forms an acyclicity problem. The set of acyclicity problems used in our experiments is denoted AC. If m = 0, the clausified form of this problem is ground (ACG). The formula ∃s 1 , s

2 . exchain(s 1 , Γ[•]) ∧ exchain(s 2 , Γ[•]) ∧ s 1 ≈ s 2 ,
where type(s 1 ) ∈ T coind , forms a uniqueness problem (U). Note that in such a problem, the two chains may not be formed upon the same equalities, although they build the same constructor context. Similarly, if m = 0, we obtain a ground uniqueness problem (UG). Finally, the sentence ∀s. ¬ exchain(s, Γ[•]), for type(s) ∈ T coind , forms an existence problem (EX).

We generated 100 instances of each type of problem. The number of problems solved by Vampire (V) on these problems are presented in the following table, along with the results obtained using CVC4's [3] and Z3's [START_REF] De Moura | Z3: An efficient SMT solver[END_REF] native for datatypes and, in CVC4's case, for codatatypes: The number of problems solved shows that the Acycl rule performs better than the axioms for acyclicity problems with variables. Only one of these problems could be solved by the axiomatic approach and not by the Acycl rule. Both approaches managed to solve all of the ground acyclicity problems. Z3 solved all of the ground problems, performing slightly less well on those featuring universal quantifiers. CVC4 was able to solve all of the acyclicity problems, including those with universal quantifiers, a notable improvement over previous results obtained on similar problems [START_REF] Robillard | An inference rule for the acyclicity property of term algebras[END_REF]Section 6]. On uniqueness problems, the Uniq rule solved a superset of the ground problems solved by the axiomatic approach, whereas on nonground problems each approach uniquely solved 3 problems, for a total of 17 problems solved. Again, CVC4 performed remarkably well on ground problems, while the presence of variables in the problem led to a marked degradation of its performance. Finally, for existence problems, the refutation relies mostly on the Cycl axiom, which is included in the clause set in both Vampire configurations. Yet, the purely axiomatic approach was able to solve 6 problems that could not be solved when the Uniq rule was activated, indicating that the rule might lead the search in a suboptimal direction. The theory solver in CVC4 does not take into account the existence of fixpoints for codatatypes, which is a nonground property. Consequently, none of the existence problems were solved by CVC4.

AC ACG U UG EX V CVC4 Z3 V CVC4 Z3 V CVC4 V CVC4 V CVC4 Axioms 65 - - 100 - - 14
From the results, it would appear that the calculus supersedes the axiomatic approach for problems with datatypes. For codatatypes, both approaches are able to solve different problems, suggesting that they should both be included in a strategy portfolio.

Related Work

The potential of (co)datatypes for automated reasoning has been studied mostly in the context of satisfiability modulo theories (SMT). Datatypes are parts of the SMT-LIB 2.6 standard [START_REF] Barrett | The SMT-LIB standard: Version 2.7[END_REF]. They were implemented in CVC3 by Barrett et al. [5], in Z3 [START_REF] De Moura | Z3: An efficient SMT solver[END_REF] by de Moura, and in CVC4 by Reynolds and Blanchette [START_REF] Reynolds | A decision procedure for (co)datatypes in SMT solvers[END_REF]. The CVC4 work also includes a decision procedure for the ground theory of codatatypes. Moreover, CVC4 supports automatic structural induction [START_REF] Reynolds | Induction for SMT solvers[END_REF] and dedicated reasoning support for selectors.

Structural induction has also been added to superposition by Kersani and Peltier [START_REF] Kersani | Combining superposition and induction: A practical realization[END_REF], Cruanes [START_REF] Cruanes | Superposition with structural induction[END_REF], and Wand [START_REF] Wand | Superposition: Types and Polymorphism[END_REF]. In unpublished work, Wand implemented incomplete inference rules for datatypes, including acyclicity, in his superposition prover Pirate. Robillard's earlier Acycl rule [START_REF] Robillard | An inference rule for the acyclicity property of term algebras[END_REF] has inspired our Acycl rule, but it suffered from many forms of incompleteness. For example, given the unsatisfiable clause set { a ≈ c(x) ∨ p(x), ¬ p(c(a))}, the old Acycl rule derived only p(a) before reaching saturation. Another issue concerned cycles built from multiple copies of the same premise.

In the context of program verification, Bjørner [START_REF] Bjørner | Integrating Decision Procedures for Temporal Verification[END_REF] introduced a decision for (co)datatypes in STeP, the Stanford Temporal Prover. The program verification tool Dafny provides both a syntax for defining (co)datatypes and some support for automatic (co)induction proofs [START_REF] Leino | Co-induction simply-Automatic co-inductive proofs in a program verifier[END_REF]. Other verification tools such as Leon [START_REF] Suter | Satisfiability modulo recursive programs[END_REF] and RADA [START_REF] Pham | RADA: A tool for reasoning about algebraic data types with abstractions[END_REF] also include (semi-)decision procedures for datatypes. We refer to Barrett et al. [START_REF] Barrett | An abstract decision procedure for satisfiability in the theory of inductive data types[END_REF] and Reynolds and Blanchette [START_REF] Reynolds | A decision procedure for (co)datatypes in SMT solvers[END_REF] for further discussions of related work.

Conclusion

We presented two approaches to reason about datatypes and codatatypes in first-order logic: an axiomatization and an extension of the superposition calculus. We established completeness results about both. We also showed how to integrate the new inference rules in a saturation prover's main loop and implemented them in the Vampire prover. The empirical results look promising, although it is not clear from our benchmarks how often the most difficult properties-acyclicity for datatypes, existence and uniqueness of fixpoints for codatatypes-are useful in practice.

This work is part of a wider research program that aims at bridging the gap between automatic theorem provers and their applications to program verification and interactive theorem proving. In future work, we want to reconstruct the new proof rules in Isabelle, to make it possible to enable datatype reasoning in Sledgehammer. We also believe that further tuning and evaluations could help improve the calculus and the heuristics.

  and cst τ υ : τ → τ υ be new function symbols. Intuitively, if y denotes the context Γ[•] P , then app(x, y) denotes the term Γ[x] P , cyc(y) denotes the fixpoint of Γ[•] P , and cst τ υ denotes a constant context (i.e., a context Γ[•] P with P = ∅).

Lemma 4 (

 4 Soundness of the Axioms). If interpretation I satisfies Acy and FP, there exists a sub-minimal extension of I validating Sub, NSub, App, Uniq, Cycl, and Hole. Lemma 5 (Completeness of the Axioms). Any model of the set of axioms {Sub, NSub, App, Uniq, Cycl, Hole} fulfills Acy and FP. Lemma 6 (Completeness of the Theory). Let T be the theory of free constructors, as defined by the properties Exh, Inf, Acy, FP, Dst, and Inj, with Ctr inj = Ctr and c d for all distinct constructors c and d. If S is a first-order sentence in which the only symbols occurring are constructors and equality (≈), then either T |= S or T |= ¬ S.

Lemma 7 ( 1

 71 Soundness of Inf). Let N be a clause set, and let I be a model of N satisfying Inf. If C is derived from N by Inf, then I |= C. Distinctness. The distinctness property of constructors takes the form of two rules: c( s) ≈ t ∨ C Dist Cσ if σ = mgu {t ? = d( x)}, where c d and x are fresh pairwise distinct variables; and

  uσ, and d( t )σ u σ. Proposition 8 (Soundness of Dist 1 and Dist 2 ). Let N be a clause set, and let I be a model of N satisfying Dst. If a clause C is derived from N by Dist 1 or Dist 2 , then I |= C.

Proposition 22 .

 22 Let N be a clause set saturated under SP and Inf. Let u ≈ v ∨ C ∈ N, and let θ be a substitution such that uθ vθ, (u ≈ v)θ Cθ, and M N |= Cθ. If type(u) ∈ T ind ∪ T coind , then u is not a variable. Corollary 23. Let N be a clause set saturated under SP and Inf. For every rule c( t ) → R N s in R N , where c is a constructor, s is R N -irreducible. Lemma 24 (Infiniteness). Let N be a clause set saturated under SP and Inf. If / ∈ N, then M N satisfies Inf. Lemma 25 (Distinctness). Let N be a clause set saturated under SP, Dist 1 , Dist 2 , and Inf. For all ground terms a = c(ā) and b = d( b) such that c d, we have a * ← → R N b. Lemma 26 (Injectivity). Let N be a clause set saturated under SP, Inf, Inj 1 , and Inj 2 . For all ground terms a = c(a 1 , . . . , a n ) and b = c(b 1 , . . . , b n ) with c ∈ Ctr inj and such that a i * ← → R N b i for some i ∈ [1, n], we have a * ← → R N b.

Example 35 .

 35 Corollary 34 does not hold for arbitrary signatures. The clause set {a ≈ c(d(a, b)), b ≈ e(d(a, b)), a ≈ c(d(a , b )), b ≈ e(d(a , b )), d(a, b) ≈ d(a , b )} contradicts FP, because d(a, b) and d(a , b ) are both solutions of x ≈ d(c(x), e(x)). However, the Uniq rule applies only with constructor contexts of head symbol c (if the chain starts with a or a ) or e (if it starts with b or b ).

  where x is a variable of type τ not occurring in Γ;• FP (existence and uniqueness of fixpoints, for codatatypes) iff, for every type τ ∈ T coind , for every nonempty constructor context Γ[•] P , I |= (∃x. Γ[x] P ≈ x) ∧

	(Γ[x] P ≈ x ∧ Γ[y] P ≈ y = ⇒ x ≈ y), where x, y are fresh variables of type τ;
	• Dst (distinctness of constructors) iff, for every pair of constructors c, d of the same
	codomain such that c d, I |= c( x) ≈ d(ȳ) where x and ȳ are disjoint vectors of
	pairwise distinct variables of the appropriate length and types;
	• Inj (injectivity) iff, for every n-ary constructor c ∈ Ctr inj and pairwise distinct vari-
	ables x 1 , . . . , x n , y 1 , . . . , y n of the appropriate types, I |= c(x 1 , . . . , x n ) ≈ c(y 1 , . . . , y n ) = ⇒ n i=1

  Definition 16. A chain of length n is eligible if it is variable-ended and n = 1, or if it is not variable-ended, it satisfies Keep, and either it is a cycle or there exists an extension of length n + 1 that does not satisfy Keep.Lemma 20 (Soundness of Uniq). Let N be a clause set, and let be a model of N ∪ {App, Hole} satisfying FP. If C is derived from N by Uniq, then I |= C.

  then apply rule Acycl or Uniq to chain Ch under mgu θ else if s i is a variable then if |Ch| = 1 then apply rule Acycl or Uniq to chain Ch under mgu θ else if exists (C i , σ, T ) ∈ nextLinks(s i θ) such that C i ∈ Ch then apply rule Acycl or Uniq to chain Ch under mgu θ else for (C i , σ, T ) ∈ nextLinks(s i θ) do extendChain(s 1 , s i+1 , σθ, Ch {C i })

http://github.com/vprover/vampire/releases/tag/ijcar2018-data

http://matryoshka.gforge.inria.fr/pubs/supdata _ data.tar.gz

Acknowledgment. We thank Alexander Bentkamp, Simon Cruanes, Uwe Waldmann, Daniel Wand, and Christoph Weidenbach for fruitful discussions that led to this work. We also thank Mark Summerfield and the anonymous reviewers for suggesting textual improvements.

Blanchette has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka). Robillard has received funding from the ERC Starting Grant 2014 SYMCAR 639270, the Wallenberg Academy Fellowship 2014 TheProSE, the Swedish Research Council grant Gen-Pro D0497701, and the Austrian FWF research project RiSE S11409-N23.

Remark 17. The conditions on eligible chains are the ones preserving completeness, but they are not necessary for soundness.

The acyclicity rule follows:

C 1 Uniqueness of Fixpoints. The uniqueness rule also depends on the notion of chain:

if there exists an eligible chain (t 1 , . . . , t n+1 ) of constructor context Γ[•] q built on (C 1 , . . . , C n ) under condition D and the following requirements are met:

1. u = Γ[t n+1 ] q ; 2. P is the set of positions p of some type τ ∼ type(t 1 ) in u such that p < q; 3. for every p ∈ P, s p is a fresh variable of the appropriate context type; 4. u is obtained from u by replacing all terms at a position p ∈ P by app(s p , z).

Intuitively, the existence of the chain ensures (if D is false) that t 1 ≈ Γ[t n+1 ] q . If t 1 = t n+1 , we could derive y ≈ Γ[y] q ∨ y ≈ t 1 by uniqueness. However, this would not be sufficient for completeness. First, t 1 may be distinct from t n+1 , but we may have t n+1 = ∆[t 1 ] Q , for some constructor context ∆, in which case we should derive y ≈ Γ[∆[y] Q ] q ∨ y ≈ t 1 instead. Second, t 1 may also occur at other positions in Γ. To capture all these cases using a finitely branching rule, we introduce new variables s p whose purpose is to denote the context Γ p such that Γ p [t 1 ] = u| p . (If t 1 does not occur inside u| p , then Γ p is constant.) Example 19. From the clause a ≈ c(b, x), using the chain (a, x), with the constructor context c(b, •), we derive


Rosa Michaelson
email: r.michaelson@dundee.ac.uk

The Challenge of Change: reducing conflict in implementing e-learning

Keywords: e-learning, design focus for Grid technologies, teacher's rights, Information Systems methodologies, managing change

This paper calls for the design of the European Grid for Learning to take note of important issues which have arisen in previous e-learning cycles in the UK. In particular, low take-up of products and services by lecturers has been explained in terms of techno-fear, or ignorance of e-learning potential. These claims are unsubstantiated. Other explanations are possible for the observed resistance of the educational specialist to the use of educational technology. Rather than ignore possible areas of conflict, or to assume (after Foucault) that any change results in shifts of power which produce inevitable counter-balances from a threatened group, it is possible to use resistance to change as an important part of the design process. To this end, I discuss the findings of an analysis of recent UK-wide initiatives in C&IT and e-learning. The issues raised by participants of the many different groups involved have implications for the take-up of future Grid-based learning. In particular, the needs of educators are identified as crucial to the effective deployment of e-learning.

BACKGROUND

In the UK Higher Education sector online learning has been greeted with enthusiasm by many. For example, the UK-wide e-University has been launched to meet a suggested lack in HE online provision for lifelong learning [START_REF]ICT in Higher Education[END_REF]. The growth of the virtual university, such as the global conglomerates Fathom and Cardean University, based on Unext.com, has been perceived as a threat to standard university education [START_REF] Kirschner | Fathom: the global university[END_REF], [START_REF] Rosenfield | unxt.com (founder, chairman and CEO of unxt.com[END_REF]. Many such ambitious e-learning projects have failed [START_REF] Ryan | Emerging indicators of success and failure in borderless higher education[END_REF].

Evaluation of large Information Systems implementation, and in particular of IS failure, leads to the understanding of the importance of counter-implementation and resistance to change, informing methods which reduce conflict and improve design processes [START_REF] Keen | Information Systems and Organizational Change[END_REF], [START_REF] Beynon-Davies | Human error and information systems failure: the case of the London ambulance service computer-aided despatch system project[END_REF]. In order to inform the effective design of a European Grid for Learning we need to consider possible problem areas which might be of concern to the lectures and teachers who will use Gridenabled applications. This paper outlines issues that arose in two UK-wide initiatives which have deployed C & IT in Higher and Further Education. The first initiative of interest was the Teaching and Learning Technologies Project (TLTP). This initiative has recently ended, after10 years of funding. The first phases of the TLTP consisted of 72 subject-specific projects, many of which produced multimedia resources. More recent projects focused on web-based delivery of these products, and other forms of networked education.

The second initiative, which has been promoted by JISC (the Joint Information Systems Committee), concerns the use of Learning Environments (LE). Within UK higher and further education there are now many users of web-based applications variously described as virtual learning environments (VLE) including First Class, WebCT and BlackBoard. Many institutions are also using locally developed VLE such as TAGS, COSE and Merlin [START_REF] Allison | Using TAGS for Distributed IT Project Management[END_REF], [START_REF][END_REF], [9]. More recently managed learning environments (MLE) -the integration of VLE with the institutions MIS -have been the main funding focus for JISC supported projects [START_REF] Michaelson | Let's get real: Virtual or Managed Learning Environments[END_REF].

IMPORTANT ISSUES

An analysis of the above initiatives has identified the following issues as problematic for elearning [START_REF] Michaelson | Learning from our mistakes: 10 years of UK-wide C&IT initiatives[END_REF], [START_REF] Michaelson | Let's get real: Virtual or Managed Learning Environments[END_REF]:

• Cost • Evaluation • Sustainability • Focus • Standards • Social Learning • De-skilling
• Acceptance and take-up Many of the above have implications for those who are intended to use the new educational technologies, namely the lecturers and teachers. The next section details the problems that were identified in the analysis of reports and papers generated by the initiatives.

IMPACT OF E-LEARNING ISSUES

Cost

The actual cost of networked learning is contentious. Many claim cost-benefits for e-learning. The main assumption is that there is no extra cost, or comparable costs, in using educational technology. This was expressed as the need to show efficiency gains during the TLTP period. There are those who claim that they know about the cost of developing C&IT, but assumptions concerning economies of scale or time-scale of use adjust the true cost downwards [START_REF] Bacsich | The cost of networked learning[END_REF]. It is unusual for infrastructure and maintenance costs (which are of great importance for e-learning service provision) to be explicitly included in cost-benefit analysis.

Evaluation

What is evaluated? There seems confusion over how to evaluate learning efficacy via educational technology. The focus of evaluation varies from usability issues, type of application, software functionality [START_REF] Britain | A Framework for Pedagogical Evaluation of Virtual Learning Environments[END_REF], 'soft' studies of student attitudes, and as suggested above, cost. There are few evaluations of the UK-wide impact of particular programmes for C&IT [START_REF] Selwyn | Researching computers and education -glimpses of the wider picture[END_REF], [START_REF] Michaelson | Let's get real: Virtual or Managed Learning Environments[END_REF].

Sustainability

Sustainability has a persistent theme for the last 30 years of C&IT in education, as it has for computing in general. Timeliness of adoption of new technologies by a community has a farreaching effect on sustainability: by the time a novel technology has been taken up in the wider educational community it is out of date. In addition the research efforts of those who test the particular technology are ignored as managers wish to use off-the-shelf commercial solutions. The paradox of research and development in educational technologies is that during the lifetime of the project there is already some other technology on the horizon which will supersede or replace the focus of the current enthusiasm. The replacement technologies often over-stretch the existing infrastructure requirements.

Focus

An important issue for the success of any IS project is focus. However, educational or pedagogic objectives are rarely discussed by those who drive initiatives. It is often the case that the originators of change promote the idea that a particular problem will be solved by the application of technology, even if there is no evidence for such an outcome. For example, in the UK the wider access agenda is often expected to be solved by e-learning, thereby ignoring the costs to the individual, and the high drop-out rates of distance learning.

Social Learning e-learning blurs the distinction between Distance Learning versus campus-based learning.

There is an assumed equivalence of these models which needs to be carefully considered. Networked learning institutes are often given the name 'university' but are more akin to distance learning establishments such as the UK Open University than the majority of campus-based institutions. What are the implications for the teacher's role when such blurring occurs? How does this affect the role of the social in learning? [START_REF] Peters | The iceberg has not melted: further reflections on the concept of industrialisation and distance teaching[END_REF], [START_REF] Brown | The Social Life of Information[END_REF].

The Threat of de-skilling

Is the objective of e-learning the replacement of the educator? Threats to the educator's professionalism include unbundling and interoperability. The concept of unbundling follows the division of labour needs of Distance Learning discussed above. Patel and Franklin's report to JISC on MLE states: "Unbundling the delivery of HE courses is a key issue in the provision of a national learning infrastructure. Currently the delivery of courses in HE is bundled i.e. the same people design develop and deliver courses and materials and deliver and conduct assessment and courses are studied as a whole at one institution." [START_REF] Patel | Summary Briefing Paper on issues for the development and implementation of MLE[END_REF] Thus the professional role of the lecturer or teacher in controlling their own materials is directly challenged by the impetus of networked learning.

There has also been, in the UK, an unpredicted growth of 'specialised' support -the Learning Technologist with as yet no formal or professional status within the sector. Some propose that learning technologists are vital to re-introduce the social learning aspects to e-learning [START_REF] Salmon | E-moderating: the key to teaching and learning online[END_REF]. What is the new role of the lecturer if learning technologists or e-moderators are required to make e-learning work?

Standards

In the case of web-based learning the need for interoperability of systems translates into a quest for meta-data or classification systems for educational content. Here content is talked about in terms of 'learning objects' or 'chunks' which may have wider application than a specific course and are seen as the key to material being created in one system and being transferable between different systems. There are still unresolved issues of quality and consistency associated with this view. In addition the management of learning is seen only in terms of the production of small enough 'chunks'. Unfortunately there is as yet no single definition of what constitutes a 'learning object'. Many vendors are creating their own definitions with little recourse to the diversity of practise among educators. Hence there are competing standards, some of which emerge from training in the US (e.g. SCORM, ADL). This also raises issues concerning cultural differences in education. There is already work to show that expectations of the way teachers use material have proved incorrect [START_REF] Monthienvichienchai | Educational Metadata: Teacher's Friend or Foe? in Euro CSCL[END_REF].

Acceptance and Take-up

By the end of the TLTP initiative it was discovered that very few products were in use. Those employed were generally for pre-university education -often used to bring students up to a particular level of achievement. The common consensus from those involved in the projects was that to increase use staff needed to be taught about C&IT. The concept of possible replacement of staff by new technologies, and hence cost-benefits, were rejected. The technology was seen as an addition to range of techniques available for lecturers and teachers. This had an additional effect on take-up, also noted in the LE initiative. Lectures noted that this addition of technology increased the individual workload tremendously. In the case of production of content for LE this may seem so overwhelming, given that staff continue to teach with traditional methods, that they cannot easily include LE in their teaching practise.

POSSIBLE REASONS FOR CONFLICT

Those who are not educators, or enthusiasts for particular applications, tend to explain resistance to using C&IT as being based on lack of staff-development or lack of management support for the champions of e-learning. Other explanations also include the claim that lecturers are scared of new technology. In fact, most lecturers in HE have assimilated computing technology as part of their everyday work -the production of overhead slides, the administration of student records, the use of e-mail for communicating with colleagues, students and research collaborators, the use of the Internet as an additional resource -all of these are common in UK academic life. What is difficult for those with involvement in research and development of novel educational technology to recognise, is that they may have ignored the diverse educational styles and objectives of professional staff, or that they may have designed unusable applications.

Another factor in the effective take-up of new technologies is that enthusiasm for C&IT deployment in education produces a subsequent, often unrecognised, growth in IT infrastructure since all C&IT is dependent on increased IT resources. This increases the influence that technologists have on the educational process, without engaging the educationalist. In addition, Managerialism in e-learning manifests itself in ideas of cost-effectiveness; the replacement of the lecturer by technology; the introduction of the specialist technology moderator (the threat of de-skilling the educator); concepts of unbundling and granularity of content; the down-grading of pedagogy; assumptions of metadata classification by the nonspecialist; and the intervention of IT support and administration into teaching style (as in the MLE program). Can these types of conflict be avoided by possible future Grid technologies?

CONCLUSION

I would argue, in the light of these issues that in order to design effective Grid-based e-learning the current processes of education must be more fully understood. Educational objectives must be a focus for the design, as must the wishes and needs of the educators. The idea of radical change, brought about by new technologies, cannot be realised without understanding possible points of conflict such as those identified in previous initiatives.

2nd International LeGE-WG Workshop on e-Learning and Grid Technologies: a fundamental challenge for Europe