Tim-Joachim Jensen

Olivier Baverel

Cyril Douthe

Morphological and mechanical investigation of interconnected gridshells

This paper describes the structural reinforcement of grid shells by interconnecting several gridshells together. Reference for the present investigation is taken from the composite (GFRP) gridshell structure built for the Forum of the Solidays music festival in Paris in 2011. The principle of interconnection is illustrated with various structures which are generated using a grasshoppper components developed by the Navier laboratory for the automatic meshing of free-forms structures on Rhino. Then the effect of the interconnection on the structural behaviour is briefly discussed based on elementary loading cases. Finally, the feasibility of the concept as well as its architectural and morphological potential is show by the construction of a double gridshell prototype. The authors conclude on the possible future developments of such morphologies which could give interesting and unexpected architectures.

Introduction

The Navier laboratory has participated to the design and construction of the first composite (GFRP) gridshell building for a public event, the Solidays music Festival in june 2011 (see figure 1), sponsored by academic (ENPC), caritative (Solidarité Sida) and industrial partners (T/E/S/S, Viry) [START_REF] Baverel | Gridshells in composite materials: Construction of a 300 m2 forum for the solidays' festival in Paris[END_REF]. It was made possible with a team that has worked on (GFRP) gridshell knowledge for about ten years [START_REF] Douthe | Gridshell structures in glass fibre reinforced polymers[END_REF][START_REF] Douthe | Gridshell in composite materials: toward wide span shelters[END_REF][START_REF] Douthe | Form-finding of a grid shell in composite materials[END_REF][START_REF] Douthe | Study of slender prestressed structures in composite materials: application to the conception of gridshells[END_REF]. Speaking of structural types, the word gridshell commonly describes a grid structure having the shape and the rigidity of a double curvature shell. In the present case, the word gridshell will be used for elastic gridshell meaning there that the form is obtained by elastic deformation of a two-way grid initially flat. At the end of the forming process, the deformed grid is rigidified, using presently a third direction of beams.

Figure 1: Aerial view of the gridshell for the Solidays music festival (2011)

In this paper, a morphological investigation of several gridshells that intersect each other is presented, originally aiming at improving the structural behaviour of such structures. The gridshell built for the Solidays festival is taken as a reference for the various interconnected gridshells with similar spans which will be proposed. In the following section, the numerical tools used to adjust the form, to take into account the mechanical constrains and the method to mesh the form are presented. In the third section then, different cases of interconnected gridshells are shown and key issues of their mechanical behaviour are illustrated by comparison with the configuration of the Solidays structure. In the fourth section, the feasibility of the concept of two interconnected gridshells is practically studied by constructing a prototype during a workshop organized with the master students.. Finally, the morphological potential is illustrated before concluding on the general advantages of such configurations.

Experimental Feedback on the Solidays Building

As a guideline, the designer has to concentrate his efforts on three important points:

• That the curvature in each bar is not too high;

• That the entire surface is meshed;

• That the mesh does not get too concentrated locally.

Global and local transformation of the surface

Figure 2 shows the first drawing steps with the possible transformation of the freeform surface which must be meshed on Rhino and which actually ressemble a half-peanut with two domes and a curvature inversion between them. This surface is defined as a patch on the contour polylines (visible on figure 2 (A) which defines the perimeter in plan and on some contour polylines in elevation which defines the height of the building [START_REF] Rhinoceros | Nurbs modelling for Windows[END_REF]. The patching command depends on a stiffness parameter which govern the smoothing of the surface. For the surface in figure 2, the parameters are the following: Stiffness, k=5, Surface U Spans=10, Surface V Spans=10; (the red line are the support curves for the patch). If necessary, this surface can be modified locally by displacing the surface control points according to the designer wishes (see figure 2,B). It must be noted here that if the sample point spacing of the patch surface is too high, the manipulation of the control points gets too precise and inappropriate for the definition of a smooth surface.

Figure 2: Aerial view of the patch stiffness (A) and the control point transformation (B)

Geometrical constraints due to the structural behaviour

The main stresses in the gridshell are due to the bending in the beams due to the forming process (not to variable external loads) [START_REF] Douthe | Gridshell in composite materials: toward wide span shelters[END_REF][START_REF] Douthe | Form-finding of a grid shell in composite materials[END_REF]. The geometry of the surface to be meshed imposes thus the stress distribution in the gridshell members. These stresses are inversely proportional to the curvature and are given by the expression:

comp flex flex E v R ⋅ σ = σ + σ ≈ σ =
where σ denotes the stress in MPa, E the Young modulus in MPa, v the distance to the neutral axis of the member in m and R its radius of curvature in m. For a given material (here the GFRP tubes used for the Solidays structure) this stress must remain below a certain limit (σ max =200 MPa). Thus for a given section (here a 48mm diameter tube), the above equation can be transformed into a geometrical constrain:

max min min max v E v E R ( 3.28m) R ⋅ ⋅ ≤σ ⇒ ≥ = σ
As the extreme radii of curvature R min and R max can be estimated easily by Rhino, it is possible to handle the surface in order to keep its curvature below a certain level insuring hence that a mesh will be feasible. Indeed figure 3 shows a comparison between stresses in the grid and curving radii of the surface with R min = 3 m and R max = 8.7m)..In figure 3(A), the local stress (in red) located in the neighboring of the doors must be disregarded as local strengthening have been added in those parts. This being said, it can be remarked that the most loaded member are submitted to stresses between 100 and 140MPa. These members are located on the blue regions of the curvature diagram (figure 3(B)) which corresponds to where the lowest radii. This observation is a good starting point for the design of the surface but does not presume of the mechanical behavior of the structure under self-weight or external forces which must still be investigated. It just can be guessed that the most flat areas (in red on figure 3(B)) will form the weakest zones of the structure when loaded.

Figure 3: Comparison between the prestresses in the grid (A) and the minimum radii of the surface (B) 2.3. Meshing of the Surface

The "compass method" used to generate the grid consists in constructing a network of parallelograms on a given surface. This method was described in IL10 Gitterschalen of Frei Otto et al [START_REF] Frei | IL10 Gitterschalen[END_REF]. Figure 4 shows the different steps of the method on a plane surface. The task is to construct a grid of parallelograms on a surface with a compass. Two arbitrary intersecting curves or generators are first laid on the surface. Then, a mesh width is selected and serves as compass radius. The spacing of the grid is marked along each axis, starting from the point of intersection of the axes. Afterwards, the nodes are determined by the intersection of two circles drawn around each of the neighboring points. Then, gradually, new points are determined in the same way. Finally the nodes are connected rectilinearly.

Figure 4: Principle of "compass method" (after IL10 [START_REF] Frei | IL10 Gitterschalen[END_REF])

For non plane surfaces, the principle of the construction of the grid is exactly the same than previously. This method leads to a grid that fits the 3D surface and allows hence in a certain way for the "development" of non-developable surfaces. It has been implemented numerically in grasshopper for Rhino to mesh free forms and an illustration of it is shown in figure 5 (with in dark grey the patch surface, in light grey the cutting surface for the meshing, in red the director polylines for the "compass method" meshing, in black the main lines of the meshing and in light grey the lines for the third/fourth direction of the meshing). It can be seeen that the position and the geometry of the director lines on the patch surface as well as the chosen step define a specific grid. The direction of these polylines should as possible follow the geometry of the form: a bad choice of this director polylines creates a nonharmonious grid or an incomplete grid (see figure 5,B) with local concentration of the mesh. Although one could think of possible automation of the generation of optimal meshes, the search for a suitable mesh is here done manually.

Mechanical behaviour

The mechanical behaviour of the structure has then been studied. The reference grid was generated following the compass method based on the two generators shown on figure 5A and a mesh width of 1 m. This led to a total length of beams of approximately 1200 m for the main grid and 1600 m for the triangulation (here in both directions contrary to the real Solidays building). For the present study, the actual entrances of the structure are not considered and boundary conditions are thus simple hinged supports on the reference plane for all members extremities. Concerning loading conditions, a single representative case has been investigated: it is composed of the self weight of the structure and an equivalent snow load of approximately 40 daN/m² transformed into uniform nodal forces of 25 daN at every nodes. Two analyses are conducted (with the software Autodesk Robot Structural Analysis):

an elastic linear analysis and a linear buckling analysis. For these two calculus, the initial bending prestress has been neglected (for simplicity reasons and also because current research of the authors tends to show that the prestress plays a secondary role in whole stability of the grid).

The results of the linear analysis are shown in figure 6. It appears that the deformations concentrate mainly in two areas: the first one in the inner central part of the peanut, the other in the outer central part. The comparison of this figure with that of figure 3B shows that these area correspond to the two zones where the curvature is the smallest. Structural analysis hence confirms the initial intuition that flat areas constitute the weakest points of the structure. This intuition is also verified by the linear buckling analysis which shows that the first ten buckling modes are all located in those areas (figure 7). Modes 1 to 4 concerns the inner area A, mode 5 zone B, mode 6 zones A and B, modes 7 and 8 zone C and modes 9 and 10 the three zones. Typical load factors are 5 for mode 1, 10 for mode 5 and 11 for mode 7, so that in its actual form, the structure is safe. -increasing the grid density (which increases self weight and the work required for the construction) -increasing the section of the members (which is actually not a good strategy as it increases also bending prestress and may not be possible for the investigated surface without exceeding the stress limit); -introducing local reinforcements (with for example some additional stiffer members or as will be investigated in next section by intersecting in those areas the gridshell with another gridshell…).

Morphological and mechanical investigation of interconnected gridshells

In this section, the conception of gridshells based on the addition and intersection of surfaces is presented. These intersections and additions are made using various operations presented in figure 8, 11 and 14. The two meshes of these intersecting surfaces are connected along the intersecting lines with hinges similar to those used for the two main grids.

Interconnection of two identical gridshells

The reference patch surface and the director lines for the meshing presented in figure 5A are here duplicated and translated horizontally in one direction (see figure 8B). Then the two patch surfaces and their director lines are scaled in one direction to enlarge the inner space in plan to cover approximately the same area as the reference structure. The distance between the surfaces is limited to two meters and the region of crossing is located on the highest part of each surface where the curvature is the most important. The principle of the duplication is first illustrated on a 2D cut where the black dashed line stands for the reference patch surface, the grey dashed line for the reference clone surface (identical), the black continuous line for the 1D scale of the reference patch surfaces and the black continuous line for the 1D scale of the reference clone patch surface.

Interconnection of two gridshells on the same perimeter

In this case, the patch surfaces are resulting from the transformation of the reference support curves for the patch (see figure 2A). The perimeter of the two surfaces is the reference surface perimeter. The support curves for each patch surfaces (see figure 11A) are drawn between the reference curves supporting the patch (c) and the reference offset curves (d). The distance between the two curves is limited to two meters.

Figure 11: Cut front view (A) and Aerial view (B) of the intersection of two surfaces on the same perimeter

The high curvature on the support curves leads to a reduced minimum radius as can be seen in figure 12: initially R min =3m and R max =8.7m after transformation for the first surface R min = 0.9m and R max =11.2m and for the second surface R min = 1,2m; R max =9.7m.

Interconnection of two homothetic gridshells

For this third illustration, the reference surface is intersected with a larger surface with a lower altimetry (see figure 14). The reference patch surface (a) and the director lines for the meshing presented in figure 2A are offset so that the distance between the surfaces is limited to two meters. Then the offset patch surface with the director lines is scaled in one direction vertically to intersect the reference surface. The region of crossing is located on the highest part (see figure 14) of each surface where the curvature is the most important (see figure 15).

Figure 14: Cut front view (A) and Aerial view (B) of the intersection of the reference surface with a homothetic one

It can be seen in figure 15 that the 3D scaling of the reference surface reduces the global minimum curvature of the surface excepted on the inverted region between the two domes. In this region the minimum radius value increases. The maximum curvature radius increases at the same time on all other regions. It must also be noticed that the intersection line connects the high curvature regions of the both surfaces.

Interconnection of the reference gridshell with its mirror image

In last example, the two patch surfaces are the same than the one presented in the case study 3.1 with the interconnection of two identical gridshells but this time the translation of both surfaces is done in two opposite directions with a mirror effect (figure17). The intersection of both surfaces creates three intersection lines that are approximately located in the regions with large radii of curvature. This results in an architecturally interesting space splitting and also in a reinforcement of the structure in the areas where it is potentially the weakest (from a mechanical point of view).

Mechanical behavior

The four variants of interconnected gridshells have then been submitted to the same loading as the reference gridshell in section 2.4 by simply adapting the snow load, so that only external nodes are loaded. For all variants, the interconnection improved the performance of the initial structure, but not in the same way (see table1) and only the last proposal provided a really efficient solution. Indeed in the first three variants works, the additional gridshell provided a kind of support at the ridge of the initial structure and reciprocally. This could not harm the structural behavior of the whole but did not reinforce directly the weakest areas. On the contrary, in the last variant, the mirror gridshell crossed the three weakest area indentified in figure 7, so that it directly reinforced the structure where needed. When interconnecting gridshells, it is thus essential to identify flat area and to seek to locate interconnections in these areas.

Reference

Variant

Construction of a prototype

Interconnection of two gridshells

In this section, the feasibility of such structures is illustrated through the construction of a prototype which will be based on the intersection of two simple surfaces like in section 3.3 (see figure 18). The surfaces a and b are a patch of two half ellipsoids. The interior patch surface is intersected with a larger and lower altimetry patch surface. On the ground, the distance for the offset is limited at one meter. The curvature radii of the prototype surfaces are then illustrated in figure 19 (where the black line is the intersection line between the two surfaces). For the inner surface, we have R min =1.8m and R max =3m, for the outer surface R min =2.7m and R max =5.2m. Both Grids are meshed with the "compass method" with perpendicular director polylines crossing and lying on top of the patch surfaces. To facilitate the interweaving of the two grids, the director polylines for the meshing of the first patch surface are fixed with an angle of 45° to the grid director polylines for the meshing of the second patch surface (see figure 20).

Construction of the double Grid

The challenge was to build the two Grids on the ground. To facilitate the erection of the two interweaving grids (see figure 21) the mesh width is wider than in the model shown in figure 20. Indeed, initially the mesh width was set at 0,8 meters but finally ended up with a mesh width of 1,6 meters.

Figure 21: Meshing plan of the double Grid on ground before

Practically, both grids were assembled on the ground, using for two different colors for the two surfaces: white for the larger one, blue for the highest one (see figure 22). All connections between members were made with standard scaffolding elements, including connections between the blue beams of the interior gridshell with the exterior white beams of the larger gridshell. Both grids were assembled interwoven, then lifted and finally connected between them. Following, an experimental test of the connection between both gridshells with a local load on the top of 60 kg was conducted and showed that the structure is more rigidwith than without connection. The last step of the construction -that has not been done for this prototype but that is mandatory for a real gridshell structure-should be to stabilize the two meshed forms with a third direction of beams or with stiffening cables in both directions to block the network of parallelograms.

Conclusion

In this paper, an investigation of interconnection of gridshells was presented. After showing the method to control the form and the mesh, different configurations of interconnections of gridshells were proposed. The structural behaviour of the various configurations was compared with the initial structure without interconnections. It showed that if the intersection lines cross the area with the lower curvature of the initial structure, then interconnection provides an efficient alternative way to improve the performance of a gridshell. A report on the experimental prototype of interconnected gridshell was also presented. The construction showed that the erection process is more complex than a normal gridshell. It seems thus that interconnection of gridshell has a good potential in the development of a new generation of gridshells with astonishing interior spaces.

Figure 5 :

 5 Figure 5: Complete (A) and incomplete (B) meshing of the patch surface

Figure 6 :

 6 Figure 6: Initial and deformed shape of the gridshell under uniform snow load.

Figure 7 :

 7 Figure 7: Buckling modes However, one could think of strategies to improve the structural performances of this building, among which:

Figure 8 :

 8 Figure 8: Cut front view (A) and aerial view (B) of the intersection of two identical surfaces

Figure 9 :

 9 Figure 9: Comparison between the minimum radius of the reference surface and the two intersecting surfaces

Figure 10 :

 10 Figure 10: Meshing of the intersecting surfaces

Figure 12 :

 12 Figure 12: Comparison between the minimum radius of the reference surface and the two intersecting surfaces.

Figure 13

 13 Figure13shows then different views of the interconnected gridshell with like previously: (A) inside meshing, (B) outside meshing, (C) inside meshing parallel perspective, (D) outside meshing parallel perspective.

Figure 13 :

 13 Figure 13: Meshing of the intersecting surfaces

Figure 15 :

 15 Figure 15: Minimum radius of the reference surface and the intersecting

Figure 16 :

 16 Figure 16: Meshing of the intersecting surfaces

Figure 17 :

 17 Figure 17: Meshing of the intersecting surfaces

Figure 18 :

 18 Figure 18: Cut front view (A) and Aerial view (B) of the prototype two surfaces a and b

Figure 20 :

 20 Figure 20: Meshing of the intersecting surfaces

Figure 22 :

 22 Figure 22: View of the interweaving grid on the ground and of the two interconnected gridshells

Figure 23 :

 23 Figure 23: Interior view and exterior view by night of the prototype

Table 1 :

 1 Comparison of main characteristic of the mechanical behavior of variants.

	1	Variant 2	Variant 3	Variant 4

Acknowledgments

We would like to thank Jean-François Caron and Frederic Tayeb from the Navier laboratory. For the construction of the prototype we would like to thank Gilles Ebersolt and his master class students Johanna Schmidt, Florentia Christokorov, Mehdi Grosjean, Amine Khodri, Tra Lehuong, Florentin Duroy, Maureen Gerbe, Emilie Anglada, Habib Bencherif, Amir Hossein Shirvani, Maxime Ravaux, Martin Delarue, Quentin Leteurtre and Pauline Mourani (ENSAV). For the prototype construction we also would like to thank the technical team of "Les Grands Ateliers" and the students of ENPC Juliette Adam and Camille Glacet.


Kaustuv Chaudhuri
email: kaustuv.chaudhuri@inria.fr

Subformula Linking as an Interaction Method

come

Introduction

Formal proofs are more fundamentally computational than mathematical. Say we want to prove (a ⊃ b) ⊃ (b ⊃ c) ⊃ (a ⊃ c). Current proof languages are generally always languages of interaction, so a proof is an arrangement of instructions to a stateful interpreter that allows it to build (or check) an underlying proof object in a trusted natural deduction or a sequent calculus formulation of the logic. A formal proof of this theorem is, therefore, something like this; Suppose (1) a ⊃ b, (2) b ⊃ c, (3) a; to show c, we backchain [START_REF] Baelde | Least and greatest fixed points in linear logic[END_REF] to change the goal to b, then we backchain [START_REF] Andreoli | Logic programming with focusing proofs in linear logic[END_REF] to change it to a, which we already have by [START_REF] Bertot | The CtCoq system: Design and architecture[END_REF].

(Most proof languages can express the above more succinctly.) This proof naturally resembles a computational trace where the steps of the computation are the (primitive or derived) inference rules of the logic, possibly with the use of additional lemmas. However, this formal proof obscures the simple mathematical intuition behind the proof, function composition; indeed, the composition is fully unfolded and sequentialized. In order to write the more natural mathematical proof, the user would first have to find a lemma in the standard library (or write one) that implements this intuition.

Because formal proof languages are more closely tied to the underlying calculus, and often to formal theories, they are generally not portable as such across different systems. In the rare instances where two different formal proof systems (take, e.g., Coq and Isabelle) do exchange proof objects, they tend to be low-level "logical bytecode" (λ-terms built internally by the proof tactics or rewriting traces) that bear no resemblance to the proof text a user actually writes and are not expected to be read by humans (some examples: [START_REF] Stump | Proof checking technology for satisfiability modulo theories[END_REF][START_REF] Boespflug | The λΠ-calculus modulo as a universal proof language[END_REF]). Only the most committed (and masochistic) user learns to be proficient in many systems, so the communities of users of formal systems have become rather balkanized. It is worth asking if there is a sense in which one can build an interactive prover free of the shackles of language.

To answer this question, let us begin by noting that a proof fundamentally consists of two varieties of reasoning: reasoning about the subformula structure, and reasoning about links between different subformulas. Examples of the first variety are: to prove the goal A ∧ B create two independent subgoals for A and B, or to use an assumption ∀x. A add an instantiation [t/x]A as an additional assumption. Examples of the second variety are: to prove the goal A search for an assumption A (use of hypothesis), or to prove the goal C first prove A and then show that C follows from A (cut or substitution). The language for establishing the links is surprisingly similar across proof languages; they generally always use hypothesis labels and terms such as apply or assert. Structural reasoning differs widely, however; at one end of a spectrum are languages based on tactics that drive a stateful prover through a proof tree, while at the other end are languages that reify the proof tree textually in the proof document but do not prescribe an order of evaluation. Crucially, though, the entire point of the structural reasoning is to enable the links, which are the only ways to finish and compose proofs and are therefore the essence of a proof, so the surprising design focus on structural reasoning seems misplaced.

How can one make linking the primary aspect of formal proof construction? Unsurprisingly, this question has been asked and answered a number of times, but never satisfactorily. This paper combines two existing answers-proof by pointing [START_REF] Bertot | Proof by pointing[END_REF] and the calculus of structures [START_REF] Chaudhuri | The Focused Calculus of Structures[END_REF][START_REF] Straßburger | Linear Logic and Noncommutativity in the Calculus of Structures[END_REF]-in a way that improves on both and suggests a research direction.

Proof by pointing is the first attempt to systematically construct a non-linguistic interaction method on top of an existing proof interaction language such as the tactics language of Coq [START_REF] Bertot | The CtCoq system: Design and architecture[END_REF]. The user proves a theorem by a sequence of mouse clicks on subformulas; each click brings the indicated formula to the foreground of the current goal, and possibly creates additional background subgoals. Depending on the occurrence of the subformula, each click is interpreted as a sequence of tactics that mimics a sequence of sequent rules. Once a subformula is brought into the foreground on both sides of the sequent arrow, the corresponding link is established and the goal is closed. The problem with the pointing approach appears after this closure: the remaining subgoals that were produced to establish the link are left in an "exposed" state and may be difficult to reason about subsequently. To illustrate, in the earlier example of The problem with the example above is that interpreting clicks as applications of sequent rules destroys the surrounding formula context by bringing the indicated subformula to the top of the sequent. The interaction method is inherently deep (working on arbitrary subformulas), but the underlying shallow calculus prevents deep reasoning. The user is forced to think about the order of clicks to ensure that the sequents have the right shape. For instance, in the above example the user would have to click on the rightmost a first, which would ensure that when the bs are finally clicked on that the first residual subgoal is not a ⊃ b ⊢ a but a, a ⊃ b ⊢ a.

To escape the bureaucracy of sequential syntax, we require a calculus of deep inference that can preserve formula contexts and thereby perform logically unrelated reasoning steps in a free order. In this paper we use the calculus of structures where there is no difference between a formula and a sequent, and proof steps are allowed to apply in any formula context. Unfortunately, the calculus of structures by itself cannot support our desired linking procedure above either, because every rule in the calculus is still limited to immediate operands of the principal connectives. (The two bs in the example were only ancestrally linked.) We need to generalize the calculus of structures so that the interacting subformulas may be themselves separated by other subformulas.

As the main technical contribution, this paper gives a calculus for linked structures for first-order classical linear logic (Sec. 3). We pick linear logic because: (1) it seamlessly encodes many intuitionistic and classical logics and has clean proof-theoretic foundations; (2) it directly represents resource-nondeterministic choices (splitting and sharing) that are essential when reasoning about computations; and (3) it is an extension to proof by pointing that was left to future work in [START_REF] Bertot | Proof by pointing[END_REF][START_REF] Thery | Real theorem provers deserve real user-interfaces[END_REF]. We substantiate the claims in the paper by a prototype implementation of a linking-based proof-assistant called Profound (Sec. 4). Our implementation is not currently integrated with any mainstream theorem proving system, so it should be seen as conceptual and somewhat speculative.

The Calculus of Structures for Linear Logic

Let us begin with an overview of the calculus of structures for classical first-order linear logic. Formulas (written A, B, . . . ) have the following grammar, A, B, . . .

::= a A ⊗ ⊗ ⊗ B 1 A ⊕ ⊕ ⊕ B 0 !A ∃x. A | a A & B T A & B T ?A ∀x. A
Atomic formulas (or atoms) are written using a, b, . . . , and the negation of a is written as a. We use the term literal to refer to either an atom or a negated atom. Each atomic formula is of the form p(t 1 , . . . , t n ) where p is a predicate symbol and t 1 , . . . , t n are first-order terms (written s, t, . . . ) formed from term variables (written x, y, . . . ) and applications of function symbols (written f, g, . . . ) to terms. As is standard, we assume an ambient signature for the logic that assigns arities to predicate and function symbols. Formulas are in negation-normal form with each vertical column in the above grammar depicting one De Morgan dual pair; we write A for the dual of A.

For our definition of truth in this logic, we use a standard one-sided cut-free sequent calculus-called system LLK-consisting of sequents of the form ⊢ Γ, where Γ is a multiset of formulas. Figure 1 contains the rules of LLK. The meta-theory of this calculus can be found in any standard reference [START_REF] Girard | Linear logic[END_REF][START_REF] Troelstra | Lectures on Linear Logic[END_REF].

The calculus of structures is a formalism where there is no difference between formula and sequent. It is a rewrite system where some entailment ⊢ A, B are turned into rewrite rules that replace, reading from conclusion to premises, a subformula B in a formula with A. The system is best described in a contextual form, where a formula context (written χ, ξ, . . . ) is formed by replacing a single subformula of a formula by the hole ( ). We write χ{A} for the formula formed by replacing the hole in χ by A (possibly capturing the free variables of A).

Figure 2 contains the rules of the classical linear system CLS, which is a minor variant of the system LS from [START_REF] Chaudhuri | The Focused Calculus of Structures[END_REF]. Each rule is to be understood as closed over a formula context; to illustrate, the rule id represents this

⊢ a, a init ⊢ Γ ⊢ Γ, ?A weak ⊢ Γ, ?A, ?A ⊢ Γ, ?A contr ⊢ Γ, A ⊢ ∆, B ⊢ Γ, ∆, A ⊗ ⊗ ⊗ B ⊗ ⊗ ⊗ ⊢ 1 1 ⊢ Γ, Ai ⊢ Γ, A1 ⊕ ⊕ ⊕ A2 ⊕ ⊕ ⊕ ⊢ ?Γ, A ⊢ ?Γ, !A ! ⊢ Γ, [t/x]A ⊢ Γ, ∃x. A ∃ ⊢ Γ, A ⊢ Γ, B ⊢ Γ, A & B & ⊢ Γ, T T ⊢ Γ, A, B ⊢ Γ, A & B & ⊢ Γ ⊢ Γ, T T ⊢ Γ, A ⊢ Γ, ?A ? ⊢ Γ, A ⊢ Γ, ∀x. A ∀ Figure 1: Rules of LLK.
In the ⊕ ⊕ ⊕ rule, i ∈ {1, 2}. In the ! rule, ?Γ stands for a multiset of formulas each of which is prefixed by ?. In the ∀ rule, x is not free in the conclusion. The first line of rules in Fig. 2 are the structural rules of the system. They are, in order, the atomic identity rule; rules for commutativity, associativity, and unit for & (due to which & , T behaves as a commutative monoid structure); and weakening and contraction for ?-formulas. The second line contains logical rules corresponding to the positive connectives: splits (lsp and rsp) for ⊗ ⊗ ⊗, choices (chc) for ⊕ ⊕ ⊕, promotion (bng), and instantiation (wit). In the wit rule, the witness term t is only allowed to mention the bound variables in scope at the hole; in other words, the signature over which conclusion and premise are well-formed does not change on the application of any rule. The third line of rules contain the logical rules for the negative connectives: distributivity (add) for &, absorption (top) for T, dereliction (drl) for ?, and scope-enlargement of universal quantification (all). The final line of rules define the mechanisms of combining different successful "branches" of a CLS proof.

1 a & a id B & A A & B com (A & B) & C A & (B & C) asc A A & T bot T ?A wk ?A & ?A ?A con (A & C) ⊗ ⊗ ⊗ B (A ⊗ ⊗ ⊗ B) & C lsp B ⊗ ⊗ ⊗ (A & C) A & (B ⊗ ⊗ ⊗ C) rsp Ai A1 ⊕ ⊕ ⊕ A2 chc !(?A & B) ?A & !B bng [t/x]A ∃x. A wit (A & B) & (A & C) A & (B & C) add T A & T top A ?A drl ∀x. (A & B) (∀x. A) & B all 1 1 ⊗ ⊗ ⊗ 1 1 1 & 1 1 T 1 !1 1 ∀x. 1
A derivation φ of B from A in any unary proof-system S, written φ : A S --→B, is a sequence of rules of S with the bottom-most rule having conclusion B and the top-most rule having premise A. We write just A S --→B to assert that there is a φ such that φ :

A S --→B. A proof φ of A in CLS is a derivation φ : 1 CLS ---→A.
Under this notion of proof, CLS is sound and complete with respect to the usual linear truth given in terms of LLK.

Theorem 1 (Soundness of

CLS wrt. LLK). If A CLS ---→B, then ⊢ A, B in LLK.
Proof. Every inference rule in CLS with premise A and conclusion B corresponds to a provable sequent ⊢ A, B of LLK. The result follows by a sequence of applications of cut in LLK.

Theorem 2 (Completeness of

CLS wrt. LLK). If ⊢ A 1 , . . . , A n in LLK, then 1 CLS ---→A 1 & • • • & A n .
Proof. Under the interpretation of an LLK sequent ⊢ A 1 , . . . , A n as the formula

A 1 & • • • & A n , every rule of LLK is derivable in CLS.
Generally speaking, one LLK rule corresponds to a sequence of CLS rules; in particular, the ⊗ ⊗ ⊗ rule of LLK corresponds to a sequence of applications of lsp and rsp, while the & rule corresponds to a sequence of applications of add.

Although the system CLS is cut-free, the following cut rule is admissible:

χ A ⊗ ⊗ ⊗ A χ{ T } cut
As usual, this rule is just the dual of the generalized identity (gid) rule:

χ{1} χ A & A gid
Indeed, every rule of CLS has a dual form where the premise and conclusion are exchanged and dualized. The dual system of CLS, which we write as CLS, is a system of refutation, where a refutation of A is a proof A CLS ---→ T , and the system that contains both CLS and CLS is a system where both cut and identity can be reduced to their atomic forms [START_REF] Chaudhuri | The Focused Calculus of Structures[END_REF][START_REF] Straßburger | Linear Logic and Noncommutativity in the Calculus of Structures[END_REF]. Note that the rules lsp and rsp are self-duals, and therefore in the intersection of CLS and its dual system.

Formula Linking

The system CLS forms the foundation of the underlying calculus of the formula linking approach. As mentioned in the introduction, we would like to support a mode of interaction where the user can indicate that any two subformulas are to be linked. The rules of CLS are not well suited for such interactions because each inference rules operates on two immediately & -joined formulas. The essence of linking is to generalize the interaction from & -joined formulas to formulas that are (eventually) ancestrally joined by & . Then, the user can simply mark the formulas they wish to link and the system will apply the right sequence of CLS rules to bring the linked formulas into the same context. If the linked formulas are dual literals, then the system can simply replace the & -formula with 1. The user can therefore repeatedly link dual literals when constructing a proof. (The user is of course free to link other non-atomic subformulas as well.) Importantly, the user is allowed to make incorrect linkages that render the formula unprovable. We require only that any provable formula be also provable by a linkage simplification procedure.

First, let us make the notion of linkage formal. We enlarge the syntax of formulas with a new form, u::A, called a linkage, which indicates that the formula A is marked by a link u. (Links are drawn from some infinite set that is disjoint from the set of variables.) We write u ∈ C to assert that C contains a subformula of the form u::A. We require that every linkage in a formula occurs exactly twice, and that the two subformulas marked by a link be ancestrally joined by & in the subformula ordering. In other words, for each link u ∈ C, there must exist formula contexts ξ, χ 1 , χ 2 and subformulas A and B of C such that C = ξ{χ 1 {u::A} & χ 2 {u::B}}. These restrictions will be preserved by the linkage simplification rules.

The user initiates a linkage by marking two distinct ancestrally & -joined subformulas of the goal formula by a fresh link. We write this as an inference rule that produces a new kind of connective * * * (called interaction), as follows: We restrict this rule to only be applicable when the conclusion formula is free of all linkages, although this restriction can often be relaxed. Note that unlike the rules of CLS (Fig. 2), the rule lnk is doubly deep: not only is the principal formula allowed to occur in any formula context, but also the result of applying the rule has an effect on subformulas that are not necessarily the immediate descendants of the principal formula. Semantically, * * * has the same truth value as & , but the rules applicable to * * * have more restrictions than the analogous rules for & . If the immediate operands of the interaction are the linkages-i.e., if the context χ 1 and χ 2 in the rule lnk above are just holes-then one of the following two rules will be applied. where the unlnk rule is only applicable when A and B are not dual literals. The remaining rules for interaction connectives are used to permute it into smaller contexts. Defining these rules requires a bit of caution, as best illustrated by an example.

Let us attempt to use the same rules as

& in CLS for the * * * -formulas. If we immediately apply a lsp to the interaction formula in the premise above, we would obtain an unprovable formula:

(a * * * (a & b)) ⊗ ⊗ ⊗ b & (a ⊕ ⊕ ⊕ b) (a ⊗ ⊗ ⊗ b) * * * (a & b) & (a ⊕ ⊕ ⊕ b) lsp
The issue here is that lsp forces both a and b (that are &-joined) to be "sent" to exactly one of the operands of the ⊗ ⊗ ⊗, but the theorem is only provable if exactly one of the ⊗ ⊗ ⊗-operands gets exactly one of the &-operands. This can be achieved by a different order of the inference rules, performing add before lsp as follows. The formula in the premise is now provable in CLS under the interpretation of * * * as & . As a general principle, if there is more than one way to interpret a linkage, we should pick an interpretation that preserves provability.

((a * * * a) ⊗ ⊗ ⊗ b) & (a ⊗ ⊗ ⊗ (b * * * b)) & (a ⊕ ⊕ ⊕ b) ((a ⊗ ⊗ ⊗ b) * * * a) & ((a ⊗ ⊗ ⊗ b) * * * b) & (a ⊕ ⊕ ⊕ b) lsp and rsp (a ⊗ ⊗ ⊗ b) * * * (a & b) & (a ⊕ ⊕ ⊕ b) add

Polarities as Organizational Hints

To build our provability-preserving interaction rules, we use the well known concept of polarity. Some rules of CLS such as the split rules lsp and rsp or the choice rule chc add information to the proof; they correspond to proper implications and are not invertible as rules. Other rules such as add or all are equivalences (the conclusion implies the premise), and therefore the rules are invertible. Following general terminology, we say that the connectives with non-invertible interactions have positive polarity, while those with invertible interactions have negative polarity. More precisely, the formulas are separated into positive formulas (written P, Q, . . . ) and negative formulas (written N, M, . . . ) according to the following grammar.

A, B, . . . ::= P N P, Q, . . .

::= a A ⊗ ⊗ ⊗ B 1 A ⊕ ⊕ ⊕ B 0 !A ∃x. A N, M, . . . ::= a A & B T A & B T ?A ∀x. A
Note that the dual of a positive formula is a negative formula and vice versa.

The key feature of polarity is that the rules for positive connectives commute with those for other positive connectives, and likewise for negative connectives with other negative connectives, but the rules for positive and negative connectives do not necessarily commute with each other. It is common to use this observation to design a focused version of a sequent calculus with alternate positive and negative phases of rules [START_REF] Andreoli | Logic programming with focusing proofs in linear logic[END_REF][START_REF] Chaudhuri | A logical characterization of forward and backward chaining in the inverse method[END_REF][START_REF] Liang | Focusing and polarization in linear, intuitionistic, and classical logics[END_REF]. Focusing drastically reduces the non-determinism during proof search (see the experimental results in, e.g., [START_REF] Chaudhuri | A logical characterization of forward and backward chaining in the inverse method[END_REF][START_REF] Mclaughlin | Imogen: Focusing the polarized focused inverse method for intuitionistic propositional logic[END_REF]), but it also clarifies the structure of sequent proofs by identifying, precisely, the informative portions of full sequent proofs. The calculus of structures can also be focused [START_REF] Chaudhuri | The Focused Calculus of Structures[END_REF], although the phase structure is not as evident there because of the incremental and interleaved nature of deep inference. We can, of course, adopt the full focusing discipline in this paper, but the additional structure on proofs is sometimes counter-intuitive from a user's perspective. Instead, we will use features from focusing solely to handle the interaction connective * * * ; in other words, A & B is the ordinary unfocused formula, while A * * * B denotes a focused interaction where, if either A or B is positive then it behaves as the analogue of a focused formula (called the head in [START_REF] Chaudhuri | The Focused Calculus of Structures[END_REF]). Note that, unlike the system in [START_REF] Chaudhuri | The Focused Calculus of Structures[END_REF], there can be zero, one, or two positive formulas in a focused interaction.

Figure 3 defines the system CLn of these focused rules for the interaction connective. In these rules, ρ represents a positive formula context, i.e., for any formula A, the substitution ρ{A} is either A itself or a positive formula. CLn can obviously be seen as a subsystem of CLS with the interpretation of * * * as & and ignoring the linkage information. In particular, it corresponds to that fragment of CLS that defines the interaction of two & -joined formulas. The number of occurrences of interaction formulas and marked subformulas is the same in both premise and conclusion in every rule of CLn. The add rule of CLS splits into two forms in CLn, depending on which of the operands of the & contains the linkage.

The system CLn defines all the rules for simplifying interactions. We embed it into a larger system, named CLnS, that contains:

• the rules lnk, lnid, and unlnk (from above);

• the rules of CLn (Fig. 3); and

• the CLS rules com, asc, bot, wk, con, chc, wit, top, drl and all the rules in the final line in Fig. 2.

CLnS is relatively complete with respect to CLS. This does not mean, of course, that any application of lnk will be valid; consider, for example, linking the a and the a in !a & a. Instead, we have the following correspondence.

Theorem 4 (Completeness of CLnS Relative to CLS).

1. χ{ξ 3 {1}} CLS ---→χ{ξ 1 {a} & ξ 2 {a}} iff χ{ξ 3 {1}} CLnS ----→χ{ξ 1 {a} & ξ 2 {a}}.

If A and B are not dual literals, then χ{ξ

3 {A & B}} CLS ---→χ{ξ 1 {A} & ξ 2 {B}} iff χ{ξ 3 {A & B}} CLnS ----→χ{ξ 1 {A} & ξ 2 {B}}.
Proof. Every CLnS proof is manifestly a CLS proof under the interpretation of * * * as & and eliding the links. In the other direction, it suffices to observe that the lnk rule can be applied in such a way that the linked subformulas are the immediate operands of the principal & . Thus, every CLS rule that involves an interaction of two & -joined formulas can be simulated by a lnk, the corresponding CLn rule, and then unlnk or lnid. Once the full CLS derivation has been simulated in CLnS in this way, we remove all but the deepest linkages on A and B, and the corresponding instances of unlnk or lnid.

Corollary 5. A is provable in CLS if and only if it is provable in CLnS.

Proof. CLnS lacks all the CLS rules that permute a & into a smaller context: lsp, rsp, bng, add, and all. Thus, the only way for two & -joined formulas to interact is by means lnk followed by CLn rules. We can thus appeal to Thm. 4.

The CLn rules preserve the number of occurrences of linkages and interactions. Moreover, they are biased to permute the negative connectives (i.e., & and ∀) out of the positive connectives. This guarantees that if the conclusion of any CLn rule is provable in CLnS, then so is its premise; in other words, every rule of CLn is invertible. The order of application of the CLn rules is therefore immaterial. While different orders can produce different premises, the premises are equivalent.

Theorem 6 (Order Independence of CLn

). If A CLn ---→B and A ′ CLn ---→B, then A ≡ A ′ . 1
Proof. Straightforward inspection of the rules of CLn.

As a consequence, the only choices the user needs to explicitly instantiate an ∃ using wit, and contract a ?-formula using drl. The other choices in a proof-the multiplicative splits for ⊗ ⊗ ⊗ and disjunctive choices for ⊕ ⊕ ⊕-are deterministically inferred directly from the links. Observe that the CLn rules are interleaved with the other rules of CLnS.

It is instructive to compare the CLn rules with the similar focused interaction rules of LSF [START_REF] Chaudhuri | The Focused Calculus of Structures[END_REF], which is a polarized and focused variant of CLS. Most of the rules for positive connectives are the same, except for lnbng,2 which differs only in the fact that the interaction * * * does not dissipate into a & in CLn. As a result, CLn requires rules for interactions between negative formulas as well, while LSF defines focused interactions only for one positive interacting with one negative formula. Conceptually, a CLnS proof can be viewed as an LSF proof where several neighbouring (focused) interactions are merged into one.

Positive Equality and First-Order Effects

Let us call a sequence of applications of CLnS rules that begin at the bottom with lnk and end at the top with its corresponding unlnk or lnid a linking phase. Of the non-CLn rules in Ex. 7, the instances of drl and chc are all forced and can be done automatically. The instances of wit, on the other hand, require user guidance. The quantifier structure of this theorem requires the application of at least one lnall before a wit, so in the general case the system will not be able to keep all the rules of a single linking phase together in a block, i.e., the linking phase are not atomic. Notice that this problem is only significant in the first-order case; for the propositional connectives, we can add rules such as the following to perform a non-CLn rule in the middle of a CLn derivation. To make the linking phase atomic, we add an equality predicate to the language, change lnid to introduce equations between the terms, and add the following lnwit rule to CLn. The derivation can now keep all the CLn rules together.

s1 = t1 ⊗ ⊗ ⊗ • • • ⊗ ⊗ ⊗ sn = tn
A linking phase now ends (reading from conclusion to premise) with either lnid or unlnk. In Ex. 8 above, the residual premise after the lnid is essentially a first-order unification problem. The equations formed by the instances of lnid are all positively signed atomic formulas, with the following two rules.

1 x = x refl s1 = s2 ⊗ ⊗ ⊗ • • • ⊗ ⊗ ⊗ sn = tn f (s1, . . . , sn) = f (t1, . . . , tn) cong
Fact 9. The rules refl, cong, and 1-→1 ⊗ ⊗ ⊗ 1 suffice to show that t = t for any term t.

Since every derivation can be embedded in any formula context, we thus obtain a smooth continuum between deduction and unification in terms of the equality predicate. This freedom comes at a price: the order of the applications of lnwit and lnall is now important. The residual premise is unprovable.

It is not possible to fix this problem without further user guidance, because determining the correct quantifier nesting is equivalent to the full theorem proving problem for first-order logic, which is unsolvable. Fortunately, there is only a single critical pair that needs to be resolved: an interaction between two ∃-formulas. In every other case, we can appeal to Thm 6, suitably generalized.

Our solution therefore involves a modification to linkages. We now have two kinds of oriented linkages, u≫A (called a source) and u≪A (called a sink), with u::A standing for either form when irrelevant. The lnk rule is modified to produce a single source and sink pair:

ξ{χ1{u≫A} * * * χ2{u≪B}} ξ{χ1{A} & χ2{B}} lnk
Most of the remaining rules stay the same, except for the following new rule for resolving an interaction between ∃-formulas. The ideal linking-based proof would just link the a to the two occurrences of a. However, the first link would "consume" the ?a. The user is forced to explicitly contract it before drawing the links.

In Profound, this issue is solved by means of special variants of lnk that store a copy of the ?formula for reuse in subsequent links. One such rule is as follows. Of course, this incurs the dual overhead of ?-formulas that survive unnecessarily. The user will need to clear them with explicit instances of wk, which can quickly become burdensome. From our experimentation, there does not seem to be a preferable default, so Profound allows both contracting and non-contracting uses of lnk. Indeed, Profound allows the user to independently decide to contract the source and the sink when marking them.

There is a related issue when marking the source and the sink that are not ancestrally & -related, but that have an ancestral ?. The simplest example is ?(a ⊕ ⊕ ⊕ a). With the CLonS calculus and implicit linking as described, the user will still not be able to link the a and the a without first explicitly contracting the formula. This is not an altogether contrived example: consider the actual representation of the classical Drinker's formula, ?∃x. ∀y. (p(x) ⊕ ⊕ ⊕ p(y)), as opposed to its linear version in Ex. 7. To solve this issue, we further extend the lnk rule to allow contraction at an ancestral ? when there is no ancestral & as follows.

ξ{?(χ1{u≫A} • χ2{B}) * * * ?(χ1{A} • χ2{u≪B})} ξ{?(χ1{A} • χ2{B})}

where • ∈ {⊗ ⊗ ⊗, ⊕ ⊕ ⊕, &}.

Other Convenience Features

The CLonS system is cut-free, but in practice it is invaluable to use cuts in a proof, both for conceptual and textual simplicity. The Profound implementation therefore allows the user to introduce a cut at any moment, even in the middle of constructing a link. Instead of the general cut rule, however, we actually implement the following variant, which is a composition of the usual cut rule and rsp.

A ⊗ ⊗ ⊗ (A & C) C
The rules for conjunctive truth on the last line of Fig. 2, while sufficient for completeness, are generally too cumbersome to use in practice. Instead, Profound actually implements the following monoidal versions (which are all derivable);

A A • † A † • A 1 1 • 1 A ∀x. A A ∃x. A
where •, † ∈ { ⊗ ⊗ ⊗, 1 , ⊕ ⊕ ⊕, 0 , &, T }, and in the final two rules x is not free in A. In fact, these rules are not explicitly presented to the user, but are instead folded into the traversal mechanism. That is, whenever the cursor on † in A • † or † • A, traversing to the parent simply changes the entire formula to A. This allows us to implement chc in a very simple manner: we just add the following general rule:

0 A del
The user can use del to change any subformula to 0, and if it is the operand of a ⊕ ⊕ ⊕ then traversing to the parent will remove the 0 as a side effect. We find this to be a solid improvement over a direct use of chc, which would otherwise require a further clarification from the user.

Caveats

It is important to point out that Profound is only a research prototype at this point. To make it more broadly viable, we need at least two more crucial features that would require basic research on the calculus of structures.

• Support for intensional equality and induction: in order to make Profound suitable as a user interface for reasoning about computational specifications, the logic must be extended to support intensional (predicate) equality and induction. Equality can be supported by the rules of unification logic, which can be turned into a contextual and incremental form without too much effort. However, for practical uses it will need to support reasoning about equality transitively (e.g., to show (x = z) ⊗ ⊗ ⊗ (x = s(z) & 0 where z and s represent zero and successor, respectively). In the general case this will amount to (incremental) congruence-closure.

The general induction rules in the style of LINC [START_REF] Tiu | A Logical Framework for Reasoning about Logical Specifications[END_REF] or µMALL [START_REF] Baelde | Least and greatest fixed points in linear logic[END_REF] can be readily added to the deep inference formalism. However, experience suggests that proofs written using such induction rules tend to be verbose and confusing. It is more standard to use more restricted induction schemas based on subterm or lexicographic ordering, such as in the Abella system [START_REF] Gacek | The Abella system and homepage[END_REF]. Unfortunately, such restricted schemas tend to have a global and shallow flavour that runs counter to the incremental nature of deep inference. However, the final word is far from written on this matter.

• Support for typed and higher-order reasoning: supporting typed first-order terms is completely straightforward and Profound already assumes that the predicates and terms are simply typed. We intend to extend it to support polymorphically typed predicates and terms in the near future. Supporting dependently typed terms is not particularly critical as dependent restrictions can be recovered relationally; nevertheless, constructing a variant of the calculus of structure for dependent types is an open problem. Second-order quantification [START_REF] Straßburger | Some observations on the proof theory of second order propositional multiplicative linear logic[END_REF] should be straightforward. Extending the calculus of structures to full higher-order logic is also open.

  (a ⊃ b) ⊃ (b ⊃ c) ⊃ (a ⊃ c) the user can click on (i.e., point to) the two occurrences of b. The residual goals after the main goal is closed are: a ⊃ b ⊢ a and a ⊃ b, b ⊃ c, c ⊢ a ⊃ c; the former goal is unprovable! This does not correspond to the intuition of linking the two bs, i.e., of composing the assumptions a ⊃ b and b ⊃ c to get a new assumption a ⊃ c, which would match the succedent of the original theorem.

Figure 2 :

 2 Figure 2: Rules of CLS. In the chc rule, i ∈ {1, 2}. In the all rule, x is not free in B.

  ξ{χ1{u::A} * * * χ2{u::B}} ξ{χ1{A} & χ2{B}} lnk

  χ{1} χ{u::a * * * u::a} lnid χ{A & B} χ{u::A * * * u::B} unlnk

Example 3 .

 3 Let us temporarily ignore linkages and just consider the interaction connective * * * . Consider the provable formula (a ⊗ ⊗ ⊗ b)

(

  χ{u::A} * * * ρ{u::C}) ⊗ ⊗ ⊗ B (χ{u::A} ⊗ ⊗ ⊗ B) * * * ρ{u::C} lnspl B ⊗ ⊗ ⊗ (ρ{u::A} * * * χ{u::C}) ρ{u::A} * * * (B ⊗ ⊗ ⊗ χ{u::C}) lnspr !(?χ{u::A} * * * ξ{u::B}) ?χ{u::A} * * * !ξ{u::B} lnbng (χ{u::A} * * * ξ{u::C}) & (B & ξ{C}) (χ{u::A} & B) * * * ξ{u::C} lnaddl (A & ξ{C}) & (χ{u::B} * * * ξ{u::C}) (A & χ{u::B}) * * * ξ{u::C} lnaddr ∀x. (χ{u::A} * * * ξ{u::C}) (∀x. χ{u::A}) * * * ξ{u::C} lnall B * * * A A * * * B lncom

Figure 3 :

 3 Figure 3: Rules of CLn

Example 7 .

 7 The following CLnS proof illustrates the use of linking. ∀y, z. 1 ∀y, z. u::p(y) * * * u::p(y) lnid ∀y, z. (u::p(y) ⊕ ⊕ ⊕ p(z)) * * * (p(c) ⊕ ⊕ ⊕ u::p(y)) chc × 2 ∀y. ∀z. u::p(y) ⊕ ⊕ ⊕ p(z) * * * p(c) ⊕ ⊕ ⊕ u::p(y) lnall ∀y. ∃x. ∀z. u::p(x) ⊕ ⊕ ⊕ p(z) * * * p(c) ⊕ ⊕ ⊕ u::p(y) wit ∃x. ∀y. u::p(x) ⊕ ⊕ ⊕ p(y) * * * ∀y. p(c) ⊕ ⊕ ⊕ u::p(y) lnall ∃x. ∀y. u::p(x) ⊕ ⊕ ⊕ p(y) * * * ∃x. ∀y. p(x) ⊕ ⊕ ⊕ u::p(y) wit ∃x. ∀y. p(x) ⊕ ⊕ ⊕ p(y) & ∃x. ∀y. p(x) ⊕ ⊕ ⊕ p(y) lnk

(

  χ{u::A}) * * * ξ{u::B} (?χ{u::A}) * * * ξ{u::B} lndrl χ{u::A} * * * ξ{u::C} (χ{u::A} ⊕ ⊕ ⊕ B) * * * ξ{u::C} lnlch χ{u::B} * * * ξ{u::C} (A ⊕ ⊕ ⊕ χ{u::B}) * * * ξ{u::C} lnrch

Example 8 .

 8 u::p(s1, . . . , sn) * * * u::p(t1, . . . , tn) lnid ∃x. χ{u::A} * * * ξ{u::B} ∃x. χ{u::A} * * * ξ{u::B} lnwit Let us revisit Ex. 7 using the above rules. We have this derivation. ∃x. ∀y. ∃x1. ∀y1. x1 = y ∃x. ∀y. ∃x1. ∀y1. u::p(x1) * * * u::p(y) lnid ∃x. ∀y. ∃x1. ∀y1. (u::p(x1) ⊕ ⊕ ⊕ p(y1)) * * * (p(x) ⊕ ⊕ ⊕ u::p(y)) lnlch, lnrch ∃x. ∀y. ∃x1. ∀z. u::p(y) ⊕ ⊕ ⊕ p(y1) * * * p(x) ⊕ ⊕ ⊕ u::p(y) lnall ∃x. ∀y. ∃x1. ∀y1. u::p(x1) ⊕ ⊕ ⊕ p(y1) * * * p(x) ⊕ ⊕ ⊕ u::p(y) lnwit ∃x. ∃x1. ∀y. u::p(x1) ⊕ ⊕ ⊕ p(y) * * * ∀y. p(x) ⊕ ⊕ ⊕ u::p(y) lnall ∃x. ∀y. u::p(x) ⊕ ⊕ ⊕ p(y) * * * ∃x. ∀y. p(x) ⊕ ⊕ ⊕ u::p(y) lnwit ∃x. ∀y. p(x) ⊕ ⊕ ⊕ p(y) & ∃x. ∀y. p(x) ⊕ ⊕ ⊕ p(y) lnk

Example 10 .

 10 This is what happens if the lnwit and lnall rules of Ex. 8 are done in the wrong order. ∃x, x1. ∀y, y1. x1 = y1 ∃x, x1. ∀y, y1. u::p(x1) * * * u::p(y1) lnid ∃x, x1. ∀y, y1. u::p(x1) ⊕ ⊕ ⊕ p(y) * * * p(x) ⊕ ⊕ ⊕ u::p(y1) lnlch, lnrch ∃x, x1. ∀y. u::p(x1) ⊕ ⊕ ⊕ p(y) * * * ∀y1. p(x) ⊕ ⊕ ⊕ u::p(y1) lnall ∃x, x1. ∀y. u::p(x1) ⊕ ⊕ ⊕ p(y) * * * ∀y. p(x) ⊕ ⊕ ⊕ u::p(y) lnall ∃x. ∃x1. ∀y. u::p(x1) ⊕ ⊕ ⊕ p(y) * * * ∀y. p(x) ⊕ ⊕ ⊕ u::p(y) lnwit ∃x. ∀y. u::p(x) ⊕ ⊕ ⊕ p(y) * * * ∃x. ∀y. p(x) ⊕ ⊕ ⊕ u::p(y) lnwit ∃x. ∀y. p(x) ⊕ ⊕ ⊕ p(y) & ∃x. ∀y. p(x) ⊕ ⊕ ⊕ p(y) lnk

  ∃y. (∃x. χ{u≫A}) * * * ξ{u≪B} ∃x. χ{u≫A} * * * ∃y. ξ{u≪B} lnex (b ⊗ ⊗ ⊗ c).

& (a & b) & (a ⊕ ⊕ ⊕ b). Suppose the common & -ancestor a and the leftmost a is turned into * * * with lnk.(a ⊗ ⊗ ⊗ b) * * * (a & b) & (a ⊕ ⊕ ⊕ b) (a ⊗ ⊗ ⊗ b) & (a & b) & (a ⊕ ⊕ ⊕ b) lnk

A ≡ B can be defined as usual as (A & B) & (B & A).

In the polarized setting, there would be a similar case for the ↓ connective that can be seen as a purely linear variant of !.

& ?(a ⊗ ⊗ ⊗ c) & ?a &

Unfortunately, this turns out to be fairly frustrating when trying to select, for instance, the subformula B &

& B & C, because& is internally treated as a left-associative binary operator. The user is forced to first bring the entire subformula they wish to select to the left (which can be done freely in the logical mode).

Acknowledgements: We thank Dale Miller and Lutz Straßburger for their help with many aspects of this work.

Intuitively, the source is "brought to" the sink. The rules are prioritized so that the lnwit rule is only applicable in the case that lnex is not. Note that if the source is not on the left of the interaction * * * , then the lncom rule can be used to put it there. Let CLonS stand for:

CLnS ∪ {lndrl, lnlch, lnrch, lnwit, lnex} ∪ {refl, cong} (with the understanding that the lnk rule introduces oriented linkages), and let CLon stand for CLonS \ CLS.

Theorem 11 (Order Independence of CLon

Proof. Same idea as for Thm. 6.

Theorem 12. For any formula A free of =-subformulas, 1

CLonS

----→A if and only if 1

CLnS

----→A.

Sketch. For the forward direction (only if), the CLonS rules lnwit, lnex, lndrl, lnlch and lnrch are admissible in CLnS. To recover the CLnS proof, it suffices to use the wit, drl and chc rules to rewrite all the instances of lnwit, lnex, lndrl, lnlch and lnrch. Then, these rules can be permuted below any occurrences of (the CLonS variant of) lnid on subformulas. This leaves just the instances of refl and cong above the CLonS variants of lnid; but, these rules do not interact with any other rules, and can therefore be permuted to stand in a block right above the lnid that gives rise to them; the entire block can then be replaced with the CLnS variant of lnid.

The reverse direction (if) is a simple consequence of Fact 9.

Implementation Notes

The classical system CLonS has been implemented as part of the interactive proving tool Profound [START_REF] Chaudhuri | Profound[END_REF]. The tool is launched by giving it a goal theorem either on the command line or using an input file. It then presents the user with an interface where the text of the theorem may be directly manipulated (using the keyboard or the mouse) in two modes: a logical mode and a linking mode. In the logical mode, the user is allowed to perform any of the rules in CLonS \ CLon. In other words, the only non-trivial actions available in this mode are: (1) instantiating ∃ (wit) and choice (chc) when there are no linkages, and ( 2) contraction (con) and weakening (wk). The user is also allowed the freedom to freely reorganize the formula using associativity and commutativity of & . The system lets the user also treat the other binary connectives as associative and commutative (the corresponding rules are admissible in CLS and CLnS).

In the linking mode, the user indicates an oriented link between a pair of subformulas. Using the keyboard, this amounts to traversing the subformula tree and marking two subformulas that are ancestrally & -linked as source and sink. This action is more intuitive with a pointing device such as the mouse, where one subformula is simply dragged and dropped on another. The main difficulty with pointing is to determine which subformulas the user wishes to point to, as most cursor positions occur within many subformulas. The system uses the heuristic of selecting the smallest subformula surrounding the cursor position, and letting the user go up in the subformula tree by scrolling the mouse-wheel. 3 The current implementation of Profound is in OCaml and uses the GTK+ windowing library for its graphical interface, and has been tested to run on POSIX-compatible systems such as Linux and Mac OS X. In the future, we will probably re-implement it as a server/client setup using Javascript and using the HTML5 Canvas library for the user interface, which would make it portable across a wide range of platforms that support graphical webbrowsers. Systems that can support multiple pointers and different interaction metaphors such as "pinching" might also enable Profound to perform marking or linking of formulas more directly.

In the rest of this section, we will describe some additional features of Profound that are not strictly part of the CLonS proof system, but are nevertheless very important for practical use of linking-based interaction.

Implicit Contraction

Perhaps the most natural aspect of the linking-based interaction metaphor is the ability to treat a logical problem as a kind of matching puzzle: bits of the current obligation are linked to bits of known facts and lemmas until the problem reduces to a known and manageable form. However, the formal CLonS system does require an additional step of explicit contraction that can complicates this simple aspect. For example, suppose we want to prove ?(a ⊗ ⊗ ⊗ b)