A Database Browser based on Pattern Concepts Jens Kötters and Heinz W. Schmidt† †Computer Science & IT, RMIT University, Melbourne, Australia (Heinz.Schmidt@rmit.edu.au) Abstract. A Galois connection is stated between a knowledge base and queries over this knowledge. Queries are stated as conjunctions. Both the knowledge and queries are represented by certain graphs. This Galois connection gives rise to lattices of pattern concepts implicitly contained in the theory (all derivable facts) over the knowledge base. The formal foundation for browsing such lattices and a realisation in terms of a prototype tool is outlined. Data types may be assigned to individual columns of tables in the database. A type assignment corre- sponds to an extension of the query language and incorporates additional knowledge into the process of concept creation. Type and derivation sup- port in the tool may be provided by pluggable modules. In the examples in this paper, only the numeric type and concrete, stored relations are featured. Keywords: Database Browsing, Pattern Concepts, Formal Concept Anal- ysis, Knowledge Representation, Many-Sorted Logics 1 Introduction The paper presents a prototype of a FCA browser for knowledge bases and its formal foundation. The browser allows interactive access to the content of a database. Via a command-line interface, concept lattices over relational data can be traversed. Each concept intent corresponds to a logical formula (or query) in one or more free variables, using relational expressions over function terms with variables where the functions range over primitive and user-defined data sorts. Each extent is the corresponding table of results. There is one concept lattice for each set of free variables; the user can cross over into different lattices during navigation (thus changing variables in the result set). We will see that each concept lattice arises from a suitably defined pattern structure [5] (stretching the definition a bit), and pattern concepts have indeed been considered for the representation of logical formulas [5, p.129]. Further references and details of the approach can be found in [10], although many-sorted logic has not been considered there. The formalisation of FCA navigation includes concrete (stored) and abstract (computed) relations derived by domain-specific conditional logical rules and/or relational algebra operations (SQL). Domain knowledge rules need to capture – derived relations (e.g. computing relatives based on a network of parent-child relationships); 48 Jens Kötters and Heinz W. Schmidt – domain-specific interpretations of object attributes, incl. common taxonomies and discretizations (e.g. age range of legal childhood, adulthood, retirement in social insurance databases etc.) – representation invariants abstracting from syntactic and computational de- tails of the representation incl. relational algebra, and independent of the spe- cific database platform. While representations are typically realised impera- tively, occassionally such invariants are required to manipulate and transform queries or tables for the purpose of navigation. We call these rules abstract, in particular, because they are independent of specific sets of concrete relation tables, and hence remain invariant across dif- ferent concrete databases for the given domain and also across updates of the same database. Although our browser prototype does not include an inference engine, such a module can be interfaced easily by storing the results of external reasoning steps as special tables accessible to the browser, on-the-fly. Here we focus on the connection with FCA lattices. For the purpose of this paper, we interpret many-sorted logics in an algebraic- categorical framework – a view that has gained wide acceptance in the semantics of programming languages, abstract data types, knowledge representation and behaviour specification over several decades. It goes back to universal algebra [7] and work on formal specification and abstraction since the seventies (cf. e.g. [3, 4, 1]). In the interest of readability of the paper to a broad FCA audience, we limit ourselves to an overview and introduce notation only where necessary to be able to follow the core examples and algorithms presented in the paper. A complete formal exposition is beyond the scope of this paper and this conference. The paper is organised as follows. In Section 2 we review relevant existing work on many-sorted structures and logics and summarise our notation; section 3 presents some technical advanced many-sorted structures that form the basis for our FCA-centric approach to patterns and queries; section 4 focuses on the browser, both in terms of the core algorithm and the user interface for navigation. Finally Section 5 provides some links to related work. 2 Many-Sorted Structures and Logics In this section we briefly summarise basic notations and formalisation used in the rest of the paper. The algebraic-categorical view of abstract data types and data analysis has developed in line with model theory: syntax is captured in sig- natures limiting the construction of well-sorted terms and atomic formulae over algebras (data and functions) or structures (algebras plus relations) as models. Terms are sorted to represent data of primitive sorts abstractly, independent of a specific interpretation by a data domain. For example attributes, arithmetic or logical operators appearing in logical formulae or database queries may be sorted, as in the example below, where Anne is a constant of sort person, age is a numeric attribute of an object and Parent is a binary predicate on sort person. For flexible abstract many-sorted definitions we permit so-called order- A Database Browser based on Pattern Concepts 49 sorted models, i.e., where sorts are partially ordered. bool and int are assumed to be built in primitive sorts. object is a built-in maximal sort. sort int < number, person < object Anne,Bob,Chris,Dora,Emily: → person + : number × number → number < : number × number → bool age: object → int Parent: person × person female,male: person As we will see later, the sort order abstracts from a corresponding subset rela- tionship between corresponding data domains. We also allow so-called ‘mixfix’ notation for function and predicate symbols as known from platforms realising algebraic-categorical forms of many-sorted type or logical specifications, such as OBJ3 [6], CASL [1], and ELAN [2, 9]. For instance, + indicates the two argument positions for this binary infix operator ‘+’. Signatures. Formally, Parent age META c0 c1 c0 c1 table column type Anne Bob Anne 59 Parent c0 person Anne Chris Bob 31 Parent c1 person Bob Dora Chris 27 male c0 person Bob Emily Dora 7 female c0 person Emily 3 age c0 person female male age c1 number c0 c0 Anne Bob Dora Chris Emily Fig. 1. Database a many-sorted signature is a triple Σ = (S, F, P ) where S is a finite partial order (of elements called sort symbols or sorts for short), F = (Fu,s )u∈S ∗ ,s∈S is a pairwise disjoint family of sets of symbols (called function symbols) and P = (Pu )u∈S ∗ is a family of pairwise disjoint sets of symbol (called predicate symbols). For f ∈ Fu,s (or p ∈ Pu ) we set dom(f ) = u (or dom(p) = u, respec- tively) and cod(f ) = s (read ’domain’ and ’codomain’ respectively). As usual for abstract types and many-sorted logics, signature morphism remap sorts, func- tion and predicate symbols preserving domains, codomains and sort order. We use TΣ,s to denote the set of well-formed terms of sort s and AΣ the set of well-formed atoms p(t1 , . . . , tn ) for p ∈ Pu , u = s1 · · · sn , ti ∈ TΣ,si (1 ≤ i ≤ n). Elimination of junk. Many-sorted approaches are interesting to us as they reduce the search space for inferencing and navigation: ill-sorted terms and for- mulae can be recognised efficiently, and in fact eliminated syntactically. This 50 Jens Kötters and Heinz W. Schmidt reduces the search space significantly and eliminates massive amounts of so- called ’junk data’ in terms of ill-sorted elements, in particular in queries and auxiliary formulae occuring in searches. Example database. Before we formalise concrete models, let us look at a example database as a concrete model in terms of sets and tables. A database table corresponds to (a) a relation interpreting a corresponding predicate symbol, or (b) a function from a set of columns (arguments) to a column (result), or (c) a set of attributes mapping the rows (object keys) to attributes, thus encoding functions similar not unlike (b). For example in Fig. 1, the table named Parent contains all pairs (p, p0 ) such that P arent(p, p0 ) is valid, while the table age maps persons to their ages. Column are representing attributes including selectors of components in tuples. For example c0 in the age table selects the person component of the table rows etc. Queries supported by the database are constrained by the signature and the logical connectives permitted in the structure of formulae outside the algebraic structure captured by the signatures. For concrete databases and in our prototype implementation, we assume the existence of a META table (see Fig. 1) which represents the signature information relevant for the tables in the database. The remaining signature (outside the data base) represents operators on data types in the tables or relations that can be computed from the data base using queries. Many-sorted structures. Given a many-sorted signature Σ, a Σ-structure D = h(Ds )s∈S ; F, Ri has a family of carrier sets Ds (aka domains) sorted and ordered by S and families of sets of functions and relations compatible with the prescribed domains and codomains of functions and predicate symbols in Σ. The partial order of sorts is interpreted as subsorting: Ds ⊆ Dt if s ≤ t. Functions are total on their domains.1 For readability in concrete examples we also denote Ds by sD (the interpretation of sort s in D). Likewise, for f ∈ Fu,s (p ∈ Pu ) we denote the corresponding function in D by fD (or pD respectively). It is well-known that the term structure TΣ := h(Ts )s∈S ; F, P i with empty relations forms the free Σ-structure. Homomorphisms between Σ-structures are weak, i.e. preserve definedness but not necessarily undefinedness of relations. They are called strong if they also preserve undefinedness. The formal structure underlying the database in Fig. 1 has for example: personD = {Anne, Bob, Chris, Dora, Emily}, AnneD = Anne, . . . , EmilyD = Emily, numberD = {3, 7, 27, 31, 59, ...}, ParentD = {(Anne, Bob), (Anne, Chris), (Bob, Dora), (Bob, Emily)}, ageD = {Anne 7→ 59, Bob 7→ 31, Chris 7→ 27, Dora 7→ 7, Emily 7→ 3} Many-sorted logics. For the rest of the paper, let Σ be a fixed signature and D a Σ-structure. We assume each sort in Σ includes a distinguished equality pred- icate =s with the obvious interpretation in D. For sorted terms and formulae 1 Note that the underlying algebra D = hD; Fi, with the unsorted carrier D the union of the Ds , is partial, as is the underlying unsorted structure. A Database Browser based on Pattern Concepts 51 with variables we use a many-sorted family (Vs )s∈S of at most countably infinite and pairwise disjoint sets of variable symbols that are disjoint from function symbols in F. We denote by Σ(V ) the extended signature that adds variables as constant function symbols to Σ. The Σ(V ) − term structure now contains all well-sorted terms with variables. Σ-formulae are built using well-sorted atoms p(t, ...) for predicate symbols p in Σ, conjunction, implication and existential quantifiers over sorted variables constrained to prenex normal form (i.e. not oc- curring under conjunction or implication but ranging over the entire formula at hand). We denote by F ree(φ) the free variables of a formula φ, call φ closed iff F ree(φ) = ∅, denote by AtΣ the set of all Σ-atoms, and by ClΣ the set of Σ-formulae. Formulae are evaluated over a Σ-structure as usual, by recursively ’translating’ function symbols into function application, predicate symbols into relations in D and interpreting conjunction, implication and existential quan- tification logically. We use ID to denote the corresponding interpretation of closed terms and fomulae and write D |= φ to denote that φ is valid in the model D. For terms or formulae with variables (F ree(φ) = {x1 , . . . , xn }) we write ID (φ[a1 /x1 , . . . , an /xn ]) to denote the corresponding evaluation under the assignment of the ai to xi . age: [31,59] ∃p0 ∃p1 ∃p2 ∃n0 ∃n1 ∃n2 : ( age(p0 , n0 ) ∧ 31 ≤ n0 ≤ 59 Parent Parent ∧ age(p1 , n1 ) ∧ 7 ≤ n1 ≤ 27 ∧ age(p2 , n2 ) ∧ 3 ≤ n2 ≤ 31 ∧ P arent(p0, p1) ∧ P arent(p0, p2) x ∧ x =person p2 ) age: [7,27] age: [3,31] Fig. 2. Query graph for pattern formula 3 Patterns For queries in particular, we are interested in formulae ψ in the following prenex normal form, ∃x1 . . . ∃xm : φ (1) where φ is a conjunction, φ ≡ (φ1 ∧ · · · ∧ φl ). We interpret ψ as the request to compute all possible consistent assignments to F ree(ψ) such that D |= ψ[a1 /x1 , . . . , an /xn ]. Without loss of generality, we assume that each free vari- able y ∈ F ree(ψ) has a single occurrence on the left-hand side of an equation y =s . . .. In the above sense, Σ-formulae of the form ψ can be regarded as pat- terns that select matches in any Σ-structure. More precisely, the set of pattern matches Pφ := {(a1 , . . . , an ) ∈ Ds1 × · · · × Dsn | D |= ψ[ai /x1 , . . . , an /xn ]} is well-defined. The patterns for a given set of free variables form a lattice by implication (set inclusion of their matches): ψ ≤ ψ 0 :⇔ Pψ ⊆ Pψ0 (2) 52 Jens Kötters and Heinz W. Schmidt where ψ and ψ 0 are two Σ-formulae of the form (1) above, s.t. F ree(ψ) = F ree(ψ 0 ). We denote this lattice by LΣ,u (or Lu for short when Σ is fixed), where xi ∈ Vsi (1 ≤ i ≤ n) and u = s1 · · · sn . (Because formulae are equivalent under renaming of free variables, the sorts of variables only matter.) The top element >Lu corresponds to the tautology ∃y1 . . . ∃yn : x1 =s1 y1 ∧ · · · ∧ xn =sn yn . In particular single-sort patterns with |F ree(ψ)| = 1 define subdomains of some Ds (with {x} = F ree(ψ)). Elements of Ls represent logical subdomains of the given sort, i.e., subdomains expressible in logical formulae over Σ. For the structural representation of (1) we use a tuple (X, ν, (G, κ)) deter- mined as follows: For each sort s ∈ S, the free variables of sort s occuring in (1) are collected in the set Xs , and X := (Xs )s∈S . Correspondingly, the bound variables of sort s are collected in the domain Gs of the many-sorted structure G. For each relation symbol p ∈ Pu , we have G |= p(y1 , . . . , yk ) iff p(y1 , . . . , yk ) is an atom in φ. For each s ∈ S, κs is a mapping on Ds . For each x ∈ Ds , κs (x) is a formula equivalent to the conjunction of all domain-specific conditions φi on x. In particular, κs (x) := > if no conditions on x occur in (1). Finally, ν is a family of mappings νs : Xs → Ds , where νs (x) is the unique v such that x =s v occurs in φ. We call such a tuple a windowed structure, and the pair (G, κ) an augmented structure. For technical reasons, we allow arbitrary sets for the do- mains of G. Figure 2 shows a formula and next to it the associated windowed structure, which may be drawn as a graph. Entailment is formalized by homomorphisms. Their definition reflects the nestedness of structures. A homomorphism f : (G1 , κ1 ) → (G2 , κ2 ) of aug- mented structures is a homomorphism f : G1 → G2 of many-sorted structures such that (κD )s (f (v)) ⇒ κs (v) for all s ∈ S and v ∈ Gs . A homomorphism f : (X1 , ν1 , G1 ) → (X2 , ν2 , G2 ) exists in the case X1 ⊆ X2 and is then a homo- morphism f : G1 → G2 which preserves free variables, that is f ◦ ν1 = ν2 ◦ ιX X2 , 1 X1 where ιX2 is the subset embedding. Within the scope of this paper, we represent a knowledge base by an aug- mented structure ∆ := (D, κ∆ ), where D is a Σ-structure representing a database and and (κ∆ )s (g) is the most specific equivalence class of formulae in Ls charac- terising the object g. The solution set of a conjunctive query over ∆, represented by a windowed structure (X, ν, G), is Hom(G, ∆) ◦ ν. The solution set can be re- garded a subset of Hom(X, ∆), if we regard X as a trivial augmented structure (the details are omitted). More generally, we define a table to be a pair (X, Λ), where X is a many-sorted family of variables and Λ ⊆ Hom(X, ∆). By Tab(∆) we denote the set of all tables over ∆. The order on Tab(∆) in which the infimum is the join is given by (X1 , Λ1 ) ≤ (X2 , Λ2 ) :⇐⇒ X2 ⊆ X1 ∧ Λ1 ◦ ιXX1 ⊆ Λ 2 . 2 Given many-sorted, augmented or windowed structures S1 and S2 , we say that S1 generalizes S2 and denote this by S1 . S2 , if a homomorphism f : S1 → S2 exists. Generalization is a preorder, and we call S1 and S2 hom-equivalent, Q if S1 . S2 and S2 . S1 . It is not difficult to see that the product i∈I Gi of a family (Gi )i∈I of many-sorted structures is an infimum in the generalization preorder(recall however that an infimum in a preorder is not unique). Infima of A Database Browser based on Pattern Concepts 53 augmented or windowed structures are realized by products: Q Q V i∈I (Gi , κi ) := ( i∈I Gi , κ, where κs (v) := i∈I (κi )s (v) , Q T Q i∈I (Xi , νi , Gi ) := ( i∈I Xi , hνi i , i∈I Gi , where hνi i(x) := (νi (x))i∈I . Galois Connection The following operations define a Galois connection be- tween (W, .) and (Tab(∆), ≤): (X, ν, G)0 := (X, Hom(G, ∆) ◦ ν), (3) Y (X, Λ)0 := (X, h(λ)λ∈Λ i , ∆Λ ) = (X, λ, ∆). (4) λ∈Λ Proof. We only show operations are order-reversing, extensivity is easier to see. If (X1 , ν1 , G1 ) . (X2 , ν2 , G2 ), then there is by definition ϕ ∈ Hom(G1 , G2 ) with ν2 ◦ιX X1 X2 = ϕ◦ν1 . Thus Hom(G2 , ∆)◦ν2 ◦ιX2 = Hom(G2 , ∆)◦ϕ◦ν1 ⊆ Hom(G1 , ∆). 1 So (·)0 in (3) is order-reversing. Q (X1 , Λ1 ) ≤ (X2 , Λ2 ). Then Xfor Let all λ ∈ Λ1 we have Qλ ◦ ιX X1 ∈ Λ2 , and 2 thus λ∈Λ2 (X, λ, ∆) . (X 2 , λ ◦ ι 2 X1 , ∆) . (X, λ, ∆). So λ∈Λ2 (X, λ, ∆) . 0 Q λ∈Λ1 (X, λ, ∆), and (·) in (4) is order-reversing. t u The Galois connection gives rise to theS complete lattice L∆ , or to L∆ [X] if restricted to queries φ with F ree(φ) = s∈S Xs : L∆ := {(T, W ) | T ∈ Tab(∆), W ∈ W, T 0 = W, W 0 = T } (5) L∆ [X] := {(T, W ) ∈ L∆ | ∃Λ : T = (X, Λ)} (6) We hold that only formulas represented by connected patterns (as in Fig. 2) qualify as concept descriptions, and thus only components of powers of ∆ qualify as concept intents (cf. (4)). The implemented algorithm is still immature and will therefore only briefly be considered in the next section. #(concepts) DB relations +constants +numeric comparison x:person 9 12 18 x,y:person 26 59 85 Table 1. Number of concepts, depending on free variables and signature 4 Pattern Browser 4.1 Algorithm In the order ∆0 , ∆1 , ∆2 , . . . , powers are computed and decomposed into their components, which are paired up with morphisms designating the subjects of the query (cf. h(λ)λ∈Λ i in (4)), translated into SQL, paired up with result tables 54 Jens Kötters and Heinz W. Schmidt returned by a MySQL server, and then compared (using the order on Tab(∆)) to eliminate equivalent patterns and build the concept lattice(s). The algorithm terminates when a power ∆k does not produce new patterns. Table 1 shows the number of generated concepts for queries in one and two free variables of type person, for different settings of query expressiveness. The ”naive” algorithm did not terminate in reasonable time even for some of the small examples. This is due to combinatorial explosion of patterns in higher powers of ∆ and hardness of query optimization. More efficient algorithms are expected to make use of the fact that graph nodes are tuples over ∆. 00| DATABASE BROWSER (press ’h’ for help) 01| Concept#0>top 02| Concept#0>intent 03| x : age(x,n0) AND 3<=n0<=59 04| Concept#0>specialize 05| Concept#1>intent 06| x : age(x,n0) AND female(x) AND 3<=n0<=59 07| Concept#1>extent 08| 09| x 10| ----- 11| Anne 12| Dora 13| Emily 14| 15| Concept#1>generalize 16| Concept#0>specialize 17| Concept#3>intent 18| x : age(p0,n0) AND age(p4,n4) AND age(x,n5) AND parent(p0,p4) AND parent(p0,x) 19| AND 31<=n0<=59 AND 7<=n4<=27 AND 3<=n5<=31 20| 21| Concept#3>specialize 22| Concept#14>intent 23| y,x : age(y,n0) AND age(p3,n3) AND age(x,n2) AND parent(y,p3) AND parent(y,x) 24| AND 31<=n0<=59 AND 7<=n3<=27 AND 3<=n2<=31 25| 26| Concept#14>extent 27| 28| y | x 29| --------- 30| Anne| Bob 31| Anne| Chris 32| Bob | Dora 33| Bob | Emily 34| 35| Concept#14>specialize 36| ->Concept#46*** 37| ->Concept#18 38| 39| -------------------------------------------------------------------- 40| y,x : age(y,n0) AND age(p3,n3) AND age(x,n4) AND parent(y,p3) AND 41| parent(y,x) AND 31<=n0<=59 AND 7<=n3<=27 AND 3<=n4<=27 Fig. 3. Browsing session 4.2 Interface Figure 3 shows a browsing session, which starts in the top concept. Extent, intent, lower neighbors and upper neighbors of the current concept can each be shown by pressing a key. If a list of neighbors is shown, each concept in the list A Database Browser based on Pattern Concepts 55 can be highlighted and examined in the subwindow below the dashed line before it is selected (see Fig.3). The intent is shown as a formula; free variables are listed before the colon, all other variables are existence quantified. The concepts computed are the 103 concepts listed in the right column of Table 1. 5 Related Work The Galois connection between Σ-theories (sets of Σ-formulae closed under derivation) and categories of models (here Σ-structures) is folklore in model theory and celebrated in textbooks on algebraic and logical specification for data and behaviour. In this paper we use a more restricted connection for for- mal concept navigation on a knowledge base, focusing on queries (formulae) and their result sets (structures). The abstraction of the representation of data and knowledge bases in such theories renders access to a powerful mathematical tools. Details of a mapping from such data and knowledge bases to theories and structures can be found elsewhere. The second author used a many-sorted theory construction [11] for expres- sively modeling typed formal concepts with a rich set of sorts and user-defined data types, including subsorts. However typed conceptual scaling was used for the relevant subsorts to associate a Galois connection with the resulting struc- tures for each sort and to work directly on typed context tables. Patterns were not supported in that work. If we extend the definition of pattern S structure in [5] to d categories of pat- terns (preordered by morphisms), then ( X Hom(X, ∆), (W, ), δ) is a pattern structure. A morphism λ ∈ Hom(X, ∆), X ⊆ V , is essentially a partially de- fined variable assignment. Each such assignment is naturally identified with a windowed structure δ(λ) := (dom(λ), λ, cod(λ)), where always cod(λ) = ∆. The Galois connection stated in [5] becomes A := λ∈Λ δ(λ) d (7)  S (X, ν, G) := {λ ∈ X Hom(X, ∆) | ∃f : (X, ν, G) → δ(λ)}. (8) The T set A of partial assignments corresponds to the table (X, Λ)0 with X :=  λ∈A dom(λ) and Λ := {λ |X | λ ∈ A}; the windowed structures Λ and A are hom-equivalent. However, the empty tables (X, ∅),X 6= V , have no representa- tion in this approach; in this, the produced lattice may differ from L∆ . A relational context family can be defined as a pair ((Ki )i∈I , (Rj )j∈J ), where each Ki =: (Gi , Mi , Ii ) is a formal context and each Rj is a binary relation on Gi1 × Gi2 for some i1 , i2 ∈ I. The concept lattice for Ki is denoted by B(Ki ). The relational context family corresponds to a many-sorted relational structure with sort set I and family of relations (Rj )j∈J . The concept lattices B(Ki ), i ∈ I, correspond to the lattices of domain logical formulas. Relational Concept Analysis, W as described in [8] and with existential scaling, produces for each sort i a -sublattice of C∆ [X], where X contains one variable of sort i, which contains all concepts generated by finite, connected, acylic windowed graphs. This can be shown by induction over the steps of the algorithm given in [8]. 56 Jens Kötters and Heinz W. Schmidt 6 Conclusion This paper introduced a novel approach to model queries over relational data – both stored and computed – in terms of FCA lattices. In logical terms, abstract patterns are represented by certain many-sorted formulae with variables. The underlying implication lattices of the formulae and certain structures computed over the database form a Galois connection, as we showed, suitable for navigation of a solution space to the query. Changes in the query are translated into changes to the underlying lattice. Navigation thus includes intra-lattice and inter-lattice moves available to the user exploring domain knowledge over a database in terms of its concrete relation tables and tacit knowledge about these tables. A proto- type browser was implemented to evaluate these concepts and was described in the paper. References 1. Baumeister, H., Bert, D.: Algebraic specification in casl. In: Frappier, M., Habrias, H. (eds.) Software Specification Methods, pp. 209–224. Formal Approaches to Computing and Information Technology FACIT, Springer London (2001), http: //dx.doi.org/10.1007/978-1-4471-0701-9_12 2. Borovansky, P., Castro, C.: Cooperation of constraint solvers: Using the new pro- cess control facilities of elan. In: Proceedings of The Second International Workshop on Rewriting Logic and its Applications, RWLW’98. pp. 379–398 (1998) 3. Broy, M., Wirsing, M.: Partial abstract types. Acta Informatica 18(1), 47–64 (1982) 4. Cohn, A.G.: A more expressive formulation of many sorted logic. Journal of auto- mated reasoning 3(2), 113–200 (1987) 5. Ganter, B., Kuznetsov, S.O.: Pattern structures and their projections. In: Delu- gach, H.S., Stumme, G. (eds.) Proceedings of ICCS 2001. LNCS, vol. 2120, pp. 129–142. Springer (2001) 6. Goguen, J., Kirchner, C., Kirchner, H., Mgrelis, A., Meseguer, J., Winkler, T.: An introduction to obj 3. In: Kaplan, S., Jouannaud, J.P. (eds.) Conditional Term Rewriting Systems, Lecture Notes in Computer Science, vol. 308, pp. 258–263. Springer Berlin Heidelberg (1988), http://dx.doi.org/10.1007/3-540-19242-5_ 22 7. Grätzer, G.: Universal algebra. Springer (2008) 8. Huchard, M., Hacene, M.R., Roume, C., Valtchev, P.: Relational concept discovery in structured datasets. Annals of Mathematics and Artificial Intelligence 49(1-4), 39–76 (2007) 9. Kirchner, H., Moreau, P.E.: Non-deterministic computations in elan. In: Fiadeiro, J. (ed.) Recent Trends in Algebraic Development Techniques, Lecture Notes in Computer Science, vol. 1589, pp. 168–183. Springer Berlin Heidelberg (1999), http: //dx.doi.org/10.1007/3-540-48483-3_12 10. Kötters, J.: Concept lattices of a relational structure. In: Pfeiffer, H.D., Ignatov, D.I., Poelmans, J., Gadiraju, N. (eds.) Proceedings of ICCS 2013. LNCS, vol. 7735, pp. 301–310. Springer (2013) 11. Peake, I.D., Thomas, I., Schmidt, H.: Typed formal concept analysis. In: 7th Inter- national Conference on Formal Concept Analysis (ICFCA09). pp. 35–51. Springer (2009)