Vol. 34 · No. 2

In this paper, we propose a formal model of the objects involved in a class of scheduling problems, namely in the classroom scheduling in universities which allow a certain degree of liberty in their curricula. Using the formal model, we present efficient algorithms for the detection of collisions of the involved objects and for the inference of a tree-like navigational structure in an interactive scheduling software allowing a selection of the most descriptive view of the scheduling objects. These algorithms were used in a real-world application called MetroNG; a visual interactive tool that is based on more than 10 years of experience we have in the field. It is currently used by the largest universities and colleges in the Czech Republic. The efficiency and usability of MetroNG suggests that our approach may be applied in many areas where multi-dimensionally structured data are presented in an interactive application.

The purpose of the PatOMat transformation framework is to bridge between different modeling styles of web ontologies. We provide a formal model of pattern-based ontology transformation, explain its implementation in PatOMat, and manifest the flexibility of the framework on diverse use cases.

The problem of proof simplification draws a lot of attention to itself across various contexts. In this paper, we present one approach for simplifying proofs constructed in the framework of coherent logic. This approach is motivated by the need for filtering-out ``clean'' and short proofs from proof-traces, which typically contain many irrelevant steps, and which are generated by automated theorem provers – in this case, theorem provers based on coherent logic. Such ``clean'' proofs can then be used for producing readable proofs in natural-language form. The proof simplification procedure consists of three transformation steps. The first one is based on the elimination of inference steps which are irrelevant for the present proof, also allowing some irrelevant branchings to be eliminated, the second one consists of lifting-up steps through the branching steps, followed by elimination of repeated steps, while the third one serves to convert proof fragments into the reductio ad absurdum form, if possible. In contrast to general simplification procedures, our proof simplification procedure is specific for a fragment of first order logic and therefore simple and easy to implement, and allows simple generation of object level proofs. We proceed to prove that this procedure is correct and terminating, and also that it never increases the size of a proof. Finally, we implement the proof simplification procedure, and provide several example proofs.

This paper focuses on a design case study of a natural hand gesture system for users with intact motion control of the metacarpophalangeal joint and thumb basal joint of the hand after brachial plexus injuries. The lexicon of hand gestures had eight entries and was demonstrated to be natural and ergonomic with the limited hand motions. A cooperative multi-cue system was proposed for the key hand posture recognition of the proposed hand gestures. We utilized the designed system into a remote smart car control and electric wheelchair control. Experimental a results demonstrated the robustness and potential feasibility of the system in human-computer interaction for the proposed users.

Old printed documents represent an important part of our cultural heritage. Their digitalization plays an important role in creating data and metadata. The paper proposed an algorithm for estimation of the global text skew. First, document image is binarized reducing the impact of noise and uneven illumination. The binary image is statistically analyzed and processed. Accordingly, redundant data have been excluded. Furthermore, the convex hulls are established encircling each text object. They are joined establishing connected components. Then, the connected components in complementary image are enlarged with morphological dilation. At the end, the biggest connected component is extracted. Its orientation is similar to the global orientation of text document which is calculated by the moments. Efficiency and correctness of the algorithm are verified by testing on a custom dataset.

The performance of data grids for data intensive, real-time applications is highly dependent on the data dissemination algorithm employed in the system. Motivated by this fact, this study first formally defines the real-time splittable data dissemination problem (RTS/DDP) where data transfer requests can be routed over multiple paths to maximize the number of data transfers to be completed before their deadlines. Since RTS/DDP is proved to be NP-hard, four different heuristic algorithms, namely kSP/ESMP, kSP/BSMP, kDP/ESMP, and kDP/BSMP are proposed. The performance of these heuristic algorithms is analyzed through an extensive set of data grid system simulation scenarios. The simulation results reveal that a performance increase up to 8

We consider two graph grammar based Petri nets models for anisotropic refinements of three dimensional hexahedral grids. The first one detects possible dead-end problems during the graph grammar based anisotropic refinements of the mesh. The second one employs an enhanced graph grammar model that is actually dead-end free. We apply the resulting algorithm to the simulation of resistivity logging measurements for estimating the location of underground oil and/or gas formations. The graph grammar based Petri net models allow to fix the self-adaptive mesh refinement algorithm and finish the adaptive computations with the required accuracy needed by the numerical solution.

Data intensive peer-to-peer (P2P) networks are becoming increasingly popular in applications like social networking, file sharing networks, etc. Data mining in such P2P environments is the new generation of advanced P2P applications. Unfortunately, most of the existing data mining algorithms do not fit well in such environments since they require data that can be accessed in its entirety. It also is not easy due to the requirements of online transactional data streams. In this paper, we have developed a local algorithm for tracing frequent item sets over a P2P network. The performance of the proposed algorithm is comparatively tested and analyzed through a series of experiments.

In the early days of computing, files where just a natural way of storing information – which reflected the way one would file their punch cards in a cabinet drawer. Unfortunately, the requirement to fragment information into such chunks, is a huge bottleneck for the evolution of global information space that the Internet has become. The concept of file causes several problems including unnatural clustering of information, unnecessary replication of data and very expensive information discovery in distributed computing environments. The overall goal of this work is to design an architecture enabling new era in computing and networking – a computing infrastructure without the concept of file. Files are seen by many specialists as one of the main bottlenecks of modern IT systems evolution. This is mostly due to a very unnatural fragmentation of information into chunks which are easier to manage by operating systems but much more difficult for information processing tools and eventually by humans themselves.

Motivated by the recent applications of the conjugate residual method to nonsymmetric linear systems by Sogabe, Sugihara and Zhang [An extension of the conjugate residual method to nonsymmetric linear systems. J. Comput. Appl. Math., Vol. 266, 2009, pp. 103–113], this paper describes two conjugate direction methods, BiCR and BiCG, and attempts to extend their applications to compute the stationary probability distribution for an irreducible Markov chain with the aim of finding an alternative basic solver. Numerical experiments show the feasibility of the BiCR and BiCG to some extent, with applications to several practical Markov chain problems.