In this paper, we introduce our work on our doctorate with title \Higher Order Support in Logic Speci cation Languages for Data Mining Applications". Current logic speci cation languages, such as FO( ) provide an intuitive way for de ning the knowledge within a problem domain. Extended support for data representation is lacking however, and we want to introduce structured recursive types and generic types, together with a rst class citizen approach to predicates. These additions correspond to higher order concepts.
relation, as shown below: Another example within the context of data mining is the concept of a graph homomorphism. A graph homomorphism is a constrained relation between two graphs. As such, it is natural to represent it as a predicate. However, data mining applications frequently use homomorphisms, isomorphisms or other `relationships' as an object of their reasoning. For example, we want something to hold for no, some, or all homomorphisms. This treats these predicates as a rst class citizen as it introduces quanti cation over these predicates.
The idea that modularity bene ts from an expressive higher order language can
be found in earlier work done conjunction with I. Dasseville et al.
The main roadblock towards implementing the forementioned abstractions is that many logic speci cation languages use a ground-and-solve technique. The grounding phase transforms a logic speci cation theory to an equivalent theory on propositional level, allowing SAT techniques to be used. It achieves this by enumerating over nite domains, instantiating the theory for every possible substitution of variables by domain elements. However, we often do not want to x our domain beforehand: we do not want to x the number of connections or elements in pattern mining, or the names of items in item set mining. Furthermore, structured recursive types and generic types introduce in nite domains of their own, for example the set of all possible lists. As a result, it will be necessary to develop grounding techniques that can handle in nite domains.
This research is focussed on providing higher order support to ground-and-solve
systems such as IDP (Imperative Declarative Programming)
Other systems, such as Flora-2
However, there are several interesting problems where it is not wise to restrict ourselves to a nite domain. Moreover, as argued in Section 1, our proposed additions and abstractions to allow more user-friendly data representations introduce these in nite domains.
Because of the possible blowup when working with large, (possibly in nite) domains, the design and implementation of novel grounding and inference techniques is necessary. These techniques must be capable of reasoning on the in nite domain in only nite time. While this is in general undecidable, various elds of computational logic and declarative problem solving have developed techniques that provide e ective solutions for a broad and practically important class of such problems. We envision to combine existing methods, to generalize them and to add novel ones.
Our main context for this work will be the eld of lifted reasoning. Possible (and
interrelated) techniques in this eld that aid with reasoning over in nite domains
are:
Lazy grounding
Bounds propagation for sets: Using several set-axioms and number-theoretic properties, it might be possible to deduce bounds for sets which are not constrained to a nite domain explicitly by the modelling. This greatly reduces the costs of grounding as it can cause large domains to be limited to much smaller, better tractable domains.
Propagation of homogeneity in subdomains for co nite sets: Even if a set contains an in nite number of elements, its elements might deviate from a simple default rule in only a nite number of situations. This means that there is a certain homogeneity or simple de ning relation for the remainder of the sets domain, and, given this prescription for the set, only a small set of additional values carries additional (meaningful) information. Because of this, for several inference tasks it can prove unnecessary to enumerate the entire set, instead reasoning only on the combination of the prescription and the small complementary set to solve the task at hand.
Specialized algorithms: specialized and e cient algorithms for set operations
Oracles: The use of subsolvers as oracles is a promising avenue for supporting higher order quanti cation over predicates. The necessary search is performed by a subsolver which is given a theory that describes all constraints over the quanti ed predicate. Using negation, universal quanti cation over a predicate is turned into existential quanti cation. As a result, it is possible to rewrite every quanti cation into an existential Second Order theory (or search problem) that a subsolver can tackle.
The subsolver answers whether the new theory is satis able, and if so, the correct conclusions about the super-theory are inferred, and if possible, propagated. The performance of these subsolvers, as well as how much information can be shared between them and the optimal level of granularity that decides when a subsolver must run, is the subject of ongoing research.
As an example, consider a shipping dock with multiple separate docking segments and ships. We want to package a large payload in (as few as possible) smaller load that we can later distribute over the ships. However, we do not know which ship will be placed in which dock, and every dock and ship has a maximal load capacity that it can bear. We can express this as follows: 9Weight[Package 7! Int] : 8Place[Ship 7! Dock] : 9Distri[Package 7! Ship] : 8ship : sumfpack[Package] : Distri(pack) = ship : Weight(pack)g
< min(dockCap(Place(ship)); shipCap(ship)): Informally, this must be read as follows: there exists a function Weight that gives the weight for each package, such that for every placement of ships in docking segments there exists a distribution Distri of the packages over the ships such that the maximal capacity of neither ship nor dock is exceeded. Here, the universal quanti cation over the placement predicate Place can be transformed to existential quanti cation by negating the remainder of the logical sentence, which will be solved by a subsolver. We will require that this subsolver proves unsatis ability, as the transformation from universal to existential quanti cation introduces a negation before and after the quanti cation. Note that this introduces a negation before the existential quanti Higher Order Support in Logic Speci cation Languages for Data Mining Applications 5 cation of the Distri predicate, which in the naive schemes results in another subsolver.
These techniques are called \lifted reasoning" because the reasoning task is partly done at the predicate level, as opposed to the current state-of-the-art that defers all reasoning until after the grounding phase, when it can be done on propositional level.
The development and adaptation of these techniques will pose theoretical and implementation challenges.
Furthermore, signi cant software architectural questions must be answered to insert these techniques in the classical two phase system with the appropriate level of modularity and encapsulation.
The goal of this research is to add higher order support to logic speci cation languages running on ground-and-solve systems, speci cally with data representation and data mining applications in mind. These higher order support will come in the form of structured recursive types, generic types, and relations as rst class citizens.
We expect that these additional features make data handling and reasoning more natural, and that they allow us to write shorter, more speci c and modular speci cations. These modular speci cations should then be combined into a larger speci cation for solving larger problems, leading the way for a software design methodology for logical speci cations.
We expect to provide an implementation of the ideas and results stemming from this research for the FO( ) language and the IDP system that supports and provides inferences for this language.
Current research topics consist of analyzing how the work on lazy grounding
From all possible justi cation graphs, the relevance of certain literals can be deduced. Some literals are irrelevant: the truth values of these literals does not matter for the truth value of the program. Combining relevance derived from the justi cation graph together with lazy grounding will likely lead to ways of e ciently handling predicates with an in nite domain by not providing an interpretation for subdomains where the predicate can be chosen freely.
This hypothesis of course needs an experimental evaluation on a well-chosen set of real world problems. We expect to publish at least one summary of the devised methods and their evaluation to be written for publication, as well as an IDP release with full support for lazy grounding.
Furthermore, we investigate our hypothesis that the justi cation graph of predicates will allow us to learn characterizations of the `behavior' of a predicate on large (in nite) parts of its domain, which can be used for lifted clause learning. The idea is that these clauses can then adequately describe the properties of the predicate, without having to compute it fully. For example, an arbitrary predicate could, by analysis of its justi cation graph, be detected to be an ordered list of ve elements of a generic type, leading to a new representation as:
ve constants of a generic type, a constraint that all 5 constants have the same type a, a constraint that a must contain at least 5 domain elements, and provide an ordering.
Moreover, we are exploring how the concept of oracles can be implemented using the idea of subcalls to the same solver. To this e ect, we are looking at ways to share information, data structures and other necessary information between di erent solver calls, with the aim of reducing overhead and setup costs. Later, we will round up our ndings regarding oracles for publication.
We are also collecting a benchmark set and use this to test how eager the system must be to perform a subsolver call, as well as how detailed the learned clauses should be when a subsolver does not produce the wanted result, i.e. represents a con ict. Using this benchmark set, we will evaluate the di erent answers to the questions above and publish a paper detailing these experimental results. It will also provide us with an important indication on whether to publish an IDP version incorporating these techniques.
Lastly, we're looking at set theory as supported by the B method
Higher Order Support in Logic Speci cation Languages for Data Mining Applications 7