Alexander Bentkamp
email: a.bentkamp@vu.nl

Jasmin Christian Blanchette

Simon Cruanes

Uwe Waldmann

Superposition for Lambda-Free Higher-Order Logic

We introduce refutationally complete superposition calculi for intentional and extensional λ-free higher-order logic, two formalisms that allow partial application and applied variables. The calculi are parameterized by a term order that need not be fully monotonic, making it possible to employ the λ-free higherorder lexicographic path and Knuth-Bendix orders. We implemented the calculi in the Zipperposition prover and evaluated them on TPTP benchmarks. They appear promising as a stepping stone towards complete, efficient automatic theorem provers for full higher-order logic.

, it suffers from a number of weaknesses, all related to its gracelessness. Transforming all the function symbols into constants considerably restricts what can be achieved with term orders; for example, argument tuples cannot be compared using different methods for different symbols. In a prover, the encoding also clutters the data structures, slows down the algorithms, and neutralizes the heuristics that look at the terms' root symbols. But our chief objection is the sheer clumsiness of encodings and their poor integration with interpreted symbols. And they quickly accumulate; for example, using the traditional encoding of polymorphism relying on a distinguished binary function symbol t [8, Section 3.3] in conjunction with the applicative encoding, the term S x becomes t(nat, app(t(fun(nat, nat), S), t(nat, x))).

. As a result, hybrid encodings are not an ideal basis for higher-order automated reasoning. Instead, we propose to generalize the superposition calculus to intensional and extensional λ-free higher-order logic. In the extensional version of the logic, the property (∀x. h x ≈ k x) -→ h ≈ k holds for all functions h, k of the same type. For each logic, we present two calculi (Section 3). The intentional calculi perfectly coincide with standard superposition on first-order clauses; the extensional calculi depend on an extra axiom.

 and the Knuth-Bendix order (KBO) [3] with argument coefficients, but they both lack this property. For example, given a KBO with g f, it may well be that g a ≺ f a if f has a large enough multiplier on its argument.

, together with more explanations and examples.

 and compare them with the applicative encoding (Section 6). We find that there is a substantial cost associated with the applicative encoding and that the nonmonotonicity is not particularly expensive.

Introduction

Superposition is a highly successful calculus for reasoning about first-order logic with equality. We are interested in graceful generalizations to higher-order logic: calculi that, as much as possible, coincide with standard superposition on first-order problems and that scale up to arbitrary higher-order problems.

As a stepping stone towards full higher-order logic, in this paper we restrict our attention to a λ-free fragment of higher-order logic that supports partial application and application of variables (Section 2). This formalism is expressive enough to permit the axiomatization of higher-order combinators such as pow τ : nat → (τ → τ) → τ → τ:

pow 0 h ≈ id pow (S n) h x ≈ h (pow n h x)
Conventionally, functions are applied without parentheses and commas, and variables are italicized. Notice the variable number of arguments to pow and the application of h. The expressiveness of full higher-order logic can be recovered by introducing SK-style combinators to represent λ-abstractions and proxies for the logical symbols [START_REF] Kerber | How to prove higher order theorems in first order logic[END_REF][START_REF] Robinson | A note on mechanizing higher order logic[END_REF].

A widespread technique to support partial application and application of variables in first-order logic is to make all symbols nullary and to represent application of functions of type τ → υ by a family of binary symbols app τ,υ . Following this scheme, the higher-order term f (h f) is translated to app(f, app(h, f)), which can be processed by first-order methods. We call this the applicative encoding. The existence of such a reduction explains why λ-free higher-order terms are also called "applicative first-order terms." Unlike for full higher-order logic, most general unifiers are unique for our λ-free fragment, just as they are for applicatively encoded first-order terms.

Logic

Refutational completeness of calculi for higher-order logic (also called simple type theory) is usually stated with respect to Henkin semantics [START_REF] Benzmüller | Automation of higher-order logic[END_REF][START_REF] Henkin | Completeness in the theory of types[END_REF], in which the universes used to interpret functions need only contain the functions that can be expressed as terms. Since the terms of λ-free higher-order logic exclude λ-abstractions, in "λ-free Henkin semantics" the universes interpreting functions can be even smaller. Unlike other higher-order logics, there are no comprehension principles, and we disallow nesting of Boolean formulas inside terms, as a convenient intermediate step on our way towards full higher-order logic.

Problematically, in a logic with applied variables but without Hilbert choice, skolemization is unsound, unless we make sure that Skolem symbols are suitably applied [START_REF] Miller | A compact representation of proofs[END_REF]. We achieve this using a hybrid logic that supports both mandatory (uncurried) and optional (curried) arguments. Thus, if symbol sk takes two mandatory and one optional arguments, sk(x, y) and sk(x, y) z are valid terms. Nevertheless, as in our earlier work [START_REF] Becker | A transfinite Knuth-Bendix order for lambda-free higher-order terms[END_REF][START_REF] Blanchette | A lambda-free higher-order recursive path order[END_REF], we use the adjective "graceful" in the strong sense that we can exploit optional arguments, identifying the first-order term f(x, y) with the curried higher-order term f x y.

A type τ, υ of λ-free higher-order logic is either an element ι of a fixed set of atomic types or a function type τ → υ of functions from type τ to type υ. In our hybrid logic, a type declaration for a symbol is an expression of the form τn ⇒ τ (or simply τ if n = 0). We write ān or ā to abbreviate the tuple (a 1 , . . . , a n ) or product

a 1 × • • • × a n , for n ≥ 0.
We fix a set V of typed variables, denoted by x : τ or x. A signature consists of a nonempty set Σ of symbols with type declarations, written as f : τ ⇒ τ or f. We reserve the letters s, t, u, v for terms and x, y, z for variables and write : τ to indicate their type.

The set of λ-free higher-order terms T X Σ over X is defined inductively. Every variable in X ⊆ V is a term. If f : τn ⇒ τ and u i : τ i for all i ∈ {1, . . . , n}, then f(ū n ) : τ is a term. If t : τ → υ and u : τ, then t u : υ is a term, called an application. Non-application terms ζ are called heads. Terms can be decomposed in a unique way as a head ζ applied to zero or more arguments: ζ s 1 . . . s n or ζ sn (abusing notation). Substitution and unification are generalized in the obvious way, without the complexities associated with λ-abstractions; for example, the most general unifier of x b z and f a y c is {x → f a, y → b, z → c}, and that of h (f a) and f (h a) is {h → f}.

Formulas ϕ, ψ are of the form ⊥, , ¬ ϕ, ϕ ∨ ψ, ϕ ∧ ψ, ϕ -→ ψ, t ≈ τ s, ∀x. ϕ, or ∃x. ϕ, where t, s are terms and x is a variable. We let s ≈ t abbreviate ¬ s ≈ t. We normally view equations s ≈ t as unordered pairs and clauses as multisets of such (dis)equations.

Loosely following Fitting [START_REF] Fitting | Types, Tableaus, and Gödel's God[END_REF], an interpretation J = (U, E, J ) consists of a typeindexed family of nonempty sets U τ , called universes; a family of functions E τ,υ : U τ→υ → (U τ → U υ ), one for each pair of types τ, υ; and a function J that maps each symbol with type declaration τn ⇒ τ to an element of U τ n → U τ . An interpretation is extensional if E τ,υ is injective for all τ, υ. Both intensional and extensional logics are widely used. The semantics is standard if E τ,υ is bijective. A valuation ξ is a function that maps variables x : τ to elements of U τ .

For an interpretation (U, E, J ) and a valuation ξ, the denotation of a term is defined as follows:

x ξ J = ξ(x); f( t ) ξ J = J (f)( t ξ J ); s t ξ J = E( s ξ J )( t ξ J ).
The truth value ϕ ξ J ∈ {0, 1} of a formula ϕ is defined as in first-order logic. The interpretation J is a model of ϕ, written J |= ϕ, if ϕ ξ J = 1 for all valuations ξ.

The Inference Systems

We introduce four versions of the superposition calculus, varying along two axes: intentional versus extensional, and nonpurifying versus purifying. To avoid repetitions, our presentation unifies them into a single framework.

The Inference Rules

The calculi are parameterized by a partial order on terms that is well founded, total on ground terms, and stable under substitutions and that has the subterm property. It must also be compatible with function contexts, meaning that t t implies both f( s, t , ū) v f( s, t, ū) v and s t ū s t ū. On the other hand, it need not be compatible with optional arguments: s s need not imply s t s t. Function contexts are built around argument subterms, defined as the reflexive transitive closure of the relation inductively specified by f( s) t s i and ζ t t i for all i. We write s u to indicate that the subterm u of s[u] is an argument subterm. For example, f and f a are subterms of f a b, but not argument subterms. The literal and clause orders are defined as multiset extensions in the usual way.

Literal selection is supported. The selection function maps each clause C to a subclause of C consisting of negative literals. A literal L is (strictly) eligible in C if it is selected in C or there are no selected literals in C and L is (strictly) maximal in C.

We start with the extensional nonpurifying calculus, which consists of five rules:

D D ∨ t ≈ t C C ∨ [¬] s u ≈ s SUP (D ∨ C ∨ [¬] s t ≈ s )σ C ∨ s ≈ t ∨ s ≈ t EQFACT (C ∨ t ≈ t ∨ s ≈ t )σ C ∨ s ≈ s EQRES C σ C ∨ s ≈ s ARGCONG C ∨ s x ≈ s x C ∨ s x ≈ s x POSEXT C ∨ s ≈ s
In the first three rules, σ denotes the most general unifier of the two grayed terms.

For SUP, we assume that D's and C's variables have been standardized apart. For SUP, EQFACT, and EQRES, the following standard order conditions apply on the premises after the application of σ: The last literal in each premise is eligible and even strictly eligible for positive literals of SUP. For the last literal of each premise of SUP and the last two literals of the premise of EQFACT, the left-hand sides are not smaller than or equal to ( ) the respective right-hand sides. For SUP, Cσ Dσ.

Definition 1. A term of the form x sn , for n ≥ 0, jells with a literal t ≈ t ∈ D if t = t ȳn and t = t ȳn for some t, t and distinct variables ȳn that do not occur elsewhere in D.

We add the following variable condition as a side condition to SUP, to further prune the search space, using the naming convention from Definition 1 for t :

If u has a variable head x and jells with the literal t ≈ t ∈ D, there must exist a ground substitution θ with tσθ t σθ and Cσθ ≺ C σθ, where

C = C[x → t ].
This condition generalizes the standard condition that u / ∈ V. The two coincide if C is first-order. In some cases involving nonmonotonicity, the variable condition effectively mandates SUP inferences at variable positions, but never below.

The last two rules are nonstandard. For ARGCONG, s ≈ s must be strictly eligible in the premise, and x is a tuple of fresh variables. For POSEXT, s x ≈ s x must be strictly eligible in the premise, and x is a tuple of distinct variables that occur nowhere else in the premise. Furthermore, for every function type τ → υ occurring in the input problem, we introduce a Skolem symbol diff τ,υ : (τ → υ) 2 ⇒ τ characterized by the following extensionality axiom: h

(diff(h, k)) ≈ k (diff(h, k)) ∨ h ≈ k.
The second calculus is the intensional nonpurifying variant. We obtain it by removing the POSEXT rule and the extensionality axiom and by replacing the variable condition with "if u ∈ V, there exists a ground substitution θ with tσθ t σθ and Cσθ ≺ C[u → t ]σθ." For monotone term orders, this condition amounts to u / ∈ V.

By contrast, the purifying calculi never perform superposition at variables. Instead, they rely on purification [START_REF] Brand | Proving theorems with the modification method[END_REF][START_REF] Snyder | Goal directed strategies for paramodulation[END_REF] (also called abstraction) to circumvent nonmonotonicity. The idea is to rename apart problematic occurrences of a variable x in a clause to x 1 , . . . , x n and to add purification literals x 1 ≈ x, . . . , x n ≈ x to connect the new variables. We must then purify the initial clauses and all derived clauses.

In the extensional purifying calculus, the purification pure(C) of clause C is defined as the result of the following iterative procedure. Consider the literals of C excluding those of the form y ≈ z. If these literals contain both x ū and x v as distinct argument subterms, replace all argument subterms x v with x i v, where x i is fresh, and add the purification literal x i ≈ x. This calculus variant contains the POSEXT rule and the extensionality axiom. The conclusion E of each rule is changed to pure(E), except for POSEXT, which preserves purity. Moreover, the variable condition is replaced by "either u has a non-variable head or u does not jell with the literal t ≈ t ∈ D."

In the intensional purifying calculus, we define pure(C) iteratively as follows.

Consider the literals of C excluding those of the form y ≈ z. If these literals contain a variable x both applied and unapplied, replace all unapplied occurrences of x in C by a fresh variable x i and add the purification literal x i ≈ x. We remove the POSEXT rule and the extensionality axiom. The variable condition is replaced by "u / ∈ V." The conclusion C of ARGCONG is changed to pure(C); the other rules preserve purity.

Finally, we impose some additional restrictions on literal selection. In the nonpurifying variants, a literal may not be selected if x ū is a maximal term of the clause and the literal contains an argument subterm x v with v = ū. In the extensional purifying calculus, a literal may not be selected if it contains a variable that is applied to different arguments in the clause. In the intensional purifying calculus, a literal may not be selected if the literal contains an unapplied variable that also appears applied in the clause.

Rationale for the Inference Rules

A key restriction of all four calculi is that they superpose only onto argument subterms, mirroring the requirement that the term order enjoy compatibility with function contexts. The ARGCONG rule then makes it possible to simulate superposition onto non-argument subterms. However, in conjunction with the SUP rule, ARGCONG can exhibit an unpleasant behavior, which we call argument congruence explosion:

g ≈ f ARGCONG g x ≈ f x h a ≈ b SUP f a ≈ b g ≈ f ARGCONG g x y z ≈ f x y z h a ≈ b SUP f x y a ≈ b
In both cases, the higher-order variable h is effectively the target of a SUP inference. Such derivations essentially amount to superposition at variable positions (as shown on the left) or even superposition below variable positions (as shown on the right), both of which can be extremely prolific. In standard superposition, the explosion is averted by the condition on the SUP rule that u / ∈ V. In the extensional purifying calculus, the variable condition tests that either u has a non-variable head or u does not jell with the literal t ≈ t ∈ D, which prevents derivations such as the above. In the corresponding nonpurifying variant, some such derivations may need to be performed when the term order exhibits nonmonotonicity for the terms of interest.

In the intensional calculi, the explosion can arise even for monotonic orders, and it must be tamed by heuristics. The reason is connected to the absence of the POSEXT rule (which would be unsound). The variable condition in the extensional calculi is designed to prevent derivations such as those shown above, but since it only considers the shape of the clauses, it might also block SUP inferences whose side premises do not originate from ARGCONG. Consider a left-to-right LPO [START_REF] Blanchette | A lambda-free higher-order recursive path order[END_REF] instance with precedence h g f b a, and consider the following unsatisfiable clause set:

g (x b) x ≈ a g (f b) h ≈ a h x ≈ f x
The only possible inference from these clauses is POSEXT, showing its necessity. It is unclear whether POSEXT is necessary for the extensional purifying variant as well, but our completeness proof suggests that it is. Our proof also suggests that to achieve refutational completeness, due to nonmonotonicity, we need either to purify the clauses or to allow some superposition at variable positions, as mandated by the respective variable conditions. However, we have yet to find an example that demonstrates the necessity of these measures. A significant advantage of our calculi over the use of standard superposition on applicatively encoded problems is the flexibility they offer in orienting equations. The following example gives two definitions of addition on Peano numbers:

add L 0 y ≈ y add R x 0 ≈ x add L (S x) y ≈ add L x (S y) add R x (S y) ≈ add R (S x) y
Let add L (S 100 0) n ≈ add R n (S 100 0) be the negated conjecture. With LPO, we can use a left-to-right comparison for add L 's arguments and a right-to-left comparison for add R 's arguments to orient all four equations from left to right. Then the negated conjecture can be simplified to S 100 n ≈ S 100 n by rewriting (demodulation), and ⊥ can be derived with a single inference. If we use the applicative encoding instead, there is no instance of LPO or KBO that can orient both recursive equations from left to right. For at least one of the two sides of the negated conjecture, the rewriting is replaced by 100 SUP inferences, which is much less efficient, especially in the presence of additional axioms.

Redundancy Criterion

For our calculi, a redundant (or composite) clause cannot simply be defined as a clause whose ground instances are entailed by smaller (≺) ground instances of existing clauses, because this would make all ARGCONG inferences redundant. Our solution is to base the redundancy criterion on a weaker ground logic in which argument congruence does not hold. This logic also plays a central role in our completeness proof, to reason about the nonmonotonicity emerging from the lack of compatibility with optional arguments. The weaker logic is defined via an encoding of ground hybrid λ-free higherorder terms into uncurried terms, with as its inverse. Accordingly, we refer to clausal λ-free higher-order logic as the ceiling logic and to its weaker relative as the floor logic. Essentially, the encoding indexes each symbol occurrence with its argument count. Thus, f = f 0 and f a = f 1 (a 0 ). This is enough to disable argument congruence; for example, {f ≈ g, f a ≈ g a} is unsatisfiable, whereas its encoding {f 0 ≈ g 0 , f 1 (a 0 ) ≈ g 1 (a 0 )} is satisfiable. For clauses built from fully applied ground terms, the two logics are isomorphic, as we would expect from a graceful generalization.

Given a signature Σ in the ceiling logic, we define a signature Σ ↓ in the floor logic as follows. For each higher-order type τ, we introduce an atomic type τ in the floor logic. For each symbol f : τk

⇒ τ k+1 → • • • → τ n → υ in Σ, where υ is atomic, we introduce symbols f m : τm ⇒ τ m+1 → • • • → τ n → υ for m ∈ {k, .
. . , n}. The translation of ground terms is given by f(ū k ) u k+1 . . . u m = f m ( ūm ). We extend this mapping to literals and clauses by applying it to each side of a literal and to each literal of a clause. Using , the clause order can be transferred to the floor logic by defining t s as equivalent to t s . The property that on clauses is the multiset extension of on literals, which in turn is the multiset extension of on terms, is maintained because maps the multiset representations elementwise. Crucially, argument subterms in the ceiling logic correspond to argument subterms in the floor logic, whereas non-argument subterms in the ceiling logic are not subterms at all in the floor logic. Well-foundedness, totality on ground terms, compatibility with all contexts, and the subterm property hold for in the floor logic.

In standard superposition, redundancy relies on the entailment relation |= on ground clauses. We define redundancy of ceiling clauses in the same way, but using the floor logic's entailment relation: A ground ceiling clause C is redundant with respect to a set of ceiling ground clauses N if C is entailed by clauses from N that are smaller than C . This notion of redundancy gracefully generalizes the first-order notion without making all ARGCONG inferences redundant.

For SUP, EQFACT, and EQRES, we can use the more precise notion of redundancy of inferences instead of redundancy of clauses, a ground inference being redundant if the conclusion follows from existing clauses that are smaller than the largest premise. For ARGCONG and POSEXT, we must use redundancy of clauses.

Skolemization

A problem expressed in λ-free higher-order logic must be transformed into clausal normal form before the calculi can be applied. This process works as in the first-order case, except for skolemization. The issue is that skolemization, when performed naively, is unsound for λ-free higher-order logic with a Henkin semantics. For example, given f : τ → υ, the formula (∀y. ∃x. f x ≈ y) ∧ (∀z. f (z a) ≈ a) has a model with U τ = U υ that interprets f as the identity function and ensures that none of the functions in the image of E υ,τ map J (a) to J (a).Yet, naive skolemization would yield the clause set {f (sk y) ≈ y, f (z a) ≈ a}, whose unsatisfiability can be shown by taking y := a and z := sk. The crux of the issue is that sk denotes a new function that can be used to instantiate z.

Inspired by Miller [28, Section 6], we adapt skolemization as follows. An existentially quantified variable x : τ in a context with universally quantified variables xn of types τn is replaced by a fresh symbol sk : τn ⇒ τ applied to the tuple xn . For the example above, we obtain {f (sk(y)) ≈ y, f (z a) ≈ a}. Syntactically, z cannot be instantiated by sk, which is not even a term. Semantically, the clause set is satisfiable because we can have J (sk)(J (a)) = J (a) even if the image of E τ,τ contains no such function.

Refutational Completeness

The proof of refutational completeness of the four calculi introduced in Section 3.1 follows the same general idea as for standard superposition [START_REF] Bachmair | Rewrite-based equational theorem proving with selection and simplification[END_REF][START_REF] Waldmann | Automated reasoning II. Lecture notes[END_REF]. Given a clause set N ⊥ saturated up to redundancy, we construct a term rewriting system R based on the set of ground instances G Σ (N). From R, we define an interpretation. We show, by induction on the clause order, that this interpretation is a model of G Σ (N) and hence of N.

To circumvent the term order's potential nonmonotonicity, our SUP inference rule only considers the argument subterms u of a maximal term s u . This is reflected in our proof by the reliance of the floor logic from Section 3.3. In that logic, the equation g 0 ≈ f 0 cannot be used directly to rewrite the clause g 1 (a 0 ) ≈ f 1 (a 0 ); instead, we first need to apply ARGCONG to derive g 1 (x) ≈ f 1 (x) and then use that equation. The floor logic is a device that enables us to reuse the traditional model construction almost verbatim, including its reliance on a first-order term rewriting system.

Following the traditional proof, we obtain a model of G Σ (N) . Since N is saturated up to redundancy with respect to ARGCONG, the model G Σ (N) can easily be turned into a model of G Σ (N) by conflating the interpretations of the members f k , . . . , f n of a same symbol family. For this section, we fix a set N ⊥ of λ-free higher-order clauses that is saturated up to redundancy. For the purifying calculi, we additionally require that all clauses in N are purified. To avoid empty Herbrand universes, we assume that the signature Σ contains, for each type τ, a symbol of type τ.

Candidate Interpretation

The construction of the candidate interpretation is as in the first-order proof, except that it is based on G Σ (N) . We first define sets of rewrite rules E C and R C for all C ∈ G Σ (N) by induction. Assume that E D has already been defined for all D ∈ G Σ (N)

with D ≺ C. Then R C = D≺C E D . Let E C = {s → t} if the following conditions are met: (a) C = C ∨ s ≈ t; (b) s ≈ t is strictly maximal in C; (c) s t; (d) C is false in R C ; (e) C is false in R C ∪ {s → t}; and (f) s is irreducible with respect to R C . Otherwise, E C = / 0. Finally, R ∞ = D E D . A rewrite system R defines an interpretation T / 0 Σ /R such that for every ground equation s ≈ t, we have T / 0 Σ /R |= s ≈ t if and only if s ↔ * R t.
Moreover, T / 0 Σ /R is term-generated. To lighten notation, we will write R to refer to both the term rewriting system R and the interpretation T / 0 Σ /R.

Lifting Lemmas

Following Waldmann's version of the first-order proof [START_REF] Waldmann | Automated reasoning II. Lecture notes[END_REF], we proceed by lifting inferences from the ground to the nonground level. We also need to lift ARGCONG. A complication that arises when lifting purifying inferences is that the nonground conclusions may contain purification literals (corresponding to applied variables) not present in the ground conclusions. Given an inference I of the form C pure(E), we refer to the ground instances of C E as ground instances of I up to purification.

Lemma 2 (Lifting of non-SUP inferences). Let Cθ ∈ G Σ (N), where θ is a substitution and the selected literals in C ∈ N correspond to those in Cθ. Then every EQRES or EQFACT inference from Cθ and every ground instance of an ARGCONG inference from Cθ is a ground instance of an inference from C up to purification.

The conditions of the lifting lemma for SUP differ slightly from the first-order version. For standard superposition, the lemma applies if the superposed term is not at or under a variable. This condition is replaced by the following criterion. Definition 3. We call a ground SUP inference from Dθ and Cθ liftable if the superposed subterm in Cθ is not under a variable in C and the correponding variable condition holds for D and C. Lemma 4 (Lifting of SUP inferences). Let Dθ,Cθ ∈ G Σ (N) where the selected literals in D ∈ N and C ∈ N correspond to those in Dθ and Cθ, respectively. Then every liftable SUP inference between Dθ and Cθ is a ground instance of a SUP inference from D and C up to purification.

Main Result

The candidate interpretation R ∞ is a model of G Σ (N) . Like in the first-order proof, this is shown by induction on the clause order. For the induction step, we fix some clause Cθ ∈ G Σ (N) and assume that all smaller clauses are true in R Cθ . We distinguish several cases, most of which amount to showing that Cθ can be used in a certain inference. Then we deduce that Cθ is true in R Cθ to complete the induction step.

The next two lemmas are slightly adapted from the first-order proof. The justification for Lemma 5, about liftable inferences, is essentially as in the first-order case. The proof of Lemma 6, about nonliftable inferences, is more problematic. The standard argument involves defining a substitution θ such that Cθ and Cθ are equivalent and Cθ ≺ Cθ. But due to nonmonotonicity, we might have Cθ Cθ, blocking the application of the induction hypothesis. This is where the variable conditions, purification, and the POSEXT rule come into play. Using these two lemmas, the induction argument works as in the first-order case.

Lemma 7 (Model construction). Let Cθ ∈ G Σ (N) . We have

(i) E Cθ = / 0 if and only if R Cθ |= Cθ ; (ii) if Cθ is redundant with respect to G Σ (N), then R Cθ |= Cθ ; (iii) Cθ is true in R ∞ and in R D for every D ∈ G Σ (N) with D Cθ ; and (iv) if Cθ has selected literals, then R Cθ |= Cθ . Given a model R ∞ of G Σ (N) , we construct a model R ↑ ∞ of G Σ (N).
The key properties are that R ∞ is term-generated and that the interpretations of the members f k , . . . , f n of a same symbol family behave in the same way.

Lemma 8 (Argument congruence). For all ground terms f m ( s) and

g n ( t ), if f m ( s) ξ R ∞ = g n ( t ) ξ R ∞ , then f m+1 ( s, u) ξ R ∞ = g n+1 ( t, u) ξ R ∞ for all u.
The proof relies on the saturation of N up to redundancy with respect to ARGCONG.

Definition 9. Define an interpretation R ↑ ∞ = (U ↑ , E ↑ , J ↑ ) in the ceiling logic as fol- lows. Let (U, E, J ) = R ∞ . Let U ↑ τ = U τ and J ↑ (f) = J (f k ),
where k is the number of mandatory arguments of f. Since R ∞ is term-generated, for every a ∈ U τ→υ , there exists a ground term s :

τ → υ such that s ξ R ∞ = a. Without loss of generality, we write s = f( sk ) s k+1 . . . s m . Then we have a = f m ( sm ) ξ R ∞ and define E ↑ by E ↑ τ,υ (a)(b) = J (f m+1 )( sm ξ R ∞ , b) for all b ∈ U τ It follows that E ↑ τ,υ (a) u ξ R ∞ = f m+1 ( sm , u) ξ R ∞ for any term u. This interpreta-
tion is well defined if the definition of E ↑ does not depend on the choice of the ground term s. To show this, we assume that there exists another ground term t = g( tl ) t l+1 . . .

t n such that t ξ R ∞ = a. By Lemma 8, it follows from s ξ R ∞ = t ξ R ∞ that f m+1 ( sm , u) ξ R ∞ = g n+1 ( tn , u) ξ R ∞
indicating that the definition of E ↑ is independent of the choice of s.

Since R ∞ is a term-generated model of G Σ (N) , we can show that R ↑ ∞ is also termgenerated. And using the same argument as in the first-order proof, we can lift this result to nonground clauses. For the extensional variants, we also need to show that R ↑ ∞ is an extensional interpretation.

Lemma 10 (Model transfer to ceiling logic). R ↑ ∞ is a term-generated model of G Σ (N).

Lemma 11 (Model transfer to nonground clauses). R ↑

∞ is a model of N. Lemma 12 (Completeness of the extensionality axioms). If N contains the extensionality axioms, R ↑ ∞ is extensional. We summarize the results of this section in the following theorem.

Theorem 13 (Refutational completeness). Let N be a clause set that is saturated by any of the four calculi, up to redundancy. For the purifying calculi, we additionally assume that all clauses in N are purified. Then N has a model if and only if ⊥ / ∈ N. Such a model is extensional if N contains the extensionality axioms.

Implementation

Zipperposition [START_REF] Cruanes | Extending Superposition with Integer Arithmetic, Structural Induction, and Beyond[END_REF][START_REF] Cruanes | Superposition with structural induction[END_REF] is an open source superposition-based theorem prover written in OCaml. 1 It was initially designed for polymorphic first-order logic with equality, as embodied by TPTP TFF [START_REF] Blanchette | TFF1: The TPTP typed first-order form with rank-1 polymorphism[END_REF]. We will refer to this implementation as Zipperposition's first-order mode. Recently, we extended the prover with a pragmatic higher-order mode with support for λ-abstractions and extensionality, without any completeness guarantees. Using this mode, Zipperposition entered the 2017 edition of the CADE ATP System Competition [START_REF] Sutcliffe | The CADE-26 automated theorem proving system competition-CASC-26[END_REF]. We have now also implemented a complete λ-free higher-order mode based on the four calculi described in this paper, extended with polymorphism.

The pragmatic higher-order mode provided a convenient basis to implement our calculi. It includes higher-order term and type representations and orders. Its ad hoc calculus extensions are similar to our calculi. Notably, they include an ARGCONG rule and a POSEXT-like rule, and SUP inferences are performed only at argument subterms. In the term indexes, which are imperfect (overapproximating), terms whose heads are applied variables and λ-abstractions are treated as fresh variables. This could be further optimized to reduce the number of unification candidates.

To implement the λ-free mode, we restricted the unification algorithm to non-λterms, and we added support for mandatory arguments to make skolemization sound, by associating the number of mandatory arguments to each symbol and incorporating this number in the unification algorithm. To satisfy the requirements on selection, we avoid selecting literals that contain higher-order variables. Finally, we disabled rewriting of non-argument subterms to comply with our redundancy notion.

For the purifying calculi, we implemented purification as a simplification rule. This ensures that it is applied aggressively on all clauses, whether initial clauses from the problem or clauses produced during saturation, before any inferences are performed.

For the nonpurifying calculi, we added the possibility to perform SUP inferences at variable positions. This means that variables must be indexed as well. In addition, we modified the variable condition. However, it is in general impossible to decide whether there exists a ground substitution θ with tσθ t σθ and Cσθ ≺ C σθ. We overapproximate the condition as follows: (1) check whether x appears with different arguments in the clause C; (2) use an order-specific algorithm (for LPO and KBO) to determine whether there might exist a ground substitution θ and terms ū such that tσθ t σθ and tσθ ū ≺ t σθ ū; and (3) check whether Cσ C σ. If these three conditions apply, we conclude that there might exist a ground substitution θ witnessing nonmonotonicity.

For the extensional calculi, we added a single extensionality axiom based on a polymorphic symbol diff : ∀α β. (α → β) 2 ⇒ α. To curb the explosion associated with extensionality, this axiom and all clauses derived from it are penalized by the clause selection heuristic. We also added a negative extensionality rule that resembles Vampire's [START_REF] Gupta | Extensional crisis and proving identity[END_REF].

Using Zipperposition, we can quantify the disadvantage of the applicative encoding on the problem given at the end of Section 3.2. Well-chosen LPO and KBO instances allow Zipperposition to derive ⊥ in 4 iterations of the prover's main loop and 0.04 s. KBO or LPO with default settings needs 203 iterations and 0.5 s, whereas KBO or LPO on the applicatively encoded problem needs 203 iterations and almost 2 s.

Evaluation

We evaluated Zipperposition's implementation of our four calculi on TPTP benchmarks. We compare them with Zipperposition's first-order mode on the applicative encoding with and without the extensionality axiom. Our experimental data is available online. 2 Since the present work is only a stepping stone towards a prover for full higher-order logic, it is too early to compare this prototype to state-of-the-art higherorder provers that support a stronger logic.

We instantiated all variants with LPO [START_REF] Blanchette | A lambda-free higher-order recursive path order[END_REF] (which is nonmonotonic) and KBO [START_REF] Becker | A transfinite Knuth-Bendix order for lambda-free higher-order terms[END_REF] without argument coefficients (which is monotonic). This gives us a rough indication of the cost of nonmonotonicity. However, when using a monotonic order, it may be more efficient (and also refutationally complete) to superpose at non-argument subterms directly instead of relying on the ARGCONG rule.

We collected 671 first-order problems in TFF format and 1114 higher-order problems in THF, both groups containing monomorphic and polymorphic problems. We excluded all problems containing λ-expressions, the quantifier constants !! (∀) and ?? (∃), arithmetic types, or the $distinct predicate, as well as problems that mix Booleans and terms. Figures 1 and2 summarize, for various configurations, the number of solved satisfiable and unsatisfiable problems within 300 s. The average time and number of main loop iterations are computed over the problems that all configurations for the respective logic and term order found to be unsatisfiable within the timeout. The evaluation was carried out on StarExec [START_REF] Stump | StarExec: A cross-community infrastructure for logic solving[END_REF] using Intel Xeon E5-2609 0 CPUs clocked at 2.40 GHz.

Our approach targets large, mildly higher-order problems-a practically relevant class of problems that is underrepresented in the TPTP library. The experimental results confirm that our calculi handle first-order problems gracefully. Even the extensional calculi, which include (graceless) extensionality axioms, are almost as effective as the first-order mode. This indicates that our calculi will perform well on mildly higherorder problems, too, where the proving effort is dominated by first-order reasoning. In contrast, the applicative encoding is comparatively inefficient on problems that are already first-order. For LPO, the success rate drops by 16%-18%; for both orders, the average time to show unsatisfiability roughly quadruples.

Many of the higher-order problems in the TPTP library are satisfiable for our λ-free logic, even though they may be unsatisfiable for full higher-order logic and labeled as such in the TPTP. This is a reason why we postpone a comparison with state-of-the-art higher-order provers until we have developed a prover for full higher-order logic. On higher-order problems, the nonpurifying calculi outperform their purifying relatives. The comparison of the applicative enconding and the nonpurifying calculi, however, is not entirely conclusive. In the light of the results of this evaluation, in future work, we would like to collect benchmarks for large, mildly higher-order problems and to investigate whether we can weaken the selection restrictions of our calculi.

The nonpurifying calculi perform slightly better with KBO than with LPO. This confirms our expectations, given that KBO is generally considered the more robust default option for superposition and that the nonmonotonic LPO triggers SUP inferences at variable positions-which is the price to pay for nonmonotonicity.

Many researchers have proposed or used encodings of higher-order logic constructs into first-order logic, including Robinson [START_REF] Robinson | A note on mechanizing higher order logic[END_REF], Kerber [START_REF] Kerber | How to prove higher order theorems in first order logic[END_REF], Dowek et al. [START_REF] Dowek | Higher-order unification via explicit substitutions (extended abstract)[END_REF], Meng and Paulson [START_REF] Meng | Translating higher-order clauses to first-order clauses[END_REF], and Czajka [START_REF] Czajka | Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions[END_REF]. Encodings of types, such as those by Bobot and Paskevich [START_REF] Bobot | Expressing polymorphic types in a many-sorted language[END_REF] and Blanchette et al. [START_REF] Blanchette | Encoding monomorphic and polymorphic types[END_REF], are also crucial to obtain a sound encoding of higher-order logic. These ideas are implemented in proof assistant tools such as HOLy-Hammer and Sledgehammer [START_REF] Blanchette | Hammering towards QED[END_REF].

Another line of research has focused on the development of automated proof procedures for higher-order logic. Robinson's [START_REF] Robinson | Mechanizing higher order logic[END_REF] and Huet's [START_REF] Huet | A mechanization of type theory[END_REF] pioneering work stands out. Andrews [START_REF] Andrews | Classical type theory[END_REF] and Benzmüller and Miller [START_REF] Benzmüller | Automation of higher-order logic[END_REF] provide excellent surveys. The competitive higher-order automatic theorem provers include LEO-II [START_REF] Benzmüller | LEO-II-A cooperative automatic theorem prover for higher-order logic[END_REF] (based on unordered paramodulation), Satallax [START_REF] Brown | Satallax: An automatic higher-order prover[END_REF] (based on a tableau calculus and a SAT solver), Agsy-HOL [START_REF] Lindblad | A focused sequent calculus for higher-order logic[END_REF] (based on a focused sequent calculus and a generic narrowing engine), and Leo-III [START_REF] Steen | The higher-order prover Leo-III[END_REF] (based on a pragmatic extension of superposition with no completeness guarantees). The Isabelle proof assistant [START_REF] Nipkow | Isabelle/HOL: A Proof Assistant for Higher-Order Logic[END_REF] and its Sledgehammer subsystem also participate in the higher-order division of the CADE ATP System Competition [START_REF] Sutcliffe | The CADE-26 automated theorem proving system competition-CASC-26[END_REF].

Zipperposition is a convenient vehicle for experimenting and prototyping because it is easier to understand and modify than highly-optimized C or C++ provers. Our middle-term goal is to design higher-order superposition calculi, implement them in state-of-the-art provers such as E [START_REF] Schulz | System description: E 1.8[END_REF], SPASS [START_REF] Weidenbach | SPASS version 3.5[END_REF], and Vampire [START_REF] Kovács | First-order theorem proving and Vampire[END_REF], and integrate these in proof assistants to provide a high level of automation. With its stratified architecture, Otter-λ [START_REF] Beeson | Lambda logic[END_REF] is perhaps the closest to what we are aiming at, but it is limited to second-order logic and offers no completeness guarantees. In preliminary work supervised by Blanchette and Schulz, Vukmirović [START_REF] Vukmirović | Implementation of Lambda-Free Higher-Order Superposition[END_REF] has generalized E's data structures and algorithms to λ-free higher-order logic, assuming a monotonic KBO [START_REF] Becker | A transfinite Knuth-Bendix order for lambda-free higher-order terms[END_REF].

Conclusion

We presented four superposition calculi for intensional and extensional λ-free higherorder logic and proved them refutationally complete. The calculi nicely generalize standard superposition and are compatible with our λ-free higher-order LPO and KBO. Our experiments partly confirm what one would naturally expect: that native support for partial application and applied variables outperforms the applicative encoding.

The new calculi reduce the gap between proof assistants based on higher-order logic and superposition provers. We can use them to reason about arbitrary higher-order problems by axiomatizing suitable combinators. But perhaps more importantly, they appear promising as a stepping stone towards complete, highly efficient automatic theorem provers for full higher-order logic.

Lemma 5 .Lemma 6 .

 56 Let Dθ,Cθ ∈ G Σ (N), where the selected literals in D ∈ N and in C ∈ N correspond to those in Dθ and Cθ, respectively. We consider a liftable SUP inference from Dθ and Cθ or an EQRES or EQFACT inference from Cθ. Let E be the conclusion. Assume that Cθ and Dθ are nonredundant with respect to G Σ (N). Then E is entailed by clauses from G Σ (N) that are smaller than Cθ . Let Dθ,Cθ ∈ G Σ (N), where the selected literals in D ∈ N and in C ∈ N correspond to those in Dθ and Cθ, respectively. We consider a nonliftable SUP inference from Dθ and Cθ. Assume that Cθ and Dθ are nonredundant with respect to G Σ (N). Let D θ be the clause Dθ without the literal involved in the inference. Then Cθ is entailed by ¬ D θ and the clauses in G Σ (N) that are smaller than Cθ .

https://github.com/c-cube/zipperposition

http://matryoshka.gforge.inria.fr/pubs/lfhosup _ data/

Acknowledgment. We are grateful to the maintainers of StarExec for letting us use their service. We want to thank Christoph Benzmüller, Sander Dahmen, Johannes Hölzl, Anders Schlichtkrull, Stephan Schulz, Alexander Steen, Geoff Sutcliffe, Andrei Voronkov, Petar Vukmirović, Daniel Wand, Christoph Weidenbach, and the participants in the 2017 Dagstuhl Seminar on Deduction beyond First-Order Logic for stimulating discussions. We also want to thank Mark Summerfield, Sophie Tourret, and the anonymous reviewers for suggesting several textual improvements to this paper and to the technical report. Bentkamp and Blanchette's research 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).

Our calculi join a long list of extensions and refinements of superposition. Among the most closely related is Peltier's [START_REF] Peltier | A variant of the superposition calculus[END_REF] Isabelle formalization of the refutational completeness of a superposition calculus that operates on λ-free higher-order terms and that is parameterized by a monotonic term order. Extensions with polymorphism and induction, developed by Cruanes [START_REF] Cruanes | Extending Superposition with Integer Arithmetic, Structural Induction, and Beyond[END_REF][START_REF] Cruanes | Superposition with structural induction[END_REF] and Wand [START_REF] Wand | Superposition: Types and Polymorphism[END_REF], contribute to increasing the power of automatic provers. Detection of inconsistencies in axioms, as suggested by Schulz et al. [START_REF] Schulz | Detecting inconsistencies in large firstorder knowledge bases[END_REF], is important for large axiomatizations. Also of interest is Bofill and Rubio's [START_REF] Bofill | Paramodulation with non-monotonic orderings and simplification[END_REF] integration of nonmonotonic orders in ordered paramodulation, a precursor of superposition. Their work is a veritable tour de force, but it is also highly complicated and restricted to ordered paramodulation. Lack of compatibility with arguments being a mild form of nonmonotonicity, it seemed preferable to start with superposition, enrich it with an ARGCONG rule, and tune the side conditions until we obtained a complete calculus. Most complications can be avoided by using a monotonic order such as KBO without argument coefficients, but we suspect that the coefficients will play an important role to support λ-abstractions. For example, the term λx. x + x could be treated as a constant with a coefficient of 2 on its argument and a heavy weight to ensure (λx. x+ x) y y+y. LPO can also be used to good effect. This technique could allow provers to perform aggressive β-reduction in the vast majority of cases, without compromising completeness.


Matteo Gaeta
email: gaeta@crmpa.unisa.it

Pierluigi Ritrovato
email: ritrovato@crmpa.unisa.it

Saverio Salerno
email: salerno@unisa.it

ELeGI: The Europen Learning Grid Infrastructure ELeGI The European Learning Grid Infrastructure

Keywords: Grid Architecture, GRID infrastructure, Complex Problem Solving and Grid applications, technology enhanced learning

The purpose of this paper is to describe the ELeGI Project1. ELeGI has the ambitious goal of developing software technologies for effective human learning and promoting and supporting a learning paradigm shift. A new paradigm focused on knowledge construction using experiential based and collaborative learning approaches in a contextualised, personalised and ubiquitous way will replace the current information transfer paradigm focused on content and on the key authoritative figure of the teacher who provides information. We have chosen a synergic approach, sometimes called "human centred design", to replace the classical, applicative approach to learning. With consideration of humans at the centre, learning is clearly a social, constructive phenomenon. It occurs as a side effect of interactions, conversations and enhanced presence in dynamic Virtual Communities: experimental research concepts integrating new powerful developments of services in the Semantic GRID, the leading edge of currently available and future ICT technologies, with highly innovative and powerfully significant scenarios of human learning.

PROJECT OBJECTIVES Project Vision: Advancing Technology Enhanced Learning in Europe

The overall aim of the project is to radically advance the effective use of technology-enhanced learning in Europe through the design, implementation and validation of a pedagogy-driven, service-oriented software architecture based on GRID technologies for supporting ubiquitous, collaborative, experiential-based, contextualised and personalised learning. Previous projects that have set out to improve learning through novel technologies have often failed to leave any significant mark because they did not give priority to the social, economic and technical perspectives of the key human actors. So, while the development and use of appropriate technology must be pedagogically driven, at the same time those involved in the formulation and evaluation of pedagogy must be made aware of, and shown by demonstration, state-of-the-art technological possibilities. We address this pervasive learning issue by explicitly listing the roles that actors play in the learning process and illustrate with reference to future learning scenarios. This provides us with a focus for formulating requirements in terms of didactical models, learning resources, services, quality of service, and usability for end-users. It also provides a clear reference for the technical context of the project -an open and flexible software architecture for creating learning environments that accommodate the roles implied by the new learning possibilities and that demonstrate state-of-the-art technologyenhanced learning.

PEDAGOGICAL GOALS AND NEW LEARNING MODES

In order to support the implementation of new learning modes related to ubiquitous, collaborative, experiential, contextualised and personalised learning, it is necessary to promote a paradigm shift in the general approach to teaching and learning.

Currently, teaching and learning practices are based mainly on the information transfer paradigm. This focuses on content, and on the key authoritative figure of the teacher that provides information. Teachers' efforts are mainly devoted to find the best way for presenting content in order to transmit information to learners. This "productteaching oriented view" finds its perfect technical mirror in the "page oriented approach to the Web" where the goal is to produce more and "better" static pages for the consumption of interested students. Learning is then considered to be an activity which helps teachers to produce, and students to consume, multimedia books on the Web. This paradigm has been popular in earlier e-Learning projects, not because it is effective, but because it is easy to implement with basic Internet facilities and it does not require any change in the traditional roles of the actors.

The information transfer paradigm is well understood and well supported by existing e-Learning practice. In order to advance effective learning we will promote another paradigm that focuses on the learner and on new forms of learning. In our approach the learner has an active and central role in the learning process. Learning activities are aimed at facilitating the construction of knowledge and skills in the learner, instead of the memorisation of information. Information transfer will still obviously exist in the new paradigm, but only as a simple component, not the main goal. Accordingly we can say that the new paradigm subsumes the old one in its displacement. Knowledge construction occurs through new forms of learning based on:

• the understanding of concepts through direct experience of their manifestation in realistic contexts (i.e.

providing access to real world data) which are constructed from sophisticated software interfaces and devices, and represented as services;

• "social learning" -active collaboration with other students, teachers, tutors, experts or, in general, available human peers, by using different kinds of collaboration technologies, including enhanced presence.

In this approach collaboration is considered as a complex conversational process that goes far beyond a simple information exchange. In order to support such a "ubiquitous conversational process", one must consider the social context where the learning process occurs. Accordingly we do not consider the learner's ability in an abstract way, but relate it to a specific situation (the context). In this ambit the term "ubiquitous" does not refer simply to "anytime / anywhere", but more generally to the ability to support multiple diverse learning contexts and automatically adapt to them.

As we consider human learning as a social process, collaboration implies community membership, it means working together, providing added value, sharing and executing tasks in order to reach a common goal. Learning is no longer an isolated activity -it implies mutual trust, shared interests, common goals, commitments, obligations, exchanging of services, a genuinely proactive, motivated behaviour.

In order to foster these new approaches to learning we will create dynamic contexts where the learner "achieves" knowledge and skills in an active way instead of simply storing information. Communities will have the right to identify their goals, in terms of knowledge and skills to be acquired, instead of just asking an authority to define a curriculum for them. Goals will therefore genuinely correspond to needs, and be highly dependent on the local culture and its priorities.

According to this new learning paradigm we consider realism as the cornerstone of the learning environment. For example, highly realistic virtual scientific experiments have only recently become possible through use of advanced technology. Innovative aspects include the definition of a standard didactical model for the achievement and representation of such experiments. In this type of model a learner is immersed in a specific context, which through appropriate simulations, develops active learning processes with progressive abstraction levels, leading to the construction of their knowledge in a dynamic way. In this learning mode the student can also receive the support of the other users (collaborative aspects) and from the comparison with them, they can build a new "mediated" knowledge.

To complement this freedom in knowledge construction, we allow the definition of personalised and individualised learning paths. This means that in a specific context we need, from one side, to create learning conditions that are adequate for a learner's preferences (individualised learning) and, from the other, guarantee that the learner will reach a cognitive excellence through different learning paths according to their skills and knowledge. Accordingly, we will study and define specific models for representing knowledge that takes the learners preferred learning styles into account. A beneficial result of allowing learners the right to construct their own knowledge is that richer GRID Infrastructure to support future technology enhanced Learning and more diversified learning contexts can arise, necessitating the dynamic integration of different kinds of information and communication technologies. The dynamics of intertwined, controlled and secure construction and use of subsequent versions of our systems, by skilled as well as unskilled human actors, and of the services enabling them, constitutes our methodological approach for successful adaptive technology-enhanced solutions.

MEETING THE TECHNICAL CHALLENGE: THE GRID TECHNOLOGY

In order to support ubiquitous, collaborative, experiential and contextualised learning in dynamic virtual communities a learning environment should provide the following features for learners:

• Collaboration; Socio-constructivist: group working should be routinely supported as well as the more traditional model of the solitary learner -this includes support for self-organising online communities who share common educational goals • Experiential; Active Learning: learning resources should be interactive, engaging, and responsive -active learning and knowledge formation should be emphasised above simple information transfer • Realism: real-world input should be easy to incorporate, as should simulations, ranging from simple interactive animations to immersive VR • Personalised: students should find themselves at the centre of their online environment, with their individual needs addressed -the quality of the learning experience should be continually validated and evaluated • Ubiquity and accessibility:

• wider, more flexible access to educational resources should be provided, often referred to as "anytime/anywhere" learning. • multiple different types of devices, interfaces, and network connection types should be supported where possible • Contextualised; Adaptive: appropriate learning contexts may be naturally be short-lived, as well as the more traditional static situations such as the classroom and the library -this calls for dynamicity in the creation of contexts

The pedagogical goals outlined above have highly demanding technical requirements, many of which are also the concerns of distributed systems research. Group working implies shared interactive resources, necessitating both concurrency control and awareness of others activities. Active learning requires interactive resources, many of which will only be engaging if they are suitably responsive -a quality of service (QoS) issue that depends on many components of a distributed system -the low-level infrastructure (hardware, OS, network), the middleware and the interface software. Concurrency control and interactive responsiveness can make conflicting demands on a system. Real world input, such as live stock market prices, or remote sensing data, makes a network connection mandatory, and this again raises QoS issues such as fault detection, masking and tolerance for the learning environment. Accessibility, as in anytime/anywhere, requires availability, which may be supported through replication of resources, but this creates further tensions with responsiveness and concurrency control due to the need to maintain state across replicas. Accessibility also means adapting to available capabilities. For example: can the same learning environment be delivered through low-bandwidth mobile devices and high-bandwidth multimedia workstations? Accessibility also means supporting special needs of the individual, such as disabilities. More generally, the individual user should be recognised and catered for, and this personalisation requires semantic tagging and profiling that can be difficult to formulate, both conceptually and in terms of machine representation. Standards efforts have been particularly slow in addressing this problem. Finally, contextualisation requires a move from the traditional view of an online learning environment as a stable long-lived entity (e.g. during the lifetime of a teaching module) -to one where the environment may evolve and change much more frequently, perhaps even several times a day -a dynamicity that is alien to current e-Learning products.

We believe that these technical requirements can best be addressed by building on the open distributed service model that has evolved as part of the Grid -why start from scratch if there is already a suitable and established base? The Grid a consolidation of selected distributed systems research output from the last twenty years. The Grid was originally designed for e-Science and was primarily concerned with supercomputing applications, but the framework it engendered to realise effective sharing of distributed heterogeneous resources (OGSA: the Open Grid Services Architecture) is now being applied to many other areas, especially enterprise computing and e-Commerce. Reciprocally, by progressing Grid technologies for learning, we will also contribute towards the advancement of the open Grid service model itself. We see the use of the Grid to support a paradigm shift in pedagogy to advance effective learning as a natural step in the recent historical progress of technology enhanced learning: Internet -> Web -> Grid.

OGSA leverages open standards including W3C, and provides an holistic view of Grid computing based on the concepts of 'Services', 'Distributed Collaboration' and 'Virtual Organisation'. At this point, new learning scenarios enter the picture: the user-centred, contextualised and experiential based approaches for ubiquitous learning imply the full exploitation of location-transparent access to distributed services such as simulation environments, realworld input, 3D visualisation systems and digital libraries, in the framework of a Virtual Organization. This allows a transition from current content-oriented e-Learning solutions towards a user-centred, collaborative model.

The next generation of Grid solutions will increasingly adopt the service-oriented model for exploiting commodity technologies. Its goal is to enable as well as facilitate the transformation of Information into Knowledge, by humans as well as -progressively -by software agents, providing the electronic underpinning for a global society in business, government, research, science, education and entertainment (semantic aspects) These efforts are sometimes referred to as the "Semantic Grid".

In summary, our proposal seeks to develop an OGSA compliant service oriented software architecture and realise a corresponding prototype infrastructure in order to support effective learning environments which exemplify the new paradigm.

METHODOLOGY: TEST-BEDS AND DEMONSTRATORS

Having described the overall objectives, the pedagogical goals and how we aim to meet the technical challenge, we now outline the methodology for the realisation and validation of ELeGI project. We have selected a particular set of demonstrators and test-beds representing scientific, social, economic and cultural cognate areas that include both formal and informal learning scenarios. The key difference between testbeds and demonstrators is that demonstrators already exist in non-Grid compliant forms, as relatively mature and well understood exemplars of the types of pedagogy ELeGI wishes to support, whereas testbeds are principally new departures, designed to test the ELeGI approach from conception to implementation and evaluation.

Testbeds: Service Elicitation and Exploitation Scenarios

As we are working towards a service-oriented architecture we refer to the test-beds as Service Elicitation and Exploitation Scenarios (SEES). The purpose of the SEES is to develop and gain insight into the processes involved from formulating pedagogic requirements to the implementing environments that meet these requirements. The following SEES, which are described in detail in the RTD section, are planned:

Demonstrators

Demonstrators differ from SEES in that they are based on the advanced prototypes which have adopted approaches congruent with the new paradigm, and where the pedagogical issues are already well understood. The purposes of the demonstrators are: 1) To provide evidence of the benefit coming from the adoption of didactical models based on socio-constructivist contextualised approach and to demonstrate the effectiveness of Grid technologies for implementing these didactical models.

2) to understand the engineering issues involved in implementing/porting existing solutions as OGSA-compliant software and services

3) to configure and customise these environments, for demonstrating effectiveness of specific research aspects 4) To prepare advanced contents for these environments 5) to provide working systems to elicit feedback and provide reference points within the project GRID Infrastructure to support future technology enhanced Learning 6) to act as "demonstrators" in support of publicity, dissemination and training activities

The demonstrators have been selected in order to maximise the benefits of the development work in that there is already a working non-Grid version. The three demonstrators planned are:

• Virtual Scientific Experiments for teaching high level mathematical courses.

• Learning Environment for Accountancy and Business Finance

• Learning Environment for Mechanical Engineering

SUMMARY OF SCIENTIFIC AND TECHNICAL OBJECTIVES

In summary, the project has three major goals. Goal 1. To define new models of human learning enabling ubiquitous and collaborative learning, merging experiential, personalised and contextualised approaches.

Goal 2. To define and implement an advanced service-oriented Grid based software architecture for learning. This will allow us to access and integrate the different technologies, resources and contents that are needed in order to realise the new paradigm. This objective will be driven by the pedagogical needs and by the requirements provided by the test-beds (SEES) and informed by the experience gained through implementing the demonstrators.

Goal 3. To validate and evaluate the software architecture and the didactical approaches through the use of SEES and demonstrators. The project will build extensively on work already done, with the emphasis on creating new environments rather than components.

In order to reach these goals it will pursue the following objectives: OB13. facilitate the exploitation of European cultural and scientific resources though the Learning GRID infrastructure;

PROJECT RESULTS AND THEIR EVALUATION

The project results will be generated and evaluated through the use of the test-beds and demonstrators. The testbeds will evaluate the didactical approaches from cost/benefit and pedagogical points of view, and the support provided by the technology infrastructure in term of QoS, usability, scalability, interoperability and transparency of access to the distributed resources used for realising the didactical approaches. The Demonstrators will be used for stimulating the final users and the learning community in general about the potentialities offered by the realisation of a pedagogical driven service-oriented software architecture based on GRID technology (ELeGI) In summary, the main ELeGI project results will be:

RS1. The service oriented GRID based Software Architecture;

RS2. Formalisation of didactical models for the new learning approaches;

RS3. Methodologies for evaluating the effectiveness of these new learning approaches from the pedagogical and usability points of view;

RS4. Methodologies and techniques for representing knowledge and for allowing personalised, individualised and collaborative learning;

RS5. Strategies for leading learning organisations and actors in the learning process to actualise the paradigm shift in learning approaches;

RS6. Prototypes for demonstrating the potentialities offered by the ELeGI technologies and methodologies;

RS7. New digital content in different contexts to support innovative learning approaches and in particular with respect to virtual scientific experiments;

RS8. Methodologies and techniques for making existing applications Grid-aware;

RS9. ELeGI evaluation and experimentation feedbacks; RS10. Contribution to the technical standards in the Learning, semantic Web, and Grid domains;

RS11. Workshops, Conferences, Publications, Information Web sites, and Demonstrator Web sites for disseminating project results.

INNOVATION RELATED ACTIVITIES

According to the objectives sections the innovations that will be introduced with the ELeGI proposal can be classified in two different, but interrelated and objective-driven main groups. The first group is related to the pedagogical aspects the second group to the technology aspects. The essence of innovations for pedagogical aspects is that in order to fully exploit e-learning processes we can not simply make the electronic transposition of traditional learning model. We need to investigate and define appropriate didactical models for e-learning. These models, based mainly on contextualised, experiential based and personalised approaches (socio-constructivist vision), will be defined taking into account in a synergic process both pedagogical and technological aspects fostering a learning paradigm based on socially situated, activitybased knowledge construction rather than information memorisation.

In particular, an innovative aspect is that our model will consider several characters of learning in a unitary approach. In the ELeGI proposal we will focus our attentions on the Active, Situated and Collaborative properties of learning.

• Active means that the learner is the principal actor of the process he/she takes the main decisions he/she learn choosing tools, exploring knowledge bases, accessing to virtual experiments, etc.

• Situated means contextualised with respect to activities motivated by goals, intentions, purposes, plans.

• Collaborative, means that the creation of the knowledge is a collaborative process evolving through interactions with colleagues, teachers, tutors, experts, instruments, etc.

In this frame standard models for experiential based learning will be proposed, in particular with respect to Virtual Scientific Experiments.

Other innovative aspects are related to the possibility to personalise the learning process according to the learners' preferences and styles. In order to allow personalised learning processes we need to study and define methodologies for representing, through adequate knowledge structures (ontologies), and managing knowledge representing both the domain (the learning context) and the learner capabilities and skills itself including the representation of learner's attitudes, flaws as well as possible misunderstandings with respect to concepts and relations among several pieces of information related to a specific learning domain (e.g.: mathematics, physics, sociology, etc.). We are convinced we can now reach these objectives because we have already developed significant, even if quite limited, prototypes that present these features.

Exploiting these advanced knowledge representation structures, it will be possible to introduce innovative intelligent functionalities embedded into to the learning environment, namely the learning GRID infrastructure, realising a first concrete interpretation of the Ambient Intelligence vision in the learning domain.

Innovative will be the approach that we follow for implementing, experimenting and validating this new learning paradigm. Indeed, each and all the research activities will be aimed at satisfying user needs and will be validated through the execution of real size test-beds in an iterative approach, thus using the results as a feed-back as well as a feed-forward for improving and changing the models defined.

It is clear that in order to reach these ambitious objectives we need to design and implement a very powerful technological infrastructure. The widest is the potential learning audience, the most sophisticated should be the technology and, at the same time, the simplest to use. From this point of view the main innovation is the use of GRID technologies for implementing a service oriented software infrastructure. The use of GRID technologies implies the adoption of a framework based approach for designing our infrastructure. This means to raise the level of abstraction in the infrastructure design:

• trying to be as much as possible neutral respect to technological evolutions,

• focusing our attention on the definition of interfaces and behaviours of "learning services" in a standard way and • implementing an infrastructure that will incrementally support the realisation and actualisation of our new learning paradigm.

We are well aware, as we said in previous sections, that for actualising this new learning paradigm we need to integrate and coherently orchestrate several kinds of technologies and existing software solutions in an innovative way.

Investigating and experimenting with the use of GRIDs as technology glue for implementing dynamic service oriented Virtual Learning Organisations (VLO) also introduces potential innovations fed to the technological level: the service elicitation scenarios will continuously feed the technologists with requirements for new services described at the abstraction level of the pedagogy, to be translated into combinations of services at the abstraction level of technologies. The continuous "translation" process from the one to the other abstraction level is exactly the core of the synergies declared as the innovative approach of ELeGI.

Finally, innovations for the GRID technologies strictly connected to support dynamic Virtual Learning Organisations emerge from the study and analysis of semantic, trust & security aspects. In order to implement dynamic VLOs, we need to define mechanism for services discovery as well as to automatically for "understanding" the capabilities of these discovered services. In order to do that, we need to define standards for describing GRID serviced semantically. This is one of the hottest research topics in the GRID domain and we believe that with the ELeGI proposal we can contribute substantially to the progress in this field. Moreover, the exploitation of this semantic enrichment of services will be fundamental for supporting collaboration and interactivity as well as for creating the necessary awareness for implementing a Learning Ambient Intelligent vision.

It is clear that VLOs, due to their dynamic nature, needs policy driven, configurable and powerful security mechanism. Moreover, without security this kind of infrastructure will be confined to the research community and will never be used in the business domain. Grid technologies, at the data level, are mature enough but their introduction is not yet diffused as it may be since work has to be done in order to make GRID technologies usable from a secure point of view.

GRID Infrastructure to support future technology enhanced Learning Conversational processes, enhanced presence and the Semantic Grid are all activities identified in ELeGI and assigned to highly qualified partners, with an outstanding record of excellence in research, both fundamental and applied. The three aspects run together: learning services, the ones needed for enabling effective learning to occur, have to be first identified by means of conversational processes by humans in virtual communities accompanied by enhanced presence in order to keep motivation and commitment to the community's goals high and performing. Identified services have then to be progressively transformed into software, i.e. the semantics of services has to be constructed in order to make an infrastructure that supports those services. It will be vital for the project's success that the life cycle of service identification, design, implementation and exploitation will be understood by each actor in the loop. Looking at the forest of available technologies, anyone is discouraged by the impressive number and complexity of each component, language and device.

THE OVERALL APPROACH

The picture below shows the organisation of the RTD activities and the relations existing among the research activities.

GRID Infrastructure to support future technology enhanced Learning

A 4 years Integrated Project submitted in the 1 st Call of the 6 th Framework Programme -Information Society Technology -of the European Commission. At the time of submission of this paper the project is in the Contract Negotiation phase and should start in January


Luca Stefanutti
email: luca.stefanutti@uni-graz.at

Dietrich Albert
email: dietrich.albert@uni-graz.at

Cord Hockemeyer
email: cord.hockemeyer@uni-graz.at

Derivation of Knowledge Structures for Distributed Learning Objects

Keywords: knowledge structures, knowledge spaces, distributed learning objects, skill maps, knowledge assessment, GRID Technology

Knowledge space theory (Doignon & Falmagne, 1985; Albert & Lukas, 1999; Doignon & Falmagne, 1999) offers a rigorous and efficient formal framework for the construction, validation, and application of eassessment and e-learning adaptive systems. This theory is at the basis of some existing e-learning and e-assessment adaptive systems in the U.S. and in Europe. Such systems are based on a fixed and local domain of knowledge, where fixed means that the domain does not change in time, and local refers to the fact that the items are stored and available locally. In this paper we present some theoretical notes on the efficient construction and application of knowledge spaces for knowledge domains that are both dynamic and distributed in space. This goes in the direction of an exploitation of new technologies like the GRID for building the next generation of learning environments.

INTRODUCTION

Knowledge space theory [START_REF] Doignon | Spaces for the assessment of knowledge[END_REF][START_REF] Albert | Knowledge spaces: theories, empirical research, applications[END_REF][START_REF] Doignon | Knowledge spaces[END_REF] offers a rigorous and efficient formal framework for the construction, validation, and application of e-assessment and elearning adaptive systems. It is mainly a psychometric theory for the assessment of knowledge; however, as adaptivity and optimal learning paths does matter, its methods and models can be fruitfully exploited for e-learning purposes as well.

According to this theory, a domain of knowledge is a collection Q of items (e.g., learning objects, problems, questions, exercises, examples, etc.) in a given field of knowledge (e.g., mathematics, physics, chemistry, biology, etc.). Then, the knowledge state of a student is the set K of all items in that this student actually masters, and a knowledge structure for is a pair in which is the collection of all knowledge states that can be observed in a certain population of students. If is closed under union (i.e., whenever ) then it is called a knowledge space. Sometimes also closure under intersection holds (

Q Q ( K , Q ) K K K ∈ ′ ∪ K K K ∈ ′ K K, K ∈ ′ ∩ K K whenever
), in which case, is called a quasi-ordinal knowledge space.

K ∈ ′ K , K K
The above-mentioned theory is at the basis of some existing e-learning and e-assessment adaptive systems in the U.S. and in Europe. Two of them are the ALEKS (Adaptive LEarning with Knowledge Spaces) system developed by the research group of Irvine, CA supervised by Falmagne (http://www.aleks.com), and the RATH (Relational Adaptive Tutoring Hypertext) system of the research group of Graz, Austria [START_REF] Hockemeyer | RATH ---a relational adaptive tutoring hypertext WWW-environment based on knowledge space theory[END_REF].

Such systems are based on a fixed and local domain of knowledge Q , where fixed means that Q does not change in time, and local refers to the fact that the items are stored and available locally. The original theory, in fact, provides methods of construction of knowledge structures which are based on these two requirements [START_REF] Koppen | How to build a knowledge space by querying an expert[END_REF][START_REF] Dowling | Applying the basis of a knowledge space for controlling the questioning of an expert[END_REF][START_REF] Koppen | Extracting human expertise for constructing knowledge spaces: an algorithm[END_REF]. Later developments of the theory provide some methods of construction for the case of dynamic domains of knowledge (see, e.g., [START_REF] Albert | Adapting knowledge structures in dynamic domains[END_REF][START_REF] Stefanutti | A procedure for the incremental construction of a knowledge space[END_REF]. However, the efficient construction and application of knowledge structures for distributed (thus, non-local) items appears to be still an open question.

New technologies like the GRID provide a promising approach for the construction of and application of e-learning systems [START_REF] Ritrovato | How to use the GRID Technology for building the next generation of learning environments[END_REF]. These technologies are strongly based on the concept of distributed services. In this paper we present some theoretical notes on the efficient construction and application of knowledge spaces for knowledge domains that are both dynamic and distributed in space. This means that the learning objects may reside on different locations and that every location has access to both local and remote learning objects. Moreover, the set (repository) of learning objects in the various locations is assumed to be dynamic in the sense that learning objects may be continuously added to (resp. removed from) the local repositories. At the basis of our approach there is the concept of a distributed skill map, which is the subject of next section.

DISTRIBUTED SKILL MAPS

A skill map [START_REF] Korossy | Modellierung von Wissen als Kompetenz und Performanz [Modeling knowledge as competence and performance[END_REF][START_REF] Doignon | Knowledge spaces and skill assignments[END_REF][START_REF] Düntsch | Skills and knowledge structures[END_REF] is a triplet ( )

A A A S Q A σ , , :=
in which Q is a nonempty set of items (problems, learning objects, exercises, questions, etc.), is a nonempty set of skills, and is a mapping such that

A A S A S A A Q 2 : → σ ( ) ∅ ≠ q A σ for all q A Q ∈ . The interpretation of A σ is the following: for any in , q A Q A ( ) q σ
is the set of all skills that (according to ) are sufficient to solve item .

A q

A knowledge structure can be easily derived from a skill map . By the conjunctive model of Doignon [START_REF] Doignon | Knowledge spaces and skill assignments[END_REF][START_REF] Doignon | Knowledge spaces[END_REF]

, a subset A K of Q is said to be delineated by a subset A T of if and only if A S ( ) ( ) { } T q Q q T K A A A ⊆ ∈ = = σ ϕ : : . ( 1
)
In words, every item in q K is solvable by (some subset of) skills in T , and K contains all such items. It turns out that the collection of all subsets fulfilling (1) is a knowledge structure close both under union and under intersection -i.e., a quasi-ordinal knowledge space.

A Q K ⊆ A distributed skill map is a pair
where D is a collection of skill maps, and " ∨ " (read: "join") is a binary operator such that, given any three skill maps

( ∨ , D ) ( ) A A A S Q A σ , , := , ( ) B B B S Q B σ , , := and C ( ) C C C S Q σ , , := in ,
if and only if

D B A C ∨ = 1. , B A C Q Q Q ∪ = 2. , B A C S S S ∪ = 3. ( ) ( ) ( ) q q q B A C σ σ σ ∪ = for all q . C Q ∈ It is a simple fact that the join of two skill maps is still a skill map. A distributed skill map ( ) ∨ , * D is said to be complete if * D ∈ ∨ B A ) T whenever
. Thus, every complete distributed skill map has a top element

* , D ∈ B A ( T T S Q T σ , , = which is determined by { } * : D ∈ ∨ = A A T
[Note that, from a mathematical point of view, a complete distributed skill map is a complete join semi-lattice in which the join operation is " ∨ ".] It follows that the knowledge structure delineated by a complete distributed skill map ( )

∨ , * D having top element T , is ( ) T κ
where, for any

* D ∈ A , ( ) ( ) { } A A A S T T K Q K A ⊆ = ⊆ = some for : : ϕ κ
, and the fact that ( ) T κ is a quasi-ordinal knowledge space immediately follows from the fact that T is, indeed, a skill map. Moreover, since the join-closure of any distributed skill map ( )

∨ , D is a complete distributed skill map, the knowledge space delineated by D is { } ( ) D ∈ ∨ A A :
κ Thus, a distributed skill map can be seen as a distributed representation of a (quasi-ordinal) knowledge space.

CONSTRUCTION AND RETRIEVAL OF DISTRIBUTED SKILL MAPS

Physically, the elements of a distributed skill map ( ) ∨ , D reside in locations that are separate in space, or they can be produced at different time points. The subset D′ of all elements in D that are accessible to a given user in a specific location is the distributed skill map accessible to that user.

Locally, a skill map

( A A A S Q A ) σ , , := is represented as a collection R of pairs ( ) P q, , where q is an item, is a set of skills such that A Q ∈ A S P ⊆ ( ) P q = A σ
, and is called a local repository of the skill map . To create a local repository one needs to specify the pairs R A ( ) P q, , each of which is a single item (problem, learning object, etc.) with a set of skills 'attached' to it. The only requirement is that the items in a local repository have to be unique (to assure consistency of the mapping A σ ), i.e., for all A Q q ∈ , ( ) ( )

P P P q and P q ′ = ⇒ ∈ ′ ∈ R R , ,
Technically, appropriate metadata schemas have to be defined for the representation of the elements of a local repository (i.e., the pairs ).

( )

P q,

The user is allowed to perform three kinds of operations with local and remote repositories:

1. insert/delete/edit items ( ) P q, in the local repository; 2. retrieve items from the local repository; 3. retrieve items from a remote repository.

Through these three operations the user derives, in fact, a local skill map and -implicitly -a local knowledge space which can then be used for e-learning and/or assessment purposes. Thus, the advantage of distributed skill maps is that the corresponding knowledge structure can be derived locally for the specific subset of items collected by the user.

ASSESSMENT OF THE KNOWLEDGE STATE OF A STUDENT

Given a set Q of items, the knowledge state of a student is the collection K of all items that this student masters.

Here we face the problem of how to determine this collection for a certain student in an efficient way. Knowledge space theory provides procedures for the efficient assessment of the knowledge state of the student provided that an explicit representation of the knowledge space is available to these procedures (see e.g., [START_REF] Falmagne | A class of stochastic procedures for the assessment of knowledge[END_REF].

When the items in are distributed in space the derivation of an explicit knowledge space for turns out to be a rather inefficient approach. To see this, imagine that a user collects a set of elements from different (local or remote) repositories creating, this way, a local skill map

Q Q ( P q, ) ( ) A A A S Q A σ , , :=
(see previous section). To use this skill map for assessing a student with the procedures above-mentioned the user needs to derive the explicit knowledge space corresponding to . This turns out to be a time and space consuming task.

A

At least for quasi-ordinal knowledge spaces, an efficient assessment procedure can be derived which does not require the explicit construction of the knowledge space corresponding to a certain skill map . In this section we provide a sketch of this procedure.

A

First, we define a binary relation " ≤ " on Q such that, for any two items

A A A Q q p ∈ , , ( ) ( )
q p q p A A A σ σ ⊆ ⇔ ≤ .
The interpretation of such a relation is the following: "the fact that a student masters item p can be surmised by the fact that this student masters q " or, equivalently, "the fact that this student does not master can be surmised by the fact that s/he does not master q p ". The introduction of the relation " ≤ " has a clear aim: it is a classical result in lattice theory that there exists a 1-1 correspondence between the quasi-ordinal knowledge spaces on a set Q and the surmise relations for Q [START_REF] Birkhoff | Lattice theory[END_REF].

A

Then we introduce the following notation: for a subset , we denote with

A Q X ⊆ { } X x q x Q q X A A ∈ ≤ ∈ = ↑ some for : :
the up-set of X in the partially ordered set ( )

A A Q ≤ ,
, and with

{ } X x x q Q q X A A ∈ ≤ ∈ = ↓ some for : : the down-set of X in . ( ) A A Q ≤ ,
Suppose now that the knowledge state of a student has to be uncovered through the skill map . This occurs in a stepwise assessment procedure where, in each step the student is presented with a new question and a representation of the knowledge state of the student is updated according to

A Q K ⊆ * A n Q K ⊆ A 0 > n A n Q q ∈
the student's answer. Under the assumption that at the outset ( 0 = n ) there is no prior knowledge about * K , the assessment algorithm is as follows:

∩ A Q q ( ) X Y \ B σ || 0 ← n , , Q ; ∅ ← n K A n Q ← while do: ∅ ≠ n Q choose new item from ; q n Q obtain answer r for from student; q if 1 = r (correct answer) then { } ↓ + ∪ ← q K K n n 1 ; { } ↓ + ← q Q Q n n \ 1 ; else { } ↑ + ← q Q Q n n \ 1 ; end 1 + ← n n ; end
The algorithm sketched above terminates in a finite number of steps

A Q m ≤
and -if no lucky guesses or careless errors occur during the assessment process (see in this connection [START_REF] Falmagne | A class of stochastic procedures for the assessment of knowledge[END_REF]) -the knowledge state of the student is correctly uncovered by the procedure. One note on the efficiency of this procedure is that, especially when

m K K = * A Q is large, the number of steps is expected to be much smaller than m A Q .

VALIDITY OF DISTRIBUTED SKILL MAPS

A skill map is a (formal) cognitive model which specifies the skills underlying a certain set of items. As a model it is a hypothetical representation of the relation between items and skills and it needs to be validated. A first step of validity is reliability. The different skill maps in a distributed skill map are supposed to be created by different sources (human experts, teachers, educational institutions, etc.). Each source creates an item and provides a skill assignment to that item. When the same item q is provided by two or more different sources, the problem arises of testing the agreement, among these sources. One question here is that, given a skill map q

( A A A S Q A ) σ , , :=
and an item q

, A Q ∈ ( ) q A σ
is the set of all skills in that are sufficient to solve item q according to . Thus, two different skill maps and

A S A A B , with ∅ ≠ B Q Q may reflect different
opinions on the sufficient skills of a given item. A perfect agreement arises when, for

B Q A ∩ ∈ , ( ) ) q B A (q σ σ = .
Given two sets X and Y , let denote their symmetric difference, i.e.,

Y X || ( ) Y X Y X \ : || ∪ =
Then, for any skill and any item q

B A S S s ∪ ∈ B A Q Q ∩ ∈ an agreement occurs whenever ( ) ( ) q q s A σ ∉ .
The ratio between the number of such agreements and the theoretical (maximum) number of agreements for all items in Q , and all skills in provides a raw measure of the total agreement between the two skill maps and

B A Q ∩ B A S S ∪ A
B (for the calculation of raw agreement indexes and their statistical significance see, e.g., Übersax, 1993).

Finally, note that reliability is a necessary but not sufficient condition of validity. This implies that even if reliable, a skill map should then be tested against empirical data. If the knowledge space corresponding to a given skill map is considered, then the methods and probabilistic models provided by [START_REF] Doignon | Knowledge spaces[END_REF] can be applied for this purpose.

CONCLUSIONS

Knowledge space theory provides formal models and methods for the efficient assessment of knowledge in a certain domain of knowledge. Existing methods, however, are applicable only in the case of a local domain of knowledge. An approach for the assessment of knowledge through knowledge spaces, which is appropriate for distributed and dynamic learning objects was presented in this paper. The approach focusses on the construction of distributed skill maps (and corresponding knowledge spaces) and on the derivation of new local skill maps from the distributed ones. The concept of a distributed skill map allows to exploit the advantages of applying knowledge spaces in knowledge assessment when the learning objects are located in distributed repositories, rather then local. This would allow the exploitation of new technologies like the GRID for the construction of e-learning and eassessment systems.

An algorithm for the efficient assessment of knowledge through distributed skill maps was sketched in Section 4. The algorithm applies in case of skill maps generating quasi-ordinal knowledge spaces. The explicit derivation of a knowledge space from a (local or distributed) skill map is time-consuming, especially when the domain of knowledge gets large. The advantage of the proposed algorithm is that its application does not require the explicit derivation of the knowledge space corresponding to a given skill map.

In a distributed skill map, new local skill maps can be obtained integrating existing ones. This integration poses the problem of the validity of local skill maps. This problem was discussed in Section 5 where some basic methods were proposed for obtaining statistical indexes of agreement among different skill maps. Finally, we would like to point out that the approach proposed here is restricted to the distributed construction and application of quasi-ordinal knowledge spaces, which are a special class of knowledge spaces, and knowledge structures. In the case of local learning objects, the concepts of skill multimap and skill multi-assignment were introduced to deal with the general case of any knowledge structure (see, e.g., [START_REF] Doignon | Knowledge spaces and skill assignments[END_REF][START_REF] Düntsch | Skills and knowledge structures[END_REF]. Based on these existing concepts, further work is needed to extend the concept of a distributed skill map to knowledge structures in general.