Haniel Barbosa
email: haniel.barbosa@inria.fr

Pascal Fontaine
email: pascal.fontaine@inria.fr

Andrew Reynolds
email: andrew.j.reynolds@gmail.com

Congruence Closure with Free Variables

HAL is

Introduction

SMT solvers [START_REF] Barrett | Satisfiability Modulo Theories[END_REF] are highly efficient at handling large ground formulas with interpreted symbols, but they still struggle with quantified formulas. Pure quantified first-order logic is best handled with resolution and superposition-based theorem proving [START_REF] Bachmair | Rewrite-Based Equational Theorem Proving with Selection and Simplification[END_REF]. Although there are first attempts to unify such techniques with SMT [START_REF] De Moura | Engineering DPLL(T) + Saturation[END_REF], the main approach used in SMT is still instantiation: quantified formulas are reduced to ground ones and refuted with the help of decision procedures for ground formulas. The main instantiation techniques are E -matching based on triggers [START_REF] De Moura | Efficient E-Matching for SMT Solvers[END_REF][START_REF] Detlefs | Simplify: A Theorem Prover for Program Checking[END_REF][START_REF] Rümmer | E-Matching with Free Variables[END_REF], finding conflicting instances [START_REF] Reynolds | Finding Conflicting Instances of Quantified Formulas in SMT[END_REF] and model-based quantifier instantiation (MBQI) [START_REF] Ge | Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories[END_REF][START_REF] Reynolds | Quantifier Instantiation Techniques for Finite Model Finding in SMT[END_REF]. Each of these techniques contributes to the efficiency of state-of-the-art solvers, yet each one is typically implemented independently.

We introduce the E-ground (dis)unification problem as the cornerstone of a unique framework in which all these techniques can be cast. This problem relates to the classic problem of rigid E -unification and is also NP-complete. Solving E-ground (dis)unification amounts to finding substitutions such that literals containing free variables hold in the context of currently asserted ground literals. Since the instantiation domain of those variables can be bound, a possible way of solving the problem is by first non-deterministically guessing a substitution and checking if it is a solution. The Congruence Closure with Free Variables algorithm (CCFV, for short) presented here is a practical decision procedure for this problem based on the classic congruence closure algorithm [START_REF] Nelson | Fast Decision Procedures Based on Congruence Closure[END_REF][START_REF] Nieuwenhuis | Fast congruence closure and extensions[END_REF]. It is goal-oriented: solutions are constructed incrementally, taking into account the congruence closure of the terms defined by the equalities in the context and the possible assignments to the variables.

We then show how to build on CCFV to implement trigger-based, conflictbased and model-based instantiation. An experimental evaluation of the technique is presented, where our implementations exhibits improvements over stateof-the-art approaches.

Related work

Instantiation techniques for SMT have been studied extensively. Heuristic instantiation based on E -matching of selected triggers was introduced by Detlefs et al. [START_REF] Detlefs | Simplify: A Theorem Prover for Program Checking[END_REF]. A highly efficient implementation of E -matching was presented by de Moura and Bjørner [START_REF] De Moura | Efficient E-Matching for SMT Solvers[END_REF]; it relies on elaborated indexing techniques and generation of machine code for optimizing performance. Rümmer uses triggers alongside a classic tableaux method [START_REF] Rümmer | E-Matching with Free Variables[END_REF]. Trigger based instantiation unfortunately produces many irrelevant instances. To tackle this issue, a goal-oriented instantiation technique producing only useful instances was introduced by Reynolds et al. [START_REF] Reynolds | Finding Conflicting Instances of Quantified Formulas in SMT[END_REF]. CCFV shares resemblance with this algorithm, the search being based on the structure of terms and a current model coming from the ground solver. The approach here is however more powerful and more general, and somehow subsumes this previous technique. Ge and de Moura's model based quantifier instantiation (MBQI) [START_REF] Ge | Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories[END_REF] provides a complete method for first-order logic through successive derivation of conflicting instances to refine a candidate model for the whole formula, including quantifiers. Thus it also allows the solver to find finite models when they exist. Model checking is performed with a separate copy of the ground SMT solver searching for a conflicting instance. Alternative methods for model construction and checking were presented by Reynolds et al. [START_REF] Reynolds | Quantifier Instantiation Techniques for Finite Model Finding in SMT[END_REF]. Both these model based approaches [START_REF] Ge | Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories[END_REF][START_REF] Reynolds | Quantifier Instantiation Techniques for Finite Model Finding in SMT[END_REF] allow integration of theories beyond equality, while CCFV for now only handles equality and uninterpreted functions.

Backeman and Rümmer solve the related problem of rigid E -unification through encoding into SAT, using an off-the-shelf SAT solver to compute solutions [START_REF] Backeman | Theorem Proving with Bounded Rigid E-Unification[END_REF]. Our work is more in line with goal-oriented techniques as those by Goubault [START_REF] Goubault | A rule-based algorithm for rigid E-unification[END_REF] and Tiwari et al. [START_REF] Tiwari | Rigid E-Unification Revisited[END_REF]; congruence closure algorithms being very efficient at checking solutions, we believe they can also be the core of efficient algorithms to discover them. CCFV differs from those previous techniques notably, since it handles disequalities and since the search for solutions is pruned based on the structure of a ground model and is thus most suitable for an SMT context.

We refer to classic notions of many-sorted first-order logic (e.g. by Baader and Nipkow [START_REF] Baader | Term Rewriting and All That[END_REF] and by Fitting [START_REF] Fitting | First-Order Logic and Automated Theorem Proving[END_REF]) as the basis for notations in this paper. Only the most relevant are mentioned.

A first-order language is a tuple L = S, X , P, F, sort in which S, X , P and F are disjoint enumerable sets of sort, variable, predicate and function symbols, respectively, and sort : X ∪ F ∪ P → S + is a function assigning sorts, according to the symbols' arities. Nullary functions and predicates are called constants and propositions, respectively. Formulas and terms are generated in a well-sorted manner by

t ::= x | f (t, . . . , t) ϕ ::= t t | p(t, . . . , t) | ¬ϕ | ϕ ∨ ϕ | ∀x 1 . . . x n . ϕ
in which x, x 1 , . . . , x n ∈ X , p ∈ P and f ∈ F. The predicate symbol stands for equality. The terms in a formula ϕ are denoted by T(ϕ). In a function or predicate application, the symbol being applied is referred as the term's top symbol. The free variables of a formula ϕ are denoted by FV(ϕ). A formula or term is ground iff it contains no variables. Whenever convenient, an enumeration of symbols s 1 , . . . , s n will be represented as s.

A substitution σ is a mapping from variables to terms. The application of σ to the formula ϕ (respectively the term t) is denoted by ϕσ (tσ). The domain of σ is the set dom(σ) = {x | x ∈ X and xσ = x}, while the range of σ is ran(σ) = {xσ | x ∈ dom(σ)}. A substitution σ is ground iff every term in ran(σ) is ground and acyclic iff, for any variable x, x does not occur in xσ . . . σ. For an acyclic substitution, σ is the fixed point substitution of σ.

Given a set of ground terms T closed under the subterm relation and a congruence relation on T, a congruence over T is a subset of {s t | s, t ∈ T} closed under entailment. The congruence closure (CC, for short) of a set of equations E on a set of terms T is the least congruence on T containing E. Given a consistent set of equality literals E, two terms t 1 , t 2 are said congruent iff E |= t 1 t 2 and disequal iff E |= t 1 t 2 . The congruence class in T of a given term is the set of terms in T congruent to it. The signature of a term is the term itself for a nullary symbol, and f (c 1 , . . . c n ) for a term f (t 1 , . . . t n ) with c i being the class of t i . The signature class of t is a set [t] E containing one and only one term in the class of t for each signature. Notice that the signature class of two terms in the same class is the same set of terms, and is a subset of the congruence class. We drop the subscript in [t] E when E is clear from the context. The set of signature classes of E on a set of terms T is

E cc = {[t] | t ∈ T}.

E-ground (dis)unification

For simplicity, and without loss of generality, we consider formulas in Skolem form, with all quantified subformulas being quantified clauses; we also assume all atomic formulas are equalities. SMT solvers proceed by enumerating the models for the propositional abstraction of the input formula, i.e. the formula obtained by replacing every atom and quantified subformula by a proposition. Such a model of the propositional abstraction corresponds to a set E ∪ Q, in which E and Q are conjunctive sets of ground literals and quantified formulas, respectively. If E ∪ Q is consistent, all of its models also satisfy the input formula; if not, a new candidate model is derived. The ground SMT solver first checks the satisfiability of E, and, if it is satisfiable, proceeds to reason on the set of quantified formulas Q. Ground instances I are derived from Q, and subsequently the satisfiability of E ∪ I is checked. This is repeated until either a conflict is found, and a new model for the propositional abstraction must be produced, or no more instantiations are possible. Of course, the whole process might not terminate and the solver might loop indefinitely.

In this approach, a central problem is to determine which instances I to derive. Section 5 shows that the problem of finding instances via existing instantiation techniques can be reduced to the problem of E-ground (dis)unification.

Definition 1 (E-ground (dis)unification). Given two finite sets of equality literals E and L, E being ground, the E-ground (dis)unification problem is that of finding substitutions σ such that E |= Lσ. E-ground (dis)unification can be recast as the classic problem of (non-simultaneous) rigid E -unification (transformation proof in Appendix B of [START_REF] Barbosa | Congruence Closure with Free Variables[END_REF]), i.e. computing substitutions σ such that E eq σ |= sσ tσ, in which E eq is a set of equations and s, t are terms. Rigid E -unification has been studied extensively in the context of automated theorem proving [START_REF] Baader | Unification Theory[END_REF][START_REF] Beckert | Ridig E-Unification[END_REF][START_REF] Degtyarev | Equality Reasoning in Sequent-Based Calculi[END_REF]. In particular, its intrinsic relation with congruence closure has been investigated by Goubault [START_REF] Goubault | A rule-based algorithm for rigid E-unification[END_REF] and Tiwari et al. [START_REF] Tiwari | Rigid E-Unification Revisited[END_REF], in which variations of the classic procedure are integrated with first-order rewriting techniques and the search for solutions is guided by the structure of the terms. We build on these ideas to develop our method for solving E-ground (dis)unification, as discussed in Section 4.

Example 1. Consider the sets

E = {f (a) f (b), h(a) h(c), g(b) h(c)} and L = {h(x 1 ) h(c), h(x 2 ) g(x 3 ), f (x 1 ) f (x 3 ), x 4 g(x 5 )}. A solution for their E-ground (dis)unification problem is {x 1 → a, x 2 → c, x 3 → b, x 4 → g(x 5 )}.
The above example shows that x 5 can be mapped to any term; this Eground (dis)unification problem has infinitely many solutions. However, here, like in general, 1 the set of all solutions can be finitely represented:

Theorem 1. Given an E-ground (dis)unification problem, if a substitution σ exists such that E |= Lσ, then there is an acyclic substitution σ such that ran(σ ) ⊆ T(E ∪ L), σ is ground, and E |= Lσ .

Proof. The proof can be found in Appendix A of [START_REF] Barbosa | Congruence Closure with Free Variables[END_REF].

As a corollary, the problem is in NP: it suffices indeed to guess an acyclic substitution with ran(σ ) ⊆ T(E ∪ L), and check (polynomially) that it is a solution. The problem is also NP-hard, by reduction of 3-SAT (Appendix C of [START_REF] Barbosa | Congruence Closure with Free Variables[END_REF]). As our experiments show, however, a concrete algorithm effective in practice is possible.

In this section we describe a calculus to find each substitution σ solving an E-ground (dis)unification problem E |= Lσ. This calculus, Congruence Closure with Free Variables (CCFV), uses a congruence closure algorithm as a core element to guide the search and build solutions. It proceeds by building a set of equations E σ such that E ∪ E σ |= L, in which E σ corresponds to a solution substitution, built step by step, by decomposing L in a top-down manner into sets of simpler constraints.

Example 2. Considering again E and L as in Example 1, the calculus should find σ such that

f (a) f (b), h(a) h(c), g(b) h(c) |= (h(x 1 ) h(c) ∧ h(x 2 ) g(x 3 ) ∧ f (x 1 ) f (x 3 ) ∧ x 4 g(x 5 )) σ
For L to be entailed by E ∪ E σ , each of its literals contributes to equations in E σ in the following manner:

-h(x 1 ) h(c): either x 1 c or x 1 a belongs to E σ ; -h(x 2 ) g(x 3 ): either x 2 c ∧ x 3 b or x 2 a ∧ x 3 b belongs to E σ ; -f (x 1 ) f (x 3 ): either x 1 x 3 or x 1 a ∧ x 3 b or x 1 b ∧ x 3 a must be in E σ ; -x 4 g(x 5 ): the literal itself must be in E σ .
One solution is thus E σ = {x 1 a, x 2 a, x 3 b, x 4 g(x 5 )}, corresponding to the acyclic substitution σ = {x 1 → a, x 2 → a, x 3 → b, x 4 → g(x 5 )}. Notice that, for any ground term t ∈ T(E ∪ L), σ g = σ ∪ {x 5 → t} is such that ran(σ g ) ⊆ T(E ∪ L), σ g is ground, and E |= Lσ g .

The calculus

Given an E-ground (dis)unification problem E |= Lσ, the CCFV calculus computes the various possible E σ corresponding to a coverage of all substitution solutions, i.e. such that E ∪ E σ |= L. We describe the calculus as a set of rules that operate on states of the form E σ E C, in which C is a (disjunctive normal form) formula stemming from the decomposition of L into simpler constraints, and E σ is a conjunctive set of equalities representing a partial solution. Starting from the initial state ∅ E L, the right side of the state is progressively decomposed, whereas the left side is step by step augmented with new equalities building the candidate solution. Example 2 shows that, for a literal to be entailed by E ∪ E σ , sometimes several solutions E σ exist, thus the calculus involves branching. To simplify the presentation, the rules do not apply branching directly, but build disjunctions on the right part of the state, those disjunctions later leading to branching. A branch is closed when its constraint is decomposed into either ⊥ or . The latter are branches for which E ∪ E σ |= L holds.

The set of CCFV derivation rules is presented in Table 1; t stands for a ground term, x, y for variables, u for non-ground terms, u 1 , . . . , u n for terms such that at least one is non-ground and s, s 1 , . . . , s n for terms in general. Rules are applied top-down, the symmetry of equality being used implicitly. Each rule simplifies the constraint of the right hand side of the state, and as a consequence any derivation strategy is terminating (Theorem 2).

When an equality is added to the left hand side of a state E σ E C (rule Assign), the constraint C is normalized with respect to congruence closure to reflect the assignments to variables. That is, all terms in C are representatives of classes in the congruence closure of E ∪ E σ . We write

rep(x) = some chosen y ∈ [x] Eσ if all terms in [x] Eσ are variables rep(f (s)) otherwise, for some f (s) ∈ [x] Eσ rep(f (s 1 , . . . , s n )) = f (s 1 , . . . , s n ) if f (s 1 , . . . , s n ) is ground f (rep(s 1 ), . . . , rep(s n )) otherwise
and write rep(C) to denote the result of applying rep on both sides of each literal s s or s s in C. The above definition of rep leaves room for some choice of representative, but soundness and completeness are not impacted by the choice. What actually matters is whether the representative is a variable, a ground term or a non-ground function application. The Assign rule adds equations from the right side of the state into the tentative solution in the left side of the state: it extends E σ with the mapping for a variable. Because C is replaced by rep(C), one variable (either x, or s if it is a variable) disappears from the right side.

The other rules can be divided into two categories. First are the branching rules (U var through R gen), which enumerate all possibilities for deriving the entailment of some literal from C. For example, the rule U comp enumerates the possibilities for which a literal of the form f (u 1 , . . . , u n ) f (s 1 , . . . , s n ) is entailed, which may be either due to syntactic unification, since both terms have the same top symbol, or by matching f -terms occurring in the same signature class of E cc . Second are the structural rules (Split, Fail and Yield), which create or close branches. Split creates branches when there are disjunctions in the constraint. Fail closes a branch when it is no longer possible to build on the current solution to entail the remaining constraints. Yield closes a branch when all remaining constraints are already entailed by E ∪ E σ , with E σ embodying a solution for the given E-ground (dis)unification problem. Theorems 3 and 4 state the correctness of the calculus.

If a branch is closed with Yield, the respective E σ defines a substitution σ = {x → rep(x) | x ∈ FV(L)}. The set Sols(E σ ) of all ground solutions extractable from E σ is composed of substitutions σ g which extend σ by mapping all variables in ran(σ ) into ground terms in T(E ∪ L), s.t. each σ g is acyclic, σ g ground and E |= Lσ g .

A strategy for the calculus

A possible derivation strategy for CCFV, given an initial state ∅ E L, is to apply the sequence of steps described below at each state E σ E C. Let sel be a function that selects a literal from a conjunction according to some heuristic, Let sel select the literal in C with the minimum number of variables. The derivation tree produced by CCFV for this problem is shown below. Selected literals are underlined. Disjunctions and the application of Split are kept implicit to simplify the presentation, as is the handling of x 4 g(x 5 ). Its entailment does not relate with the other literals in L and it can be handled by an early application of Assign.

Eσ E x s ∧ C Assign Eσ ∪ {x s} E rep(C) if x ∈ FV(s) Eσ E x f (u1, . . . , un) ∧ C U var Eσ E [t]∈E cc ,f (t 1 ,...,tn)∈[t] (x t ∧ u1 t1 ∧ • • • ∧ un tn ∧ C) if x ∈ FV(f (u1, . . . , un)) Eσ E f (u1, . . . , un) f (s1, . . . , sn) ∧ C U comp Eσ E (u1 s1 ∧ • • • ∧ un sn ∧ C) ∨ [t]∈E cc , f (t 1 ,...,tn)∈[t],f (t 1 ,...,t n )∈[t] u1 t1 ∧ • • • ∧ un tn ∧ s1 t 1 ∧ • • • ∧ sn t n ∧ C Eσ E f (u1, . . . , un) g(s1, . . . , sm) ∧ C U gen Eσ E [t]∈E cc , f (t 1 ,...,tn)∈[t],g(t 1 ,...,t m )∈[t] u1 t1 ∧ • • • ∧ un tn ∧ s1 t 1 ∧ • • • ∧ sm t m ∧ C if f = g Eσ E x y ∧ C R var Eσ E [t 1 ],[t 2 ]∈E cc ,E|=t 1 t 2 (x t1 ∧ y t2 ∧ C) Eσ E x f (s1, . . . , sn) ∧ C R fapp Eσ E [t],[t ]∈E cc , E|=t t ,f (t 1 ,...,t n )∈[t ] (x t ∧ s1 t 1 ∧ • • • ∧ sn t n ∧ C) Eσ E f (u1, . . . , un) g(s1, . . . , sm) ∧ C R gen Eσ E [t],[t ]∈E cc ,E|=t t , f (t 1 ,...,tn)∈[t],g(t 1 ,...,t m )∈[t ] u1 t1 ∧ • • • ∧ un tn ∧ s1 t 1 ∧ • • • ∧ sm t m ∧ C Eσ E C1 ∨ C2 Split Eσ E C1 Eσ E C2 Eσ E C Yield Eσ E if E ∪ Eσ |= C Eσ E C Fail Eσ E ⊥ if no
E cc = {{a}, {b}, {c}, {f (a)
∅ E h(x1) h(c) ∧ h(x2) g(x3) ∧ f (x1) f (x3) Ucomp A B
Since from h(x 1 ) h(c) leads to the constraints x 1 c ∨ x 1 a and a subsequent splitting of the derivation, A is

∅ E x1 c ∧ h(x2) g(x3) ∧ f (x1) f (x3) Assign {x1 c} E h(x2) g(x3) ∧ f (c) f (x3) Ucomp {x1 c} E h(x2) g(x3) ∧ x3 c Assign {x1 c, x3 c} E h(x2) g(c) Rgen {x1 c, x3 c} E ⊥ Fail {x1 c, x3 c} E ⊥ and B is ∅ E x1 a ∧ h(x2) g(x3) ∧ f (x1) f (x3) Assign {x1 a} E h(x2) g(x3) ∧ f (a) f (x3) Ucomp {x1 a} E h(x2) g(x3) ∧ x3 a Assign {x1 a, x3 a} E h(x2) g(a) Rgen {x1 a, x3 a} E ⊥ Fail {x1 a, x3 a} E ⊥ {x1 a} E h(x2) g(x3) ∧ x3 b Assign {x1 a, x3 b} E h(x2) g(b) Rgen C1 C2
with Proof (sketch). The width of any split rule is always finite. It then suffices to show that the depth of the tree is bounded. For simplicity, but without any fundamental effect on the proof, let us assume that all rules but Split apply on conjunctions. Let d(C) be the sum of the depths of all occurrences of variables in the literals of the conjunction C. The Assign rule decreases the number of variables of C. The Fail and Yield rules close a branch. All remaining rules from

E σ E C to E σ E C 1 ∨• • •∨C n decrease d, i.e. d(C) > d(C 1 ), . . . , d(C) > d(C n ).
At each node, d(C) or the number of variables in C are decreasing, except at the Split steps. Since no branch can contain infinite sequences of Split applications, the depth is always finite. Lemma 1. Given a computed solution E σ for an E-ground (dis)unification problem E |= Lσ, each σ g ∈ Sols(E σ ) is an acyclic substitution such that ran(σ g ) ⊆ T(E ∪ L) and σ g is ground.

Proof (sketch). The proof can be found in Appendix D of [START_REF] Barbosa | Congruence Closure with Free Variables[END_REF].

Lemma 2 (Rules capture entailment conditions). For each rule

E σ E C R E σ E C and any ground substitution σ, E |= ({C} ∪ E σ )σ iff E |= ({C } ∪ E σ )σ.
Proof (sketch). The proof can be found in Appendix D of [START_REF] Barbosa | Congruence Closure with Free Variables[END_REF].

Theorem 3 (Soundness). Whenever a branch is closed with Yield, every

σ g ∈ Sols(E σ ) is s.t. E |= Lσ g .
Proof (sketch). Consider an arbitrary substitution σ g ∈ Sols(E σ ) at the application of Yield. Lemma 1 ensures that σ g is ground. Thanks to the side condition of the Yield rule and of the construction of σ g , E |= ({C} ∪ E σ )σ g at the leaf. Then, thanks to Lemma 2, E |= ({C} ∪ E σ )σ g also holds at the root, in which C = L and E σ = ∅. Thus E |= Lσ g . Theorem 4 (Completeness). Let σ be a solution for an E-ground (dis)unification problem E |= Lσ. Then there exists a derivation tree starting on ∅ E L with at least one branch closed with Yield s.t. σ g ∈ Sols(E σ ) and E |= Lσ g . Proof (sketch). By Theorem 1, there is an acyclic substitution σ g corresponding to σ such that ran(σ g ) ⊆ T(E ∪ L), σ g is ground and E |= Lσ g . Lemma 2 ensures that all rules in CCFV preserve the entailment conditions according to ground substitutions, therefore there is a branch in the derivation tree starting from ∅ E L whose leaf is E σ E and σ g ∈ Sols(E σ ).

Corollary 1 (CCFV decides E-ground (dis)unification). Any derivation strategy based on the CCFV calculus is a decision procedure to find all solutions σ for the E-ground (dis)unification problem E |= Lσ.

Relation to instantiation techniques

Here we discuss how different instantiation techniques for evaluating a candidate model E ∪ Q can be related with E-ground (dis)unification and thus integrated with CCFV.

Trigger based instantiation

The most common instantiation technique in SMT solving is a heuristic one: its search is based solely on E -matching of selected triggers [START_REF] De Moura | Efficient E-Matching for SMT Solvers[END_REF][START_REF] Detlefs | Simplify: A Theorem Prover for Program Checking[END_REF][START_REF] Rümmer | E-Matching with Free Variables[END_REF], without further semantic criteria. A trigger T for a quantified formula ∀x.

ψ ∈ Q is a set of terms f 1 (s 1 ), . . . , f n (s n ) ∈ T(ψ) s.t. {x} ⊆ FV(f 1 (s 1 )) ∪ • • • ∪ FV(f n (s n )).
Instantiations are determined by E -matching all terms in T with terms in T(E), such that resulting substitutions allow instantiating ∀x. ψ into ground formulas. Computing such substitutions amounts to solving the E-ground (dis)unification problem

E |= (f 1 (s 1 ) y 1 ∧ • • • ∧ f n (s n ) y n ) σ
with the further restriction that σ is acyclic, ran(σ) ⊆ T(E ∪L) and σ is ground. This forces each y i to be grounded into a term in T(E), thus enumerating all possibilities for E -matching f i (s i ). 2 The desired instantiations are obtained by restricting the found solutions to x.

Example 4. Consider the sets E = {f (a) g(b), h(a) b, f (a) f (c)} and Q = {∀x. f (x) g(h(x))}. Triggers from Q are T 1 = {f (x)}, T 2 = {h(x)}, T 3 = {f (x), g(h(x))
} and so on. The instantiations from those triggers are derived from the solutions yielded by CCFV for the respective problems:

-E |= (f (x) y)σ, solved by substitutions σ 1 = {y → f (a), x → a} and σ 2 = {y → f (c), x → c} -E |= (h(x) y)σ, solved by σ = {y → h(a), x → a} -E |= (f (x) y 1 ∧ g(h(x)) y 2 )σ, by σ = {y 1 → f (a), y 2 → g(b), x → a}
2 For CCFV to generate such solutions it is sufficient to add the side condition to Assign that s is a variable or a ground term and to remove the side condition of U var. This will lead to the application of U var in each fi(s1) yi.

Discarding entailed instances Trigger-based instantiation may produce instances which are already entailed by the ground model. Such instances most probably will not contribute to the solving, so they should be discarded. Checking this, however, is not straightforward with pre-processing techniques. CCFV, on the other hand, allows it by simply checking, given an instantiation σ for a quantified formula ∀x. ψ, whether there is a literal

∈ ψ s.t. E ∪ E σ |= , with E σ = {x xσ | x ∈ dom(σ)}.

Conflict based instantiation

A goal-oriented instantiation technique was introduced by Reynolds et al. [START_REF] Reynolds | Finding Conflicting Instances of Quantified Formulas in SMT[END_REF] to provide fewer and more meaningful instances. Quantified formulas are evaluated, independently, in search for conflicting instances: for each quantified formula ∀x. ψ ∈ Q, only instances ψσ for which E ∪ ψσ is unsatisfiable are derived. Such instances force the derivation of a new candidate model E ∪ Q for the formula. Finding a conflicting instance amounts to solving the E-ground (dis)unification problem E |= ¬ψσ, for some ∀x. ψ ∈ Q since ¬ψ is a conjunction of equality literals. Differently from the algorithm shown in [START_REF] Reynolds | Finding Conflicting Instances of Quantified Formulas in SMT[END_REF], CCFV finds all conflicting instantiations for a given quantified formula.

Example 5. Let E and Q be as in Example 4. Applying CCFV in the problem

E |= (f (x) g(h(x))) σ
leads to the sole conflicting instantiation σ = {x → a}.

Propagating equalities As discussed in [START_REF] Reynolds | Finding Conflicting Instances of Quantified Formulas in SMT[END_REF], even when the search for conflicting instances fails it is still possible to "propagate" equalities. Given some

¬ψ = 1 ∧ • • • ∧ n , let σ be a ground substitution s.t. E |= 1 σ ∧ • • • ∧ k-1 σ
and all remaining literals k σ, . . . , n σ not entailed are ground disequalities with

(T( k ) ∪ • • • ∪ T( n )) ⊆ T(E).
E |= (f (x) t ∧ f (x) g(x)) σ
to entail the first literal a candidate solution E σ = {x a} is produced. The second literal would then be normalized to f (a) g(a), which would lead to the application of Fail, since it is not entailed by E. However, as it is a disequality whose terms are in T(E) and originally had variables, the rule applied is Yield instead. The resulting substitution σ = {x → a} leads to propagating the equality f (a) g(a), which merges two classes previously different in E cc .

Model based instantiation (MBQI)

A complete instantiation technique was introduced by Ge and de Moura [START_REF] Ge | Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories[END_REF].

The set E is extended into a total model, each quantified formula is evaluated in this total model, and conflicting instances are generated. The successive rounds of instantiation either lead to unsatisfiability or, when no conflicting instance is generated, to satisfiability with a concrete model. Here we follow the model construction guidelines by Reynolds et al. [START_REF] Reynolds | Quantifier Instantiation Techniques for Finite Model Finding in SMT[END_REF].

A distinguished term e τ is associated to each sort τ ∈ S. For each f ∈ F with sort τ 1 , . . . , τ n , τ a default value ξ f is defined such that

ξ f = f (t 1 , . . . , t n ) ∈ T(E) if [t 1 ] = [e τ1 ], . . . , [t n ] = [e τn ] some t ∈ T(E) otherwise
The extension E tot is built s.t. all fresh ground terms which might be considered when evaluating Q are in its congruence closure, according to the respective default values; and all terms in T(E) not asserted equal are explicitly asserted disequal, i.e.

E tot = E ∪ t1,t2∈ T(E) {t 1 t 2 | E |= t 1 t 2 } ∀x. ψ∈Q,t∈ T(E) f (s)σ ξ f σ = {x → t}, f (s) ∈ T(ψ) and f (s)σ is not in the CC of E.
As before, finding conflicting instances amounts to solving the E-ground (dis)unification problem leads to a conflicting instance with σ = {x → b}. Notice that it is not necessary to explicitly build E tot , which can be quite large. Terms can be defined lazily as they are required by CCFV for building potential solutions.

Implementation and Experiments

CCFV has been implemented in the veriT [START_REF] Bouton | veriT: An Open, Trustable and Efficient SMT-Solver[END_REF] and CVC4 [START_REF] Barrett | CVC4[END_REF] solvers. As is common in SMT solvers, they make use of an E -graph to represent the set of signa-ture classes E cc and efficiently check ground entailment. 3 Indexing techniques for fast retrieval of candidates are paramount for a practical procedure, so E cc is indexed by top symbols. Each function symbol points to all their related signatures. They are kept sorted by congruence classes to allow binary search when retrieving all signatures with a given top symbol congruent to a given term. To quickly discard classes without signatures with a given top symbol, bit masks are associated to congruence classes: each symbol is assigned an arbitrary bit, and the mask for the class is the set of all bits of the top symbols. Another important optimization is to minimize E, since the candidate model E ∪ Q produced by the SAT solver and guiding the instantiation is generally not minimal.

A minimal partial model (a prime implicant) for the CNF is computed in linear time [START_REF] Déharbe | Computing Prime Implicants[END_REF], and this model is further reduced to circumvent the effect of the CNF transformation, using a process similar to the one described by de Moura and Bjørner [START_REF] De Moura | Efficient E-Matching for SMT Solvers[END_REF] for relevancy.

During rule application, matching a term f (u) with a ground term f (t) fails unless all the ground arguments are pairwise congruent. Thus after an assignment, if an argument of a term f (u) in a branching constraint becomes ground, it can be checked whether there is a ground term f (t) ∈ T(E) s.t., for every ground argument u i , E |= u i t i . If no such term exists and f (u) is not in a literal amenable for U comp, the branch can be eagerly discarded. For this technique, a dedicated index for each function symbol f maps tuples of pairs, with a ground term and a position, (t 1 , i 1 ), . . . , (t k , i k ) to all signatures f (t 1 , . . . , t n ) in E cc s.t. E |= t 1 t i1 , . . . , E |= t k t i k , i.e. all signatures whose arguments, in the respective positions, are congruent with the given ground terms.

Experiments Here we evaluate the impact of optimizations and instantiation techniques based on CCFV over previous versions and compare them against the state-of-the-art instantiation based solver Z3 [START_REF] De Moura | Z3: An Efficient SMT Solver[END_REF]. Different configurations are identified in this section according to which techniques and algorithms they have activated: t : trigger instantiation through CCFV; c : conflict based instantiation through CCFV; e : optimization for eagerly discarding branches with unmatchable applications; d : discards already entailed trigger based instances (as in 5.1)

The configuration verit refers to the previous version of veriT, which only offered support for quantified formulas through naïve trigger instantiation, without further optimizations. The configuration cvc refers to version 1.5 of CVC4, which applies t and c by default, as well as propagation of equalities. Both implementations of CCFV include efficient term indexing and apply a simple selection heuristic, checking ground and reflexive literals first but otherwise considering the conjunction of constraints as a queue. The evaluation was made on the UF, UFLIA, UFLRA and UFIDL categories of SMT-LIB [START_REF] Barrett | The SMT-LIB Standard: Version 2.0[END_REF], with 10 495 benchmarks annotated as unsatisfiable, mostly stemming for verification and ITP platforms. The categories with bit vectors and non-linear arithmetic are currently not supported by veriT and in those in which uninterpreted functions are not predominant the techniques shown here are not as effective. Our experiments were conducted using machines with 2 CPUs Intel Xeon E5-2630 v3, 8 cores/CPU, 126GB RAM, 2x558GB HDD. The timeout was set for 30 seconds, since our goal is evaluating SMT solvers as back-ends of verification and ITP platforms, which require fast answers.

Figure 1 exhibits an important impact of CCFV and the techniques and optimizations built on top of it. verit+t performs much better than verit, solely due to CCFV. cvc+d improves significantly over cvc, exhibiting the advantage of techniques based on the entailment checking features of CCFV. The comparison between the different configurations of veriT and CVC4 with the SMT solver Z3 (version 4.4.2) is summarized in Table 2, excluding categories whose problems are trivially solved by all systems, which leaves 8 701 problems for consideration. verit+tc shows further improvements, solving approximately the same number of problems as Z3, although mostly because of the better performance on the sledgehammer benchmarks, containing less theory symbols. It also performs best in the grasshopper families, stemming from the heap verification tool GRASShopper [START_REF] Piskac | GRASShopper -Complete Heap Verification with Mixed Specifications[END_REF]. Considering the overall performance, both cvc+d and cvc+e solve significantly more problems than cvc, specially in benchmarks from verification platforms, approaching the performance of Z3 in these families. Both these techniques, as well as the propagation of equalities, are fairly important points in the performance of CVC4, so their implementation is a clear direction for improvements in veriT.

  , f (b)}, {h(a), h(c)}, {g(b)}} and the disequalities entailed by E are g(b) h(c) and g(b) h(a).

4. 3

 3 Correctness of CCFVTheorem 2 (Termination). All derivations in CCFV are finite.

E

  tot |= ¬ψσ, for some ∀x. ψ ∈ Q Example 7. Let E = {f (a) g(b), h(a) b}, Q = {∀x. f (x) g(x), ∀xy. ψ} and e = a, with all terms having the same sort. The computed default values of the function symbols are ξ f = f (a), ξ g = a, ξ h = h(a). For simplicity, the extension E tot is shown explicitly only for ∀x. f (x) g(x), E tot = E ∪ {a b, a f (a), b f (a)} ∪ {f (b) f (a), f (f (a)) f (a), g(a) a, g(f (a)) a} ∪ {. . . } Applying CCFV in {. . . , f (a) g(b), f (b) f (a), . . . } |= f (x) g(x)σ

3Fig. 1 :

 1 Fig. 1: Improvements in veriT and CVC4

Table 1 :

 1 other rule can be applied; or C is a conjunction and E |= , for some ground ∈ C The CCFV calculus in equational FOL. E is fixed from a problem E |= Lσ.such as selecting first literals with less variables or literals whose top symbols have less ground signatures in E cc . The result of sel is denoted selected literal. Since no two rules can be applied on the same literal, the function sel effectively enforces an order on the application of the rules. 1. Select branch: While C is a disjunction, apply Split and consider the leftmost branch, by convention. 2. Simplify constraint: Apply the rule for which sel(C) is amenable. 3. Discard failure: If Fail was applied or a branching rule had the empty disjunction as a result, discard this branch and consider the next open branch. 4. Mark success: If all remaining constraints in the branch are entailed by E ∪ E σ , apply Yield to mark the successful branch and then consider the next open branch.

A solution σ for the E-ground (dis)unification problem E |= Lσ can be extracted at each branch terminated by the Yield rule (Corollary 1). Example 3. Consider again E and L as in Example 1. The set of signature classes of E is

  C 1 and C 2 resulting from the disjunction x 2 a ∨ x 2 c derived from h(x 2 ) g(b):

	{x1	a, x3	b} E x2	a			{x1	a, x3	b} E x2	c
	{x1	a, x2	a, x3	b} E	Assign	{x1	a, x2	c, x3	b} E	Assign
	{x1	a, x2	a, x3	b} E	Yield		{x1	a, x2	c, x3	b} E	Yield
	Solutions are produced by both C 1 and C 2 , differing only on the assignment to
	x 2 , with the solution E σ = {x 1	a, x 2	a, x 3	b, x 4	g(x 5 )} from C 1
	corresponding to the same E σ respecting the entailment conditions shown in
	Example 2.

  The instantiation ∀x. ψ → ψσ introduces a disjunction of equalities constraining T(E). CCFV can generate such propagating substitutions if the side conditions of Fail and Yield are relaxed w.r.t. ground disequalities whose terms occur in T(E) and originally had variables: the former is not applied based on them and the latter is if all other literals are entailed.

	Example 6. Consider E = {f (a) t, t	g(a)} and ∀x. f (x) t ∨ f (x) g(x).
	When applying CCFV in the problem

It is assumed, without loss of generality, that T(E ∪ L) contains at least one ground term of each sort in E ∪ L.

Acknowledgments We are grateful to David Déharbe for his help with the implementation of CCFV and to Jasmin Blanchette for suggesting textual improvements. Experiments presented in this paper were carried out using the Grid'5000 testbed, supported by a scientific interest group hosted by Inria and including CNRS, RENATER and several universities as well as other organizations (https://www.grid5000.fr).

This work has been partially supported by the ANR/DFG project STU 483/2-1 SMArT ANR-13-IS02-0001 of the Agence Nationale de la Recherche, by the H2020-FETOPEN-2016-2017-CSA project SC 2 (712689), and by the European Research Council (ERC) starting grant Matryoshka (713999).

Conclusion and Future Work

We have introduced CCFV, a decision procedure for E-ground (dis)unification, and shown how the main instantiation techniques of SMT solving may be based on it. Our experimental evaluation shows that CCFV leads to significant improvements in the solvers CVC4 and veriT, making the former surpass the stateof-the-art in instantiation based SMT solving and the latter competitive in several benchmark libraries. The calculus presented is very general, allowing for different strategies and optimizations, as discussed in previous sections.

A direction for improvement is to use lemma learning in CCFV, in a similar manner as SAT solvers do. When a branch fails to produce a solution and is discarded, analyzing the literals which led to the conflict can allow backjump rather than simple backtracking, thus further reducing the solution search space. The Complementary Congruence Closure introduced by Backeman and Rümmer [START_REF] Backeman | Efficient Algorithms for Bounded Rigid Eunification[END_REF] could be extended to perform such an analysis.

Like other main instantiation techniques in SMT, the framework here focuses on the theory of equality only. Extensions to first-order theories such as arithmetic are left for future work. The implementation of MBQI based on CCFV, whose theoretical suitability we outlined, is left for future work as well. Another possible extension of CCFV is to handle rigid E -unification, so it could be applied in techniques such as BREU [START_REF] Backeman | Theorem Proving with Bounded Rigid E-Unification[END_REF]. This amounts to have non-ground equalities in E, so it is not trivial. It would, however, allow integrating an efficient goal-oriented procedure into E -unification based calculi.


Radu-Daniel Vatavu
email: vatavu@eed.usv.ro

Daniel Vogel
email: dvogel@mta.ca

Géry Casiez
email: gery.casiez@lifl.fr

Laurent Grisoni
email: laurent.grisoni@lifl.fr

Estimating the Perceived Difficulty of Pen Gestures

Keywords: gesture-based interfaces, pen input, gesture descriptors

Our empirical results show that users perceive the execution difficulty of single stroke gestures consistently, and execution difficulty is highly correlated with gesture production time. We use these results to design two simple rules for estimating execution difficulty: establishing the relative ranking of difficulty among multiple gestures; and classifying a single gesture into five levels of difficulty. We confirm that the CLC model does not provide an accurate prediction of production time magnitude, and instead show that a reasonably accurate estimate can be calculated using only a few gesture execution samples from a few people. Using this estimated production time, our rules, on average, rank gesture difficulty with 90% accuracy and rate gesture difficulty with 75% accuracy. Designers can use our results to choose application gestures, and researchers can build on our analysis in other gesture domains and for modeling gesture performance.

Introduction

There are three primary factors which contribute to a successful gesture-based interface: the acquisition technology, the recognizer, and the design of the gesture set. Technologies to acquire gestures [START_REF] Grange | Moris: a medical/operating room interaction system[END_REF][START_REF] Kratz | A $3 gesture recognizer: simple gesture recognition for devices equipped with 3d acceleration sensors[END_REF][START_REF] Morris | Understanding users' preferences for surface gestures[END_REF][START_REF] Wobbrock | User-defined gestures for surface computing[END_REF], and gesture recognition algorithms [START_REF] Kristensson | Shark2: a large vocabulary shorthand writing system for penbased computers[END_REF][START_REF] Li | Protractor: a fast and accurate gesture recognizer[END_REF][START_REF] Wobbrock | Gestures without libraries, toolkits or training: a $1 recognizer for user interface prototypes[END_REF], are now quite robust and widely available. However, developing techniques and criteria to help designers create an intuitive and easy-to-perform gesture set remain an active area of research. The challenge is that in order to successfully integrate into an application, a gesture has to satisfy multiple criteria: it must be unambiguously recognized [START_REF] Ashbrook | Magic: a motion gesture design tool[END_REF][START_REF] Long | Helping designers create recognition-enabled interfaces[END_REF][START_REF] Long | Implications for a gesture design tool[END_REF]; fit well with its associated function [START_REF] Morris | Understanding users' preferences for surface gestures[END_REF][START_REF] Nielsen | A procedure for developing intuitive and ergonomic gesture interfaces for HCI[END_REF][START_REF] Wobbrock | User-defined gestures for surface computing[END_REF]; be easy to learn and recall [START_REF] Nielsen | A procedure for developing intuitive and ergonomic gesture interfaces for HCI[END_REF]; and be efficient to perform [START_REF] Morris | Understanding users' preferences for surface gestures[END_REF][START_REF] Nielsen | A procedure for developing intuitive and ergonomic gesture interfaces for HCI[END_REF][START_REF] Wobbrock | User-defined gestures for surface computing[END_REF].

Researchers have offered two different strategies to assist designers. The first is to use predictive models to analytically evaluate candidate gestures. These have been successful for evaluating recognition ambiguity [START_REF] Ashbrook | Magic: a motion gesture design tool[END_REF][START_REF] Long | Implications for a gesture design tool[END_REF] and have made progress towards predicting actual performance time [START_REF] Cao | Modeling human performance of pen stroke gestures[END_REF][START_REF] Isokoski | Model for unistroke writing time[END_REF]. Unfortunately, creating accurate predictive models for non-recognition criteria such as performance time is difficult due to the complexity of gestural motion and criteria interdependencies -factors which are also influenced by an individual user's cognitive ability, physical skill, and cultural context. For these reasons, researchers have proposed a second strategy using formal user studies for participatory design and gesture set evaluation [START_REF] Ashbrook | Magic: a motion gesture design tool[END_REF][START_REF] Morris | Understanding users' preferences for surface gestures[END_REF][START_REF] Nielsen | A procedure for developing intuitive and ergonomic gesture interfaces for HCI[END_REF][START_REF] Rico | Usable gestures for mobile interfaces: evaluating social acceptability[END_REF][START_REF] Wobbrock | User-defined gestures for surface computing[END_REF]. Involving users in any design process is a good idea, but the effort to plan, run, and analyze these kinds of studies is large compared to using a predictive model.

We offer a practical solution in-between a model and a user study. Based on an estimate of actual production time, we found that designers can reasonably estimate user's perceived gesture execution difficulty. The notion of difficulty encompasses multiple criteria including the ease with which a gesture may be learned, remembered, and performed. This notion of difficulty has been mentioned in previous work [START_REF] Morris | Understanding users' preferences for surface gestures[END_REF][START_REF] Nielsen | A procedure for developing intuitive and ergonomic gesture interfaces for HCI[END_REF][START_REF] Wobbrock | User-defined gestures for surface computing[END_REF], but there has been no previous attempt to examine it in detail or estimate it. In an experiment using single stroke pen gestures, we elicited a difficulty classification rating and a relative difficulty ranking from participants. Based on data from a second validation experiment, our results show that the difficulty ranking can be predicted with greater than 93% accuracy using measured production time and 87% using the Isokoski first-order predictive production time model [START_REF] Isokoski | Model for unistroke writing time[END_REF]. Using a Bayes classification rule and measured production time, we can also classify the difficulty rating with 83% accuracy. Since the times predicted by the CLC predictive model [START_REF] Cao | Modeling human performance of pen stroke gestures[END_REF] reduced the accuracy of our classification rule to 25%, we analyzed an alternative approach. We found that production time can be reasonably estimated by gathering a few samples of actual production time -a set of data which may already exist for the purpose of training a gesture recognizer. With three people supplying three gesture samples, our classification rule achieved 75% accuracy on average and increased the average accuracy of the estimated difficulty ranking to 90%.

Our findings that gesture difficulty can be predicted from production time, together with our results regarding the reasonable estimation of production time based on a very small set of data, provide designers with a general measurement encompassing multiple criteria to assess gesture sets without a full formal user study.

Previous Work

Creating a successful gesture-based interface is challenging. Once a vocabulary of gestures moves beyond a small set of directional strokes, it becomes more difficult to learn, remember, and use [START_REF] Kurtenbach | Contextual animation of gestural commands[END_REF]. Techniques exist which assist with recall and help to transition users from novice to expert: examples include crib-sheet diagrams [START_REF] Kurtenbach | Contextual animation of gestural commands[END_REF] and dynamic path guides [START_REF] Bau | Octopocus: a dynamic guide for learning gesture-based command sets[END_REF]. While these techniques are effective, they assume that a good gesture set has already been created.

Gesture Design Tools

One way to make the designer's job easier is to use a gesture design tool. An example is Appert and Zhai's Stroke Shortcuts Toolkit [START_REF] Appert | Using strokes as command shortcuts: cognitive benefits and toolkit support[END_REF] which includes a simple tool with a predefined dictionary of stroke primitives. The hope is that a designer's creativity is stimulated with a "structured design space that can be systematically explored". Long et al.'s Quill gesture design tool [START_REF] Long | Helping designers create recognition-enabled interfaces[END_REF][START_REF] Long | Implications for a gesture design tool[END_REF] goes further by providing metrics to help designers evaluate potential gesture sets. The metrics relate to recognition rate, and conveyed through values such as classification distance or visualized as confusion matrices. Ashbrook and Starner's MAGIC tool [START_REF] Ashbrook | Magic: a motion gesture design tool[END_REF] introduces gesture goodness as a metric. In an evaluation, this seemingly abstract metric was useful as a quantitative guideline compared to a specific breakdown of individual measures (such as interclass variability graphs). However, goodness is also closely related to recognition rate. Although participants were also asked to design gestures that would be easy to remember, perform, and be socially acceptable, MAGIC, like Quill, does not provide any quantitative feedback for these criteria.

Models

Producing quantitative measurements to represent other criteria requires predictive models. For example, Long et al. [START_REF] Long | Visual similarity of pen gestures[END_REF] developed a model for predicting the perceived visual similarity of two gestures. Their model was generated by selecting a subset of geometric and dynamic features of gesture trajectories, and looking for a correlation with experimentally determined user rated visual similarity. The final model could predict visual similarity of two gestures reasonably well (correlated R 2 =.56 with ground truth). One application is increasing recognition rate by avoiding ambiguous gestures, but the authors also argue that a visual similarity metric may be used to improve a gesture's fit with its function. For example, designers could assign visually similar gestures to similar operations (such as scroll up and scroll down), and dissimilar gestures to more abstract tasks such as cut and paste.

Isokoski [START_REF] Isokoski | Model for unistroke writing time[END_REF] introduced a model to predict the relative ordering of gesture production times based on geometric complexity. The model sums the minimal number of straight segments needed to maintain a human recognizable shape in the gesture. This sum is interpreted as a complexity number and can be used as a firstorder ranking of gesture production time: the model ranked production times of Unistroke characters with R 2 =.85. Although there is ambiguity in the definition and calculation method, Isokoski's model has the advantage of being conceptually simple.

Cao and Zhai's [START_REF] Cao | Modeling human performance of pen stroke gestures[END_REF] Curves, Lines and Corners (CLC) model goes beyond Isokoski by attempting to predict the actual production time of a single stroke gesture. After decomposing a gesture into curved and straight segments, the model calculates individual production times for curves based on Viviani's 2/3 power law of curvature [START_REF] Viviani | Minimum-jerk, two-thirds power law, and isochrony: converging approaches to movement planning[END_REF] and a simple power term based on the length of straight lines (no time is calculated for corners, they are only used to segment lines and curves). The authors found that CLC works very well as a first order predictor (correlations with test data had R 2 >.90), but over-or under-predicted arbitrary gestures times by 30% and overpredicted Unistroke and Graffiti gestures by more than 40%. Castellucci and MacKenzie also noted this type of performance for CLC [START_REF] Castellucci | Graffiti vs. unistrokes: an empirical comparison[END_REF]. Cao and Zhai attribute this behaviour to the model's inability to compensate for unfamiliar and little practiced gestures, or familiar and well-practiced gestures.

User Studies

Rather than rely on predictive models, researchers have suggested that user studies should be used to assist in the design and evaluation of gesture sets. For example, Nielsen et al. [START_REF] Nielsen | A procedure for developing intuitive and ergonomic gesture interfaces for HCI[END_REF] provide a user-centered procedure to design whole-hand gestures. The procedure requires two user studies, an initial study to gather user input to inform design and a subsequent study to evaluate. In a case study application, they report they were able to obtain a good gesture set, but the procedure was very time consuming. Also, key stages such as the generation of scenarios must be carefully prepared or else results may be substandard.

Wobbrock et al. [START_REF] Wobbrock | User-defined gestures for surface computing[END_REF] take a participatory design approach by eliciting a gesture set from users. Using wizard-of-oz techniques, they asked users to mimic the best multitouch gesture to match a demonstrated action such as scale, rotate, move, etc. The study, as well as a follow-up [START_REF] Morris | Understanding users' preferences for surface gestures[END_REF], also gathered rankings for each candidate gesture's intuitiveness and ease-of-execution. Perhaps surprising, but the authors report that gestures which experienced designers propose are not always preferred by users [START_REF] Morris | Understanding users' preferences for surface gestures[END_REF].

Summary

Ideally, the best way to design an intuitive and easy-to-perform gesture set is to involve users like Nielsen et al. [START_REF] Nielsen | A procedure for developing intuitive and ergonomic gesture interfaces for HCI[END_REF] and Wobbrock et al. [START_REF] Wobbrock | User-defined gestures for surface computing[END_REF] since even experienced designers cannot predict user preference [START_REF] Morris | Understanding users' preferences for surface gestures[END_REF]. But, faced with the large amount of effort required to plan, run, and analyze these studies [START_REF] Nielsen | A procedure for developing intuitive and ergonomic gesture interfaces for HCI[END_REF], perhaps there is a way for designers to evaluate candidate designs using predictive models and/or minimal user data. Long et al.'s [START_REF] Long | Visual similarity of pen gestures[END_REF] visual similarity predictive model is interesting since it can guide designers with a gesture's fit with a function. Isokoski [START_REF] Isokoski | Model for unistroke writing time[END_REF], and Cao and Zhai [START_REF] Cao | Modeling human performance of pen stroke gestures[END_REF], have made progress towards estimating actual gesture production time, a measure which should directly relate to how efficient a gesture is to perform. However, Cao and Zhai [START_REF] Cao | Modeling human performance of pen stroke gestures[END_REF] and Castellucci and MacKenzie [START_REF] Castellucci | Graffiti vs. unistrokes: an empirical comparison[END_REF] note that production time is a partial function of many factors and therefore an accurate predictive model remains elusive. Inspired by Long et al., as well as Ashbrook and Starner's success with a seemingly abstract post-hoc measure of goodness [START_REF] Ashbrook | Magic: a motion gesture design tool[END_REF], we focus on a measure of execution difficulty.

Experiment 1: Measuring Execution Difficulty

The notion of execution difficulty (or the converse, ease-of-execution) is frequently mentioned [START_REF] Ashbrook | Magic: a motion gesture design tool[END_REF][START_REF] Long | Implications for a gesture design tool[END_REF][START_REF] Long | Visual similarity of pen gestures[END_REF][START_REF] Nielsen | A procedure for developing intuitive and ergonomic gesture interfaces for HCI[END_REF] and has been measured for multi-touch gestures with postexperiment surveys [START_REF] Morris | Understanding users' preferences for surface gestures[END_REF][START_REF] Wobbrock | User-defined gestures for surface computing[END_REF], but there has been no attempt to estimate it a priori. Morris et al. associate difficulty with "carrying out the gesture's physical action" [START_REF] Morris | Understanding users' preferences for surface gestures[END_REF]. Carrying out an action refers directly to efficiency of performance, but also involves a cognitive process which relates to how easy a gesture is to learn and recall [START_REF] Cao | Modeling human performance of pen stroke gestures[END_REF]. Thus, execution difficulty is a general quantitative measure which combines multiple design criteria: learn-ability, recall, and performance. More abstract measures, such as goodness [START_REF] Ashbrook | Magic: a motion gesture design tool[END_REF] and general preference [START_REF] Wobbrock | Gestures without libraries, toolkits or training: a $1 recognizer for user interface prototypes[END_REF] may include additional criteria (such as social acceptability [START_REF] Rico | Usable gestures for mobile interfaces: evaluating social acceptability[END_REF]), but the more general the measure, the more abstract it is due to more complex relationships of the underlying criteria. The challenge is how to estimate execution difficulty given a candidate gesture or gesture set, with the knowledge that it encompasses criteria which are known to be difficult to predict.

In the first experiment, we measure perceived execution difficulty for a set of single stroke gestures. If there is significant agreement across participants, then it is likely to be an intuitive measure suitable for a priori estimation. Using the participants' movement logs and the geometric gesture shapes, we compute quantitative measures ("descriptors") and test these for correlations with the participants' responses. If well correlated descriptors exist, and they can be estimated or computed directly, then designers have a way to estimate perceived difficulty of candidate gesture designs.

Task

Each trial began with the path of the current gesture to be entered shown on the left side of the display (Fig 1a). Participants were instructed to enter a continuous stroke for the gesture and to balance speed and accuracy. After performing the gesture, two buttons were enabled representing a choice between flagging their input as incorrect or continuing to the next gesture. Participants were instructed to flag a stroke as incorrect if the shape they entered was different from the target gesture, or if some accidental input occurred such as the pen slipping or moving unevenly. This was logged as an input error and the participant was asked to re-execute the gesture. Like Wobbrock et al. [START_REF] Wobbrock | User-defined gestures for surface computing[END_REF], we wanted our participants to decide whether a gesture was similar to the template, avoiding any confounding effects due to the behavior of a recognizer. As an extra precaution, all participant executions were visually inspected by the authors and confirmed that they were correctly entered.

Gesture Set

There were 18 different single stroke gestures (Fig 2). The set contains 9 gestures designed to be familiar (i.e. letters and shapes used in everyday writing) and 9 gestures designed to be unfamiliar (e.g. the twirl-omega and flower shapes may appear familiar, but are unlikely to be practiced as a pen stroke, while steep-hill and triangles-chain are completely new shapes). As discussed earlier, Cao and Zhai [START_REF] Cao | Modeling human performance of pen stroke gestures[END_REF] argue that familiarity affects actual performance time due to practice. The idea is that a more practiced gesture will result in a lower performance time in spite of high objective geometric complexity. For example, although the letter g is a rather complex series of twists and 180-degrees turns, it would be difficult to reproduce initially; but, with practice it can be executed very quickly. Since practice also relates to how easy a gesture is to learn and recall, familiarity is likely to relate to execution difficulty. We expected that more familiar gestures will be rated as easier to perform, even if they have high objective complexity.

Design

Each participant executed each gesture 20 times, with the 18x20 = 360 gestures presented in random order. The number of repetitions [START_REF] Rubine | Specifying gestures by example[END_REF] was chosen larger than the current practice when eliciting gestures from users, be it for training gesture recognizers [START_REF] Wobbrock | Gestures without libraries, toolkits or training: a $1 recognizer for user interface prototypes[END_REF] or even for deriving performance models [START_REF] Cao | Modeling human performance of pen stroke gestures[END_REF]. We purposely did this to ensure motor learning for all gestures so that participants would reach execution automaticity. Participants were allowed to take as many breaks as they wished. The experiment took approximately 40 minutes.

Post-Experiment Questionnaire

After the experiment, participants answered a short questionnaire regarding their perceived execution difficulty when performing the gestures. We gathered this information in two different ways: an individual execution difficulty Rating for each gesture using a 5-point Likert scale; and an ordered Ranking of all gestures according to relative execution difficulty. The 5-point Likert scale rating question (Table 1) was presented as a 5 column table: participants entered ratings for the 18 gestures in any order they chose. Participants were asked to enter the rating by drawing the gesture in the column corresponding to the desired Likert rating. We hoped this would allow them to re-enact the gesture performance and make visual inspection easy. They could modify previous ratings at any time until they were confident of their final choices. The ordered ranking of all gestures according to ascending execution difficulty was completed after the Likert rating. This enabled participants to use the rating classes to assist with this otherwise difficult task. As before, we asked them to draw the gestures in order to revisit relative differences in difficulty as they completed the ranking.

We also asked participants to explain their perception of gesture difficulty: what they found difficult or easy for each gesture execution. Finally, we asked them to identify which shapes they found Familiar (they had seen and practiced before) in order to test our choice for familiar and unfamiliar gestures.

Results

We found a high degree of agreement between participant Rating of execution difficulty (Kendall's W=.781 , χ 2 (17)=185.60, p<.001). The agreement was even stronger for Ranking which participants commented as being a difficult task (W=.82, χ 2 (17)=195.17, p<.001). Both coefficients are well above 0.5 indicating our sample size was appropriate with a large Cohen effect. Since Rating was designed to be used as a first approximation for Ranking, there was a significant correlation between their median ratings (ρ (N=18) =.97, p=.01).

Fig 3 illustrates the median Rating and Ranking ratings for each gesture. A repeated-measures Friedman's ANOVA was used in order to test the influence of gesture type (nominal with 18 cases) over Rating and Ranking. The results showed a significant effect of Gesture over both Rating (χ 2 (17)=185.60) and Ranking (χ 2 (17)=195.17, at p<.001). 3. Left: median gesture Rating (higher Rating values were perceived to be more difficult to execute). Right: median gesture Ranking (higher numerical Ranking for gestures perceived to be more difficult to execute). In both graphs, gestures are ordered by ascending Ranking. Across all 14 participants there were 17 deviations (6.7% of the total responses) from our gestures set's assumed Familiarity. 14 deviations were assumed unfamiliar gestures: 7 participants found the twirl-omega gesture familiar, 4 reversed-pi, 2 flower, and one participant said the sail-boat and steep-hill were also familiar. The latter also noted that the assumed-to-be-familiar gestures a and g were unfamiliar because the starting point was not in the same location where they usually start those letters. As part of their comments regarding their perception of gesture difficulty, three participants noted the same issue of starting position with a and g and one participant with 8, but they did not feel this made them unfamiliar. This relates to the problem of allographic variation in handwriting where individual differences in the formation of character shapes pose problems for handwriting recognizers [START_REF] Schomaker | From handwriting analysis to pen-computer applications[END_REF]. Aside from twirl-omega where Familiarity deviations occurred with half of our participants, our assumed gesture familiarity was reasonable. We could treat these deviations as outliers since they represent less than 4% out of the total responses, but when possible Familiarity related analysis is based on actual participant responses.

The median Ranking and Rating across all familiar and all unfamiliar gestures (Fig 3) are significantly different according to a Wilcoxon signed-rank test (z (N=14) =-3.402, p=.001 for Rating and z (N=14) =-3.400, p=.001 for Ranking, both with large effects, r=-.64). These 9 assumed familiar gestures are among the 11 gestures assigned to the easiest Rating levels, and are among the lowest 10 gestures in ascending difficulty Ranking (Fig 3). The twirl-omega and reversed-pi (two out of three contentiously unfamiliar gestures) also share the two easiest median Rating levels, and reversed-pi has the same median ranking as the familiar gesture g.

Towards Estimating Execution Difficulty

Given the high agreement of perceived execution difficulty Rating and Ranking in experiment 1, we can search for a way to estimate difficulty in the absence of a formal experiment. Essentially, if a correlation exists with one or more characteristic gesture descriptors, then those descriptors can be used to estimate execution difficulty. We examined many potential descriptors (Table 2): all of Rubine's static geometric descriptors and measured quantities [START_REF] Rubine | Specifying gestures by example[END_REF], the additional geometric descriptors used by Long et al. [START_REF] Long | Visual similarity of pen gestures[END_REF], Hu invariant spatial curve moments commonly used in image processing for contours and shapes [START_REF] Pratt | Digital Image Processing[END_REF](p. 606), Isokoski's complexity measure [START_REF] Isokoski | Model for unistroke writing time[END_REF], and the production time predicted by Cao and Zhai's CLC model [START_REF] Cao | Modeling human performance of pen stroke gestures[END_REF]. The calculation of the Rubine, Long et al., and Hu descriptors are straightforward to apply to the geometric shape of the gesture, given the descriptions and equations in the cited works. We computed these measurements using two representations of geometric gesture shapes. To approximate a design scenario where the gestures have been drawn, but not performed, we used the target gesture shapes displayed in the left panel of our experimental application (i.e. the vector drawings in Fig 1). We will refer to these as geometric descriptors using Drawn representations. We also computed mean descriptors using the actual gesture geometries as performed by the participants in our experiment. Theoretically, this is a best case scenario for geometric descriptor performance, but with the potential issue of overfitting. We will refer to these geometric descriptors using Performed representations. Both Drawn and Performed representations were preprocessed similar to previous work [START_REF] Cao | Modeling human performance of pen stroke gestures[END_REF][START_REF] Kristensson | Shark2: a large vocabulary shorthand writing system for penbased computers[END_REF][START_REF] Wobbrock | Gestures without libraries, toolkits or training: a $1 recognizer for user interface prototypes[END_REF] by normalizing without deformation, centering on the origin, and re-sampling uniformly into n=32 points. To calculate the CLC predicted production time, we used the PlayCLC program 2 . As noted earlier, the definition and calculation of Isokoski's complexity measure is ambiguous. By studying examples [START_REF] Isokoski | Model for unistroke writing time[END_REF](p. 360) we developed quantitative guidelines to perform the necessary reduction of arcs into line segments: if the angle α inscribed by an arc was greater than 270° use 3 segments; if α<120° use 1 segment; otherwise use 2 segments. We could verify these guidelines with our 3 and circle shapes, also included in Isokoski's examples.

Note that all descriptors based on geometry are static and will not change with practice. For example, a geometrically complex, but familiar gesture such as g may have a lower Rating compared to a geometrically simple, but unfamiliar gesture such as sail-boat. Rubine's Production Time and Speed descriptors are measured, i.e. they are computed from data gathered during actual gesture performance, so they include effects for practice. Of course, using this type of post-hoc measure for a-priori prediction seems paradoxical. Our initial rationalization is that some future model may be able to accurately predict these measures (such as an improved CLC model for Production Time), and we show later that the relevant measure of Production Time can be approximated with a very small set of informally gathered user data.

All of the potential descriptors in Table 2 were tested for correlations with execution difficulty Rating and Ranking. This was done overall, as well as separately with familiar and unfamiliar gesture groups. Descriptors with at least one significant Spearman correlation coefficient are listed in Table 3 (for geometric descriptors using Drawn representations in Fig 1 ) and Table 4 (for geometric descriptors using participant Performed representations). Production time has the highest correlations with Rating and Ranking overall; and, in all but one case, it is among the highest correlations when tested separately with familiar and unfamiliar gesture groups. Speed had the second highest (negative) correlation when all gestures were considered together, but not significant when tested separately with familiar and unfamiliar.

Note that there is evidence that production time should be a scale invariant.Viviani and Terzuolo [START_REF] Viviani | 32 space-time invariance in learned motor skills[END_REF] found that execution times for single strokes in handwriting are scale invariant. If we accept that a single stroke gesture is similar, then scale invariance should not be problematic. Isokoski [START_REF] Isokoski | Model for unistroke writing time[END_REF] also provides additional evidence with his observation that average velocity increases with longer strokes. In many cases, descriptors based on geometry had significantly lower correlation coefficients compared to measured values. An exception is length, which has all significant coefficients in Table 4 and all but one in Table 3. In the case of familiar gestures in Table 4, coefficients for length, along with density2, and cosine2 are not significantly different from actual production time. Although not significantly highest, Isokoski's complexity and two bounding box descriptors in Table 4 correlate reasonably well when all gestures were considered together, but are not even significant when tested separately with familiar and unfamiliar. In Table 3, some geometric descriptors such as the two bounding box descriptors and cosine2 correlate very well with unfamiliar gestures. Intuitively, the larger gestures may be more complex, and thus be more difficult to execute, but the high correlation of cosine2 is surprising. With low N values (8 for unfamiliar and 9 for familiar), there will be fewer significant differences between descriptors. The tendency for geometric descriptors to exhibit higher coefficients in either familiar or unfamiliar gesture groups is most likely because they cannot adapt to the effect of practice. This is similar to reasons given for the under-or over-estimation behavior of the CLC model [START_REF] Cao | Modeling human performance of pen stroke gestures[END_REF][START_REF] Castellucci | Graffiti vs. unistrokes: an empirical comparison[END_REF].

Visual inspection of the most promising descriptors provides some intuition for their relative performance in predicting difficulty (Fig 4). Gestures are listed by ascending median Ranking on the horizontal axis, so a monotonic trend would suggest it is a good candidate for estimating Ranking. Actual production time ascends almost monotonically with Ranking demonstrating that gestures rated as being more difficult to execute have a greater production time. The static geometric descriptors for the most part increase with difficulty overall, but irregularities are much more pronounced suggesting a weaker fit. For example, letters a, g and m have long lengths, yet they are rated as easy to execute. This again speaks to familiarity: despite objective complexity, practiced gestures are rated with lower execution difficulty. There are also significant correlations between descriptors. Production time is correlated with length (ρ (N=18) =.89, p=.01) and Isokoski's complexity and production time are correlated with length (ρ (N=18) >.70, p=.01). This suggests a partial correlation between these three descriptors, so it is appropriate to test for shared variance. When controlling for production time, the other parameters are no longer significant (p>.05). When controlling for all but production time, production time was still found highly correlated with Rating (ρ (N=18) =.73) and Ranking (ρ (N=18) =.67) at p<.01. For familiar and unfamiliar groups, none of the correlations with Rating and Ranking were significant when either variable was controlled during partial correlations. The tstatistic for comparing coefficients [START_REF] Chen | Correlation: Parametric and nonparametrized measures[END_REF] showed a significant difference between coefficients for Rating (t(15)=5.92) and Ranking (t(15)=4.02) at p<.01.

The poor performance of the CLC predicted production time is somewhat surprising. Previous results found CLC to be highly accurate for first-order predictions when comparing relative ratios of gesture set production times [START_REF] Cao | Modeling human performance of pen stroke gestures[END_REF][START_REF] Castellucci | Graffiti vs. unistrokes: an empirical comparison[END_REF]. So, we expected it would also perform well with a similar first-order prediction task for execution difficulty Ranking, but it has no significant correlations with Ranking at all. To investigate further, we directly compared the CLC predicted production times to actual production times. For magnitude, we found a significant, but low correlation (R 2 =.37, p=.01). For relative ranking, we also found a significant, but low Spearman correlation (ρ (N=18) =.53, p=.05).

Production time is the best indicator of execution difficulty, but the CLC model is not able to accurately predict performance time for our purposes. So, we continue the development of execution difficulty estimation rules based on actual production time, with the assumption (and caveat) that we are at the moment using a post hoc measured value. Later, we show that a small sample of data will provide suitable estimations of production time.

We present two rules for estimating execution difficulty based on production time. The first is a simple rule which compares two candidate gestures according to relative execution difficulty (as Ranking does), and the second uses Bayes' rule to classify a gesture into one of five categories of execution difficulty (such as those provided by the Rating measure).

Rule 1: Relative Difficulty Ranking

Gesture A is likely to be perceived as more difficult to execute than gesture B if the production time of A is greater than that of B:

time(A) > time(B) suggests Ranking(A) > Ranking(B)
To test this rule, we applied it to each pair of gestures (A,B) out of the (18x17)/2=153 possibilities in experiment 1 using the measured production time and counted how many times the rule was correct out of the total number of classification attempts (Ranking accuracy). The rule predicted the relative ranking correctly with 93% accuracy (11 errors out of 153 tests).

Rule 2: Classifying Difficulty Rating

Mapping from production time to one of our five difficulty classes (C i , i=1..5: very easy, easy, moderate, difficult, and very difficult) is a pattern classification problem where each gesture is represented by a single feature, in our case production time. A common technique in statistical pattern recognition is Bayes' rule that minimizes classification error [START_REF] Webb | Statistical Pattern Recognition[END_REF]. Bayes' rule uses each class-conditional density probability (i.e. the probability for a randomly chosen pattern x to lie in class C i , denoted p(x|C i )) together with the a priori probability of class C i (or how likely it is to observe a pattern from this class, denoted p(C i )). Using this data, Bayes' rule computes the a posteriori probability of x belonging to each class, p(C i |x), and assigns x to class C j for which the a posteriori probability is maximum:

( ) ( ) { } i i i j C p C x p j C x ⋅ = ⇐ ∈ = | max arg 5 , 1 (1)
In order to apply Bayes' rule, the conditional p(x|C i ) and a priori p(C i ) probabilities must be known for each of our 5 Rating classes. Normal parametric models are frequently assumed in practice (equation 2) for estimating the unknown conditional densities p(x|C i ) [START_REF] Webb | Statistical Pattern Recognition[END_REF](p.34) for which the parameters (mean µ i and standard deviation σ i ) can be easily computed from the training set (in our case, data from experiment 1).

(

) ( )

        - - = 2 2 2 2 exp 2 1 | i i i i x C x p σ µ πσ (2)
The a priori probabilities p(C i ) are estimated from the training set as the percentage of samples falling into each class [START_REF] Webb | Statistical Pattern Recognition[END_REF](p.34-39). In our case, µ i are the mean production times for each Rating class (expressed in seconds); σ i the standard deviations (seconds); and p(C i ) the percentages of samples belonging to each Rating class. Table 5 lists these parameters as computed from our training data (experiment 1) with an illustration of each normal model superimposed over the production time histogram. We tested Bayes' rule in order to see how good it fits our data. We counted how many times the rule was correct out of 18 classification attemps (the Rating accuracy) by applying it to each gesture in our set. The rule achieved an accuracy rate of 83% on its own set (15 gestures were correctly classified to their Rating category as indicated by the participants). The three errors occurred for the strike-through, turn-90, and sail-boat gestures, all of which were misclassified to the next lower class. This confirms for now a good model fit for our data while Section 9 will show how the rule applies for new gestures in our validation experiment. The mean production times µ i for each Rating level (see Table 5) could be approximated to more reasonable timestamps such as 1, 1.5, 2, 2.5 and 3.5 seconds (the µ i simplified column in Table 5). These could represent more intuitive working estimates for each Rating class to be used by designers. When using these mean values with the computed standard deviations as before, we also obtained 83% classification accuracy.

Estimating Production Time

Applying our rules using measured production time works very well, but we would like designers to estimate production time without running such a formal experiment. Ideally, this could be done with predictive models. However, using times predicted by CLC, Ranking accuracy dropped to 67% and Rating down to 28%. Although Isokoski does not predict actual time, it can be used for relative Ranking where it managed a prediction accuracy of 82%.

Examining the data from experiment 1, we found that individual participant gesture production times are highly correlated with overall mean production times ρ (N=18) =.96, p=.01 (min .92, max 1.0). This consistency made us wonder if a designer could estimate difficulty based on only few samples of measured production time. Instead of a long formal experiment, a few people could perform the candidate gestures a few times in a simple data gathering application. Even more, this data is likely to already exist for training the gesture recognizer [START_REF] Li | Protractor: a fast and accurate gesture recognizer[END_REF][START_REF] Rubine | Specifying gestures by example[END_REF][START_REF] Wobbrock | Gestures without libraries, toolkits or training: a $1 recognizer for user interface prototypes[END_REF].

We first consider the minimal case of gathering data from a single person. Again using data from experiment 1, for each participant, we randomly selected M out of 20 execution samples for each gesture to calculate a mean production time. Using these mean times, we apply our rules and compute the prediction accuracy for Rating and Ranking. The random selection was repeated 100 times as M varied from 1 to 20: thus 14 participants x 18 gestures x 20 M values x 100 repetitions = 504,000 predictions.

The mean accuracy for Rating begins to out at M=3 near 53%, and Ranking also approaches 91% (Fig 5 ,left). The effect of M over Rating is significant (χ 2 (19)=476.4, p<.001). A Wilcoxon signed-rank test found significant effects between [START_REF] Appert | Using strokes as command shortcuts: cognitive benefits and toolkit support[END_REF][START_REF] Rubine | Specifying gestures by example[END_REF], [START_REF] Bau | Octopocus: a dynamic guide for learning gesture-based command sets[END_REF][START_REF] Rubine | Specifying gestures by example[END_REF] and [START_REF] Castellucci | Graffiti vs. unistrokes: an empirical comparison[END_REF][START_REF] Rubine | Specifying gestures by example[END_REF] with a small Cohen effect (r<.3). The effect of M over Ranking was significant (χ 2 (19)=4140.54, p<.001) with significant differences between (1,20) (r=.52), [START_REF] Bau | Octopocus: a dynamic guide for learning gesture-based command sets[END_REF][START_REF] Rubine | Specifying gestures by example[END_REF] and [START_REF] Castellucci | Graffiti vs. unistrokes: an empirical comparison[END_REF][START_REF] Rubine | Specifying gestures by example[END_REF] with medium effects (r<.5). With 3 samples, mean Rating accuracy was 53% (SD 18%) and mean Ranking accuracy 89% (SD 3%). We continue our analysis by varying the number of participants N=1..14 given M=1,3,5 individual gesture execution samples from each. Similar to before, we randomly selected the gesture samples 100 times for each N: thus 14 participants x 18 gestures x 3 M values x 100 repetitions = 75,600 predictions.

The mean accuracy of Rating increases from 52% using one participant to 77% (significant, χ 2 (13)=496.45, p<.001) when data from all participants is used ( Fig 5,right). The same trend is observed independently for M=1,3, and 5 executions from each participant. The accuracy of Ranking increases from 88% to 93% (χ 2 (13)=715.1, p<.001). The effect of M was found significant for both Rating and Ranking (at p<.001) but the Wilcoxon signed-rank test showed small Cohen effects between (1,3) and (1,5) r<.3 and very small between (3,5) r<.15. With 3 participants and 3 execution samples mean Rating accuracy was 66% (SD 14%) and mean Ranking accuracy 91% (SD 2%). With 5 participants and 3 execution samples mean Rating accuracy was 70% (SD 13%) and mean Ranking accuracy 92% (SD 2%).

In summary, on average, a designer could estimate a relative Ranking of execution difficulty with 89% using 3 gesture execution samples from a single person. To estimate Rating, 3 execution samples from 3 or 5 people are needed to achieve mean accuracies of 66% and 70% respectively.

Conclusions and Future Work

Reducing gesture execution difficulty is an often mentioned goal of gesture set design. Our work provides support for this argument with empirical evidence showing that people tend to have similar perceptions of execution difficulty, that it is highly correlated with gesture production time, and that difficulty can be estimated using two simple rules for relative ranking and a classification rating. Because existing models cannot accurately predict the magnitude of production time necessary for our classification rule, we provide evidence that an estimate of production time using only a few execution samples from a few people is good enough. Moreover, this set of estimation data may already exist when designers train a recognizer. Designers can use our quantitative rules as they are when selecting from candidate single stroke pen gestures. However, we plan to make this process more automatic, by incorporating our difficulty estimation into the popular $1 gesture recognizer [START_REF] Wobbrock | Gestures without libraries, toolkits or training: a $1 recognizer for user interface prototypes[END_REF]. As future work, we also plan to examine how execution difficulty relates to multi-stroke pen gestures and multi-touch gestures.

Participants

  14 right-handed people (3 females) participated in the experiment (mean age 21 years, SD 1). 11 out of 14 participants had no pen-based interface experience. Apparatus Gestures were entered using a 17 inch (431 mm) Wacom DTU-710 Interactive Pen Display running at a resolution of 1280 x 1024 px (pixel pitch 0.264 x 0.264 mm) and capable of capturing pen input at 133Hz. The display was positioned horizontally to approximate a physical pen and paper context. A 2.4GHz computer ran a C# full screen application. The participant entered gestures in a 420 x 420 px (110 x 110 mm) square box centered in the display (Fig 1).

Fig. 1 .

 1 Fig. 1. Experiment Application: (a) current gesture to perform; (b) gesture input area; (c) postentry choice buttons.

Fig. 2 .

 2 Fig. 2. The 18 gestures used in the experiment: (a) left 9 designed to be familiar; (b) right 9 designed to be unfamiliar.

  Fig.3. Left: median gesture Rating (higher Rating values were perceived to be more difficult to execute). Right: median gesture Ranking (higher numerical Ranking for gestures perceived to be more difficult to execute). In both graphs, gestures are ordered by ascending Ranking.

1 . 15 .

 115 Cosine of initial angle (cosine1) 2. Sine of initial angle (sine1) 3. Size of bounding box (bbox size) 4. Angle of bounding box (bbox angle) 5. Distance between first and last points 6. Cosine of angle between first and last points (cosine2) 7. Sine of angle between first and last points (sine2) 8. Total length 9. Total turning angle 10. Total absolute turning angle (turn angle) 11. Sharpness or (energy) Total angle traversed / total length 16. Total angle / total absolute angle 17. Distance between first and last points (

Fig. 4 .

 4 Fig. 4.Visual comparison of the four most promising measures and predictors (y-axes) with actual ascending median gesture Ranking (x-axis). A monotonic trend suggests the measure or predictor is a good candidate for estimating Ranking (e.g. mean measured time). NOTE: Error bars in all figures represent 95% CI.

Fig. 5 .

 5 Fig. 5. Left: prediction accuracies for Rating and Ranking vs. number of execution samples. Right: Difficulty prediction accuracies vs. number of participants.

Table 1 .

 1 Likert questions used to elicit execution difficulty Rating.

	Likert rating	Associated explanation
	1. very easy to execute	I executed these gestures immediately and effortlessly
		with absolutely no need to pay attention
	2. easy to execute	I executed these easily, almost without paying attention
	3. moderate difficulty	I occasionally paid special attention during execution
	4. difficult to execute	I paid special attention with each execution
	5. very difficult to execute	I had to concentrate for each execution. There were times
		when I did not get the right shape from the first attempt

Table 2 .

 2 Descriptors (bold indicates significant correlation with Rating or Ranking).

Table 3 .

 3 Correlations of geometric descriptors using Drawn representations. Spearman correlation of descriptor with median Rating and Ranking in descending order of overall Rating coefficients; coefficients are reported at p = .01 (**) and p = .05 (*) significance levels; N = 18 for all, N = 9 for familiar and N = 8 for unfamiliar gestures (twirl-omega was excluded). The largest coefficient in each column is shown in bold text (two bold coefficients in the same column are not significantly different).

		all		familiar	unfamiliar
		Rating	Ranking	Rating	Ranking	Rating	Ranking
	bbox size	.78**	.75**	n.s.	n.s.	.93**	.98**
	bbox area	.72**	.70**	n.s.	n.s.	.93**	.98**
	length	.60**	.60**	n.s.	.67*	.79*	.86**
	cosine2	n.s.	n.s.	.73*	.81**	-.86*	-.88**
	density1	n.s.	n.s.	n.s.	n.s.	.73*	.81*
	Hu2	n.s.	-.50*	n.s.	n.s.	n.s.	n.s.

Table 4 .

 4 Correlations of geometric descriptors using Performed representations. Correlations reported as in Table3.

		all		familiar	unfamiliar
		Rating	Ranking	Rating	Ranking	Rating	Ranking
	time	.95**	.96**	.94**	.84**	.79*	.91**
	-speed	.87**	.85**	n.s.	n.s.	n.s.	n.s.
	length	.80**	.82**	.94**	.90**	.72*	.81*
	bbox size	.77**	.82**	n.s.	n.s.	n.s.	n.s.
	Isokoski	.74**	.71**	.70*	n.s.	n.s.	.79*
	bbox area	.70**	.75**	n.s.	n.s.	n.s.	n.s.
	density2	.56*	.52*	.90**	.85**	.72*	.76*
	turn angle	.53*	.51*	n.s.	n.s.	.72*	.83*
	Hu2	-.48*	-.47*	n.s.	n.s.	n.s.	n.s.
	CLC	.47*	n.s.	n.s.	n.s.	n.s.	.79*
	aspect	-.47*	n.s.	n.s.	n.s.	n.s.	n.s.
	cosine2	n.s.	n.s.	.86**	.71*	-.86**	-.88**
	density1	n.s.	n.s.	n.s.	n.s.	.79*	.86**
	energy		n.s.	n.s.	n.s.	n.s.	.79*

Table 5 .

 5 Left: Bayes' Rule Parameters for the Rating Classification Rule. Right: Production time frequency histogram with superimposed time normal models for each Rating.

	Rating		Bayes' Rule Parameters
	levels	µi	σi	p(Ci)	µi simplified 1
	very easy	1.18 0.43 27%	1.0
	easy	1.65 0.58 28%	1.5
	moderate	1.97 0.62 21%	2.0
	difficult	2.48 0.95 16%	2.5
	very difficult 3.46 1.38	8%	3.5

1 simplified values represent reasonable approximations for the mean times µi; see the text for explanation and results.

Table 6 .

 6 Validation experiments results: Ranking and Rating estimation accuracies using both measured and estimated production times.

	Production time		Estimation Accuracy Ranking Rating
	Measured		93.0%	90.0%
	Estimated (3 executions)	x 1 participant x 3 participants x 5 participants	89.6% 90.5% 91.3%	66.9% 74.6% 79.8%
	Predicted	Isokoski CLC	87.0% 75.0%	n/a 25.0%

Kendall's coefficient of concordance W in [0..1] where 0 denotes no agreement at all and 1 represents absolute agreement.

from http://www.cs.toronto.edu/~caox/PlayCLC/PlayCLC.htm

Acknowledgement

This paper was supported by the project "Progress and development through postdoctoral research and innovation in engineering and applied sciences-PRiDE -Contract no. POSDRU/89/1.5/S/57083", project co-funded from European Social Fund through Sectorial Operational Program Human Resources 2007-2013.

Experiment 2: Validation of Difficulty Estimation Rules

A second experiment, similar to the first, was used to validate our execution difficulty rules as well as our simple production time estimation technique. The same apparatus, task, and design were used, but with 20 different gestures (

Results

We found the same high level of correlation between participants' difficulty Rating (Kendall's W=.78, χ 2 (19)=163.61, p<.001) and Ranking (W=.80, χ 2 (19)=166.79, p<.001). Rating and Ranking were again highly correlated (ρ (N=20) =.94, p=.01).

Estimates of Execution Difficulty

We first establish an accuracy upper bound using the actual measured production times logged in the experiment. To test the accuracy of estimating Ranking using Rule 1, we ordered the gestures in ascending order of production time, and correlated the resulting ranks with the median participant Ranking. Again, there was a strong correlation (ρ (N=20) =.94, p=.01). Then, we applied Rule 1 for each pair of gestures (A,B) out of the (20x19)/2 = 190 possibilities, and calculated an accuracy rate (how many times the estimate was correct). In this way, estimating Ranking using Rule 1 attained 93% accuracy: 14 errors out of 190 tests. For Rule 2, we used the simplified Bayes parameters generated from Experiment 1 (Table 5). Estimating Rating using Rule 2 attained 90%: 18 gestures were correctly classified according to median participant Rating. The rectangle gesture was classified as easy instead of very easy to execute, and tree was classified as easy instead of moderate (both were shifted by one Rating class).

Next, we tested the accuracy of our rules using an estimate of production time generated from a small number of samples. Based on our analysis in the previous section, we tested N=1,3,5 participants and M=3 gesture execution samples. Rating accuracies varied from 66.9% to 79.8% while Ranking increased from 89.6% to 91.3%. Table 6 shows the accuracy rates obtained. We also re-tested using CLC and Isokoski for input to the model. CLC still produced a low Rating accuracy of 25%, but it performed better for Ranking with 75% accuracy. Isokoski did very well with 87% for Ranking, but cannot be used to estimate Rating. Overall, our rules to estimate difficulty performed well with our validation data, even when using only three samples from three participants as an estimate of production time.