=Paper=
{{Paper
|id=None
|storemode=property
|title=A Database Browser Based on Pattern Concepts
|pdfUrl=https://ceur-ws.org/Vol-977/paper7.pdf
|volume=Vol-977
}}
==A Database Browser Based on Pattern Concepts==
https://ceur-ws.org/Vol-977/paper7.pdf
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)