Proof systems for planning under 0-approximation semantics

In this paper we propose Hoare style proof systems called PR0Dand PRKW0Dfor plan generation and plan verification under 0-approximation semantics of the action language AK.In PR0D(resp.PRKW0D),a Hoare triple of the form{X}c{Y}(resp.{X}c{KWp})means that all literals in Y become true(resp.p becomes known)after executing plan c in a state satisfying all literals in X.The proof systems are shown to be sound and complete,and more importantly,they give a way to efficiently generate and verify longer plans from existing verified shorter plans by applying so-called composition rule,provided that an enough number of shorter plans have been properly stored.The idea behind is a tradeoff between space and time,we refer it to off-line planning and point out that it could be applied to general planning problems.     

Dynamic Regular Plans and Rebroadcasting for Mobile Clients

The broadcast problem including the plan design is considered. The data are inserted and numbered into customized size relations at a predefined order. The server ability to create a full, RBP （regular broadcast plan） with single and multiple channels after some data transformations is examined. The BRA （basic regular algorithm） prepares an RBP and enables users to catch their items while avoiding wasting energy by their devices. In the case of multiple channels, a dynamic grouping solution is proposed, called the PVA （partition value algorithm） under a multiplicity constraint. A FPVA （fast type of PVA） that uses small size of the integrated relations can decrease the delay. The PVACF （PVA with complete filling）, using a parameter of the cold set, can provide solution for the discovery of the RBP. In order to provide consistency in data values the RRD （rebroadcasting of regular data） Algorithm is presented. The delay differentiation of services is also examined. The above properties can enrich the servers＇ operational capabilities, beyond their self-monitoring and self-organizing features. Channel availability and lower energy consumption can be provided by using a smaller, with equal bandwidth, number of channels. Simulation results are provided. Simulation results are provided.     

Role of Metacognition in Mathematical Problem Solving Process of Permutations and Combinations--Basic Study for CAI Software Development

When solving a mathematical problem, we sometimes encounter a situation where we can not reach a correct answer in spite of acquiring knowledge and formula necessary for the solution. The reason can be attributed to the lack in metacognitive abilities. Metacognitive abilities consist of comparing the difficulty of problem with own ability, proper plan of solution process, and conscious monitoring and control of solution process. The role and importance of metacognitive ability in mathematical problem solving of permutations and combinations was explored. Participants were required to solve five practical problems related to permutations and combinations. For each problem, the solution process was divided into： （1） understanding （recognition） of mathematical problem; （2） plan of solution; （3） execution of solution. Participants were also required to rate the anticipation whether they could solve it or not, and to rate the confidence of their own answer. According to the total score of five problems, the participants were categorized into the group of the high test score and the group of the low test score. As a result, at the plan and the execution processes, statistically significant differences were detected between the high and the low score groups. As for the rating on the anticipation of result and the confidence of own answer, no significant differences were found between both groups. Moreover, the relationship between the score of plan process and the score of execution process was statistically correlated. In other words, the more proper the plan process was conducted, the more proper solution the participants reached. In such a way, the importance of metacognitive ability in the solving process, especially the plan ability, was suggested.     

Metacognition in Solving Process of Basic Electric Circuit ProblemmComparison of Metacognitive Characteristics between Non-major and Major Students in Electric Engineering

There are learners who cannot solve practical problems in spite of mastering basic scientific knowledge and formula necessary for the solution. One of the reasons might be attributed to the lack in metacognitive abilities. The aim of this study was to compare the metacognitive characteristics between non-major and major students in electric engineering and clarify the difference of metacognitive process between these two groups when solving basic problems of electronic circuit. In the experiment, the solving process was compared between non-major and major students in electric engineering using five basic problems. We found that the scores on prediction of result and confidence of own answer differed significantly between non-major and major students, and inferred that the difference of performance was due to the lack in metacognitive ability, especially the plan and the execution abilities. Both prediction of results and confidence of own answer were also found to play a significant role in effective problem solving as important components （subsystems） of metacognition.     

Key Technologies for SON in Next Generation Radio Access Networks

The aim of SON （self-organizing network） is to realize the autonomic function of the wireless network by self-configuration, self-optimization and self-healing, which reduces the human intervention and improves the user experience, Self-configuration is a process where newly deployed eNodeBs are configured by automatic installation procedures to get the necessary basic configuration for system operation. Self-optimization is a process that continuously monitors an environment and automatically optimizes various parameters when the environment changes. Self-healing is a process that detects and localizes failures, then fixes the problems automatically. This paper gives a comprehensive introduction to the SON functionalities and outlines the framework of self-configuration, self-optimization and self-healing. Some concrete algorithms are proposed for self-optimization and self-healing, which include capacity and coverage optimization and cell outage detection and compensation respectively. Simulation results in various scenarios are provided to evaluate the performance of the proposed algorithms.     

Improved construction for universality of determinant and permanent

Valiant [L. Valiant, Completeness classes in algebra, in: Proc. 11th Annual ACM Symposium on the Theory of Computing, Atlanta, GA, 1979, pp. 249–261] proved that every polynomial of formula size e is a projection of the (e+2)×(e+2) determinant polynomial. We improve “e+2” to “e+1”, also for a definition of formula size that does not count multiplications by constants as gates. Our proof imitates the “2e+2” proof of von zur Gathen [J. von zur Gathen, Feasible arithmetic computations: Valiant's hypothesis, Journal of Symbolic Computation 4 (1987) 137–172], but uses different invariants and a tighter set of base cases.     

LΩUI: Lovely ΩMEGA User Interface

The capabilities of a automated theorem prover's interface are essential for the effective use of (interactive) proof systems. LΩUI is the multi-modal interface that combines several features: a graphical display of information in a proof graph, a selective term browser with hypertext facilities, proof and proof plan presentation in natural language, and an editor for adding and maintaining the knowledge base. LΩUI is realized in an agent-based client-server architecture and implemented in the concurrent constraint programming language Oz. Received November 1998 / Accepted in revised form June 1999     

采掘工程平面图自动绘制系统

为了实现煤矿矿山测量的标准和自动化,文讨论了采掘工程平面图自动化绘制系统的设计,并以ＡｕｔｏＣＡＤ为平台开发研制了采掘工程平面图自动制系统,系统经过煤矿的运行使用,取得了显著的经济和社会效益,说明该系统具有很强的实用性,规范性,可靠性,灵活性和易操作性等特点。     

Nonexistence of finite-dimensional filters for conditional statistics of the cubic sensor problem

Consider the cubic sensor dx = dw, dy = x³dt + dv where w, v are two independent Brownian motions. Given a function φ(x) of the state x let φ_t(x) denote the conditional expectation given the observations y_s, 0 s t. This paper consists of a rather detailed discussion and outline of proof of the theorem that for nonconstant φ there cannot exist a recursive finite-dimensional filter for φ driven by the observations.     

An object-oriented approach to teaching mathematics for engineering and science students

It is suggested to teach mathematics for engineering and science students as exploration of mathematics-related classes. Similarity with classes and objects of object-oriented programming is demonstrated. In the framework of the suggested approach, each relatively self-contained unit of mathematics curriculum is assigned a data type and is considered a class. In such setting, a theorem proof may be viewed as an assignment of values to object properties. The approach augments the role of recognition of mathematical objects, their properties and methods （operations） and diminishes the value of comprehensive study of rigorous proofs. The approach emphasizes the importance of development of mathematical intuition and combines conceptual and operational approaches to teaching and learning mathematics. Prospective implementation assumes using of computer-based systems of formal proof.     

Performance Evaluation of Antenna Receive Diversity in SlMO-OFDM System over Rayleigh Fading Channel

This paper represents a comparative performance evaluation of different diversity combining techniques for a SIMO-OFDM （single-input-multiple-output orthogonal frequency division multiplexing） system over Rayleigh fading channel. OFDM is a key technique for achieving high data rates and spectral efficiency requirements for wireless communication systems. But in scattering environment, the system performances are severely degraded by the effects of multipath fading and inter-symbol interference. In wireless communication systems, antenna diversity is an important technique to combat multipath fading in order to improve the system performance and increase the channel capacity. In this paper, the performance of different diversity combining techniques-SC （selection combining）, EGC （equal gain combining） and MRC （maximal ratio combining） has been analyzed and compared in terms of SNR （signal to noise ratio） and BER （bit error rate） probability. The simulation results show that the maximal ratio combining technique provides maximum performance improvement relative to all other combining schemes by maximizing the SNR of SIMO-OFDM system at the combiner output. The analytic expressions of error probability and effective bit energy to noise ratio correlated with BPSK （binary phase shift keying） modulation have been derived and formulated for N-branch SC, EGC and MRC schemes. The BER characteristics for all three combining techniques are simulated in MATLAB （matrix laboratory） tool box for varying bit energy to noise ratio. Our results also derives that SNR can be improved if the number of receiving antenna is increased, which in turn reduces BER over a Rayleigh fading channel.     

Counterworking the Operation Disturbance of a Radiators Structure due to External Actions

The operation of a complicated radiators structure creating a required field in a given area is disturbed often due to different external actions. As an example, the impact of metallic objects approaching off to an antenna system with minimal irradiation on user＇s body is analyzed. In this case, the zone itself, where the area of a weak field （a dark spot） is created, is generally not approachable for sensors installation. In order to counteract the disturbance of the system operation due to presence of different metallic objects in close proximity to the radiators, two methods based on two information sources are studied. These information sources are antennas driving currents and fields at a predetermined point outside the given area. As an example, the antenna system used in the compensation method for reducing human＇s body irradiation, to which a metal object approaches, is analyzed. The conditions of severe external actions are considered： a great metal body and a small distance from this body to the dark spot. It is shown that under these conditions of severe external actions the second method based on the field values measuring demonstrates a higher efficiency. A block scheme for structure of an automatic adjustment is suggested. The considered problem is a common one, and developers of radio circuits are faced with them constantly.     

Normalized Efficient Routing Protocol for WSN

WSNs （wireless sensor networks） consist of thousands of tiny nodes having the capability of sensing, computation, and wireless communications. Unfortunately these devices are limited energy devices, that is means we must save energy as much as possible, to increase network life time as long as possible. In this paper we introduce NEER--normalized energy efficient routing protocol that increases network life time through switching between AODV protocol that depends on request-reply routing, and MRPC that depends on residual battery in routing.     

From IP to Start-up： Building a Robust Life Science Incubator

An incubator is an organization that supports new ventures to grow and survive during the early stages. Mainly dedicated to information technology, life science may appear to be the next hot spot for incubators. Are there stabilized good practices？ Are the business models in information technology and in life science comparable when it goes to start-ups＇ incubation？ Leveraging our experience as practitioner in this field and using an inductive methodology, this paper tends to propose simple principles to help build robust incubators in life science, and to contribute to disseminate an entrepreneurial approach through an industry still dominated by blue chips.     

Towards estimating computer users＇ mood from interaction behaviour with keyboard and mouse

The purpose of this exploratory research was to study the relationship between the mood of computer users and their use of keyboard and mouse to examine the possibility of creating a generic or individualized mood measure. To examine this, a field study （n = 26） and a controlled study （n = 16） were conducted. In the field study, interaction data and self-reported mood measurements were collected during normal PC use over several days. In the controlled study, participants worked on a programming task while listening to high or low arousing background music. Besides subjective mood measurement, galvanic skin response （GSR） data was also collected. Results found no generic relationship between the interaction data and the mood data. However, the re- suits of the studies found significant average correlations be- tween mood measurement and personalized regression models based on keyboard and mouse interaction data. Together the results suggest that individualized mood prediction is pos- sible from interaction behaviour with keyboard and mouse.     

A 2.4 GHz low power CMOS transceiver for LR-WPAN applications

A 2.4 GHz low power transceiver for low-rate wireless personal area network(LR-WPAN)applications is presented.The optimized low-IF receiver consists of a novel current reuse RF front-end with an inductor-less-load balun LNA and quadrature mixer,and an adaptive analog baseband to reduce power and area.It achieves-94 dBm of sensitivity,-9 dBm of IIP3 and 28 dBc of image rejection.The phase-locked loop based direct phase modulated transmitter is proposed to reduce power and deliver a+3 dBm output power.The phase noise of the low power frequency synthesizer with current reuse stacked LC-VCO achieves-107.8 dBc/Hz at 1 MHz offset.An ultra-low power nonvolatile memory is used to store configuration data and save power.The chip is implemented in a 0.18μm CMOS process,and the area is less than 2.8 mm2.The transceiver consumes only 10.98 mW in the receiving mode and 13.32 mW in the transmitting mode.     

Wideband Rectangular and Circular Microstrip Antennas Loaded with U-Shaped Slot

In this paper, a dual frequency resonance antenna is analysed by introducing U-shaped slot in a rectangular and circular patch, the results in terms of return loss, input impedance and radiation pattern are given. It is observed that various antenna parameters are obtained as a function of frequency for different value of slot length and width; it is easy to adjust the upper and the lower band by varying these different antenna parameters. The coaxial feed is used to excite the patch antenna. All the theoretical results using Matlab are compared with the simulated results obtained from Ansoft HFSS which are in close agreement. Furthermore, comparative study between our results and those available in the literature is done and showed to be in good agreement.     

Real-time control of human actions using inertial sensors

Our study proposes a new local model to accurately control an avatar using six inertial sensors in real-time.Creating such a system to assist interactive control of a full-body avatar is challenging because control signals from our performance interfaces are usually inadequate to completely determine the whole body movement of human actors.We use a pre-captured motion database to construct a group of local regression models,which are used along with the control signals to synthesize whole body human movement.By synthesizing a variety of human movements based on actors’control in real-time,this study verifies the effectiveness of the proposed system.Compared with the previous models,our proposed model can synthesize more accurate results.Our system is suitable for common use because it is much cheaper than commercial motion capture systems.     

Remote-Controlled Ambidextrous Robot Hand Concept

In the development of robotic limbs, the side of members is of importance to define the shape of artificial limbs and the range of movements. It is mainly significant tbr biomedical applications concerning patients suffering arms or legs injuries, fn this paper, the concept of an ambidextrous design lbr robot hands is introduced. The fingers can curl in one xvay or another, to imitate either a right hand or a left hand. The advantages and inconveniences of different models have been investigated to optimise the range and the maximum force applied by fingers. Besides, a remote control interthce is integrated to the system, allowing both to send comrnands through internet and to display a video streaming of the ambidextrous hand as feedback. Therefore, a robotic prosthesis could be used for the first time in telerehabilitation. The main application areas targeted are physiotherapy alter strokes or management of phantom pains/br amputees by/earning to control the ambidextrous hand. A client application is also accessible on Facehook social network, making the robotic limb easily reachable for the patients. Additionally the ambidextrous hand can be used tbr robotics research as well as artistic performances.