Incremental Theorem Proving
S. Andrei, A. Cheng, G. Grigoras, L. Osborne
Abstract
Theorem proving is a challenging task for formal verification of systems. There exist many efforts to efficiently solve this problem, based for example on rewriting rules and/or SAT-based techniques. We propose an alternative of SAT-based techniques by using instead a counting SAT-based technique (denoted also #SAT). A SAT solver tests if a propositional formula F has at least one truth assignment, while a #SAT solver returns the number of truth assignments of F. For efficiency reasons, many of the existing SAT-based techniques are applied incrementally, that is, using the satisfiability of some sub-formulas to determine the satisfiability of a given formula. While there exist incremental SAT solvers, to the best of our knowledge, our paper presents first time the theoretical background for the incremental counting satisfiability problem. Being a more general technique than the existing works, our approach can be used to handle all the problems solved by SAT solvers. Moreover,our #SAT solver outperforms a SAT solver when considering the challeging problemsof re-design or debugging of systems.

Analysis of Exchanging Interactions in Some Parallel Algorithms of the Linear Equational System
N. Vasilev
Abstract
This paper analyses and minimizes the exchanging interactions in the parallel algorithm of type “allocation of submatrices with identical dimensions in the processors of computer system with parallel architecture” of the linear equational system, solved by the method of sequential interations.

Combined Adaptive Algorithms for States and Parameters Estimation in Control Systems
N. Madjarov, T. Slavov
Abstract
In this paper two adaptive algorithms for the recursive parameters and the state estimation in linear discrete-time systems are proposed. These algorithms combine the standard least square method with the conventional stochastic state observer (Kalman filter). The Kalman filter improves estimates quality, obtained with the least square method, in the sense of their consistency. These algorithms can be part of a stochastic control system with indirect adaptation software. The comparison with another often used in practice estimation algorithms as well as algorithms for adaptive control (with indirect adaptation) based on conventional algorithms are presented.

Object-oriented Computer - aided Learning Design System Development
E. Shoikova, M. Ivanova
Abstract
This paper describes the object-oriented development of - Computer-aided Learning Design System as a result of the project carried out at the Technical University of Sofia, the R&D Laboratory “eLearning Technologies”. The system assists educators and other learning design professionals in their units of learning analysis and design activities and deliver effective support, promoting the exchange and interoperability of eLearning scenarios. The development methodology includes the Rational Unified Process as a successful development strategy; Unified Modeling Language for clarifying the requirements, architectures and designs, Use Case Analysis to elicit, organize, and document required system functionality; the concepts of forward software engineering to build the high-quality system. The system is realized as an integrated part of the open source standard-based eLearning platform ATutor.

An Approach to Provide Network Capabilities-based Added Value
I. Atanasov, E. Pencheva
Abstract
A new mark-up approach to next generation service creation is proposed. The approach can be summarized as development of a scripting language SLPL that exploits OSA (Open Service Access) service capability features like mobility, call control, data session control, messaging, user interaction etc. Language constructions for data types and method definitions, flow control, time measuring and supervision, database access are provided. Examples of SLPL descriptions are presented.

Some Aspects of LFU-RBH: A Replacement Algorithm for Database Disk Buffering
I. Atanassov
Abstract
Disk buffering is an important aspect of every computer system. In modern computer systems, the performance gap between the volatile memory and the non-volatile storage systems is in powers of ten. Therefore, the disk block reads/writes can be the bottleneck of the system. A major factor for increasing the overall performance is improving the cache management. Operating systems offer caching to improve I/O performance. Database systems also have a disk cache. Most of the cases it is implemented as a LRU buffer or a variant of it. The present paper offers an algorithm, which tries to take advantage of the frequency aspect and also to reduce the disadvantages of the pure LFU policy. Experiments are conducted to estimate the behavior of the algorithm and the various parameters.

Seed Quality Assessment Using Artificial Neural Networks
M. Mladenov, M. Dejanov
Abstract
This paper discusses the possibility of seed quality assessment using artificial neural networks. We present a model of a classifier based on a cascade structure, which consists of different standard neural networksLVQ networks and BPN. The classifier provides a precise classification of multidimensional vectors in classes with contacted boundaries. The classifier has an acceptable training resource. This problem is related to quality assessment of different products including seeds.In this paper the classifier is used for separation quality assessment based on geometrical parameters of corn seeds. These parameters are measured by a standard measurement method and a computer vision system. The results obtained by the proposed classifier are compared with results using the standard BP and RBF networks. If the seed dimensions are measured by the standard method the classifier gives a correct classification of all seeds. When the dimensions are measured by the computer vision system the classification accuracy is about 94.2%.