OpenRaiser/Intern-Atlas huggingface dataset:
Towards an Intelligent Tutor for Mathematical Proofs
Venue: arXiv cs.AI 2012
Year: 2012

Computer-supported learning is an increasingly important form of study since it allows for independent learning and individualized instruction. In this paper, we discuss a novel approach to developing an intelligent tutoring system for teaching textbook-style mathematical proofs. We characterize the particularities of the domain and discuss common ITS design models. Our approach is motivated by phenomena found in a corpus of tutorial dialogs that were collected in a Wizard-of-Oz experiment. We show how an intelligent tutor for textbook-style mathematical proofs can be built on top of an adapted assertion-level proof assistant by reusing representations and proof search strategies originally developed for automated and interactive theorem proving. The resulting prototype was successfully evaluated on a corpus of tutorial dialogs and yields good results.
Integrating DGSs and GATPs in an Adaptative and Collaborative Blended-Learning Web-Environment
Venue: arXiv cs.CG 2012
Year: 2012

The area of geometry with its very strong and appealing visual contents and its also strong and appealing connection between the visual content and its formal specification, is an area where computational tools can enhance, in a significant way, the learning environments. The dynamic geometry software systems (DGSs) can be used to explore the visual contents of geometry. This already mature tools allows an easy construction of geometric figures build from free objects and elementary constructions. The geometric automated theorem provers (GATPs) allows formal deductive reasoning about geometric constructions, extending the reasoning via concrete instances in a given model to formal deductive reasoning in a geometric theory. An adaptative and collaborative blended-learning environment where the DGS and GATP features could be fully explored would be, in our opinion a very rich and challenging learning environment for teachers and students. In this text we will describe the Web Geometry Laboratory a Web environment incorporating a DGS and a repository of geometric problems, that can be used in a synchronous and asynchronous fashion and with some adaptative and collaborative features. As future work we want to enhance the adaptative and collaborative aspects of the environment and also to incorporate a GATP, constructing a dynamic and individualised learning environment for geometry.
The Dissecting Power of Regular Languages
Venue: arXiv cs.FL 2012
Year: 2012

A recent study on structural properties of regular and context-free languages has greatly promoted our basic understandings of the complex behaviors of those languages. We continue the study to examine how regular languages behave when they need to cut numerous infinite languages. A particular interest rests on a situation in which a regular language needs to "dissect" a given infinite language into two subsets of infinite size. Every context-free language is dissected by carefully chosen regular languages (or it is REG-dissectible). In a larger picture, we show that constantly-growing languages and semi-linear languages are REG-dissectible. Under certain natural conditions, complements and finite intersections of semi-linear languages also become REG-dissectible. Restricted to bounded languages, the intersections of finitely many context-free languages and, more surprisingly, the entire Boolean hierarchy over bounded context-free languages are REG-dissectible. As an immediate application of the REG-dissectibility, we show another structural property, in which an appropriate bounded context-free language can "separate with infinite margins" two given nested infinite bounded context-free languages.
Algorithms for Sampling 3-Orientations of Planar Triangulations
Venue: arXiv cs.DS 2012
Year: 2012

Given a planar triangulation, a 3-orientation is an orientation of the internal edges so all internal vertices have out-degree three. Each 3-orientation gives rise to a unique edge coloring known as a Schnyder wood that has proven powerful for various computing and combinatorics applications. We consider natural Markov chains for sampling uniformly from the set of 3-orientations. First, we study a "triangle-reversing" chain on the space of 3-orientations of a fixed triangulation that reverses the orientation of the edges around a triangle in each move. It was shown previously that this chain connects the state space and we show that (i) when restricted to planar triangulations of maximum degree six, the Markov chain is rapidly mixing, and (ii) there exists a triangulation with high degree on which this Markov chain mixes slowly. Next, we consider an "edge-flipping" chain on the larger state space consisting of 3-orientations of all planar triangulations on a fixed number of vertices. It was also shown previously that this chain connects the state space and we prove that the chain is always rapidly mixing. The triangle-reversing and edge-flipping Markov chains both arise in the context of sampling other combinatorial structures, such as Eulerian orientations and triangulations of planar point sets, so our results here may shed light on the mixing rate of these related chains as well.
A Planarity Test via Construction Sequences
Venue: arXiv cs.DS 2012
Year: 2012

Optimal linear-time algorithms for testing the planarity of a graph are well-known for over 35 years. However, these algorithms are quite involved and recent publications still try to give simpler linear-time tests. We give a simple reduction from planarity testing to the problem of computing a certain construction of a 3-connected graph. The approach is different from previous planarity tests; as key concept, we maintain a planar embedding that is 3-connected at each point in time. The algorithm runs in linear time and computes a planar embedding if the input graph is planar and a Kuratowski-subdivision otherwise.
The Stretch Factor of $L_1$- and $L_\infty$-Delaunay Triangulations
Venue: arXiv cs.CG 2012
Year: 2012

In this paper we determine the stretch factor of the $L_1$-Delaunay and $L_\infty$-Delaunay triangulations, and we show that this stretch is $\sqrt{4+2\sqrt{2}} \approx 2.61$. Between any two points $x,y$ of such triangulations, we construct a path whose length is no more than $\sqrt{4+2\sqrt{2}}$ times the Euclidean distance between $x$ and $y$, and this bound is best possible. This definitively improves the 25-year old bound of $\sqrt{10}$ by Chew (SoCG '86). To the best of our knowledge, this is the first time the stretch factor of the well-studied $L_p$-Delaunay triangulations, for any real $p\ge 1$, is determined exactly.
Sequential Coding of Markov Sources over Burst Erasure Channels
Venue: arXiv cs.IT 2012
Year: 2012

We study sequential coding of Markov sources under an error propagation constraint. An encoder sequentially compresses a sequence of vector-sources that are spatially i.i.d. but temporally correlated according to a first-order Markov process. The channel erases up to B packets in a single burst, but reveals all other packets to the destination. The destination is required to reproduce all the source-vectors instantaneously and in a lossless manner, except those sequences that occur in an error propagation window of length B + W following the start of the erasure burst. We define the rate-recovery function R(B, W) - the minimum achievable compression rate per source sample in this framework - and develop upper and lower bounds on this function. Our upper bound is obtained using a random binning technique, whereas our lower bound is obtained by drawing connections to multi-terminal source coding. Our upper and lower bounds coincide, yielding R(B, W), in some special cases. More generally, both the upper and lower bounds equal the rate for predictive coding plus a term that decreases as 1/(W+1), thus establishing a scaling behaviour of the rate-recovery function. For a special class of semi-deterministic Markov sources we propose a new optimal coding scheme: prospicient coding. An extension of this coding technique to Gaussian sources is also developed. For the class of symmetric Markov sources and memoryless encoders, we establish the optimality of random binning. When the destination is required to reproduce each source sequence with a fixed delay and when W = 0 we also establish the optimality of binning.
How to Bypass Verified Boot Security in Chromium OS
Venue: arXiv cs.CR 2012
Year: 2012

Verified boot is an interesting feature of Chromium OS that supposedly can detect any modification in the root file system (rootfs) by a dedicated adversary. However, by exploiting a design flaw in verified boot, we show that an adversary can replace the original rootfs by a malicious rootfs containing exploits such as a spyware or keylogger and still pass the verified boot process. The exploit is based on the fact that a dedicated adversary can replace the rootfs and the corresponding verification information in the bootloader. We experimentally demonstrate an attack using both the base and developer version of Chromium OS in which the adversary installs a spyware in the target system to send cached user data to the attacker machine in plain text which are otherwise encrypted, and thus inaccessible. We also demonstrate techniques to mitigate this vulnerability.
Organizing the Aggregate: Languages for Spatial Computing
Venue: arXiv cs.PL 2012
Year: 2012

As the number of computing devices embedded into engineered systems continues to rise, there is a widening gap between the needs of the user to control aggregates of devices and the complex technology of individual devices. Spatial computing attempts to bridge this gap for systems with local communication by exploiting the connection between physical locality and device connectivity. A large number of spatial computing domain specific languages (DSLs) have emerged across diverse domains, from biology and reconfigurable computing, to sensor networks and agent-based systems. In this chapter, we develop a framework for analyzing and comparing spatial computing DSLs, survey the current state of the art, and provide a roadmap for future spatial computing DSL investigation.
(Really) Tight bounds for dispatching binary methods
Venue: arXiv cs.DS 2012
Year: 2012

We consider binary dispatching problem originating from object oriented programming. We want to preprocess a hierarchy of classes and collection of methods so that given a function call in the run-time we are able to retrieve the most specialized implementation which can be invoked with the actual types of the arguments. For the binary dispatching, where the methods take exactly two arguments, logarithmic query time is possible, even if the structure is allowed to take linear space. Unfortunately, known solutions achieving such complexity require superlinear time for constructing the structure. Using a different idea we are able to construct in (deterministic) linear time and space a structure allowing dispatching binary methods in the same logarithmic time. Then we show how to improve the query time to slightly sublogarithmic, which is easily seen to be optimal as a consequence of some already known lower bounds if we want to keep the size of the resulting structure close to linear.
A Novel Fractional Order Fuzzy PID Controller and Its Optimal Time Domain Tuning Based on Integral Performance Indices
Venue: arXiv cs.SY 2012
Year: 2012

A novel fractional order (FO) fuzzy Proportional-Integral-Derivative (PID) controller has been proposed in this paper which works on the closed loop error and its fractional derivative as the input and has a fractional integrator in its output. The fractional order differ-integrations in the proposed fuzzy logic controller (FLC) are kept as design variables along with the input-output scaling factors (SF) and are optimized with Genetic Algorithm (GA) while minimizing several integral error indices along with the control signal as the objective function. Simulations studies are carried out to control a delayed nonlinear process and an open loop unstable process with time delay. The closed loop performances and controller efforts in each case are compared with conventional PID, fuzzy PID and PIλDμ controller subjected to different integral performance indices. Simulation results show that the proposed fractional order fuzzy PID controller outperforms the others in most cases.
Estimation, Analysis and Smoothing of Self-Similar Network Induced Delays in Feedback Control of Nuclear Reactors
Venue: arXiv cs.SY 2012
Year: 2012

This paper analyzes a nuclear reactor power signal that suffers from network induced random delays in the shared data network while being fed-back to the Reactor Regulating System (RRS). A detailed study is carried out to investigate the self similarity of random delay dynamics due to the network traffic in shared medium. The fractionality or selfsimilarity in the network induced delay that corrupts the measured power signal coming from Self Powered Neutron Detectors (SPND) is estimated and analyzed. As any fractional order randomness is intrinsically different from conventional Gaussian kind of randomness, these delay dynamics need to be handled efficiently, before reaching the controller within the RRS. An attempt has been made to minimize the effect of the randomness in the reactor power transient data with few classes of smoothing filters. The performance measure of the smoothers with fractional order noise consideration is also investigated into.
Adaptive Gain and Order Scheduling of Optimal Fractional Order PIλDμ Controllers with Radial Basis Function Neural-Network
Venue: arXiv cs.SY 2012
Year: 2012

Gain and order scheduling of fractional order (FO) PIλDμ controllers are studied in this paper considering four different classes of higher order processes. The mapping between the optimum PID/FOPID controller parameters and the reduced order process models are done using Radial Basis Function (RBF) type Artificial Neural Network (ANN). Simulation studies have been done to show the effectiveness of the RBFNN for online scheduling of such controllers with random change in set-point and process parameters.
Computing L1 Shortest Paths among Polygonal Obstacles in the Plane
Venue: arXiv cs.CG 2012
Year: 2012

Given a point $s$ and a set of $h$ pairwise disjoint polygonal obstacles of totally $n$ vertices in the plane, we present a new algorithm for building an $L_1$ shortest path map of size O(n) in $O(T)$ time and O(n) space such that for any query point $t$, the length of the $L_1$ shortest obstacle-avoiding path from $s$ to $t$ can be reported in $O(\log n)$ time and the actual shortest path can be found in additional time proportional to the number of edges of the path, where $T$ is the time for triangulating the free space. It is currently known that $T=O(n+h\log^{1+ε}h)$ for an arbitrarily small constant $ε>0$. If the triangulation can be done optimally (i.e., $T=O(n+h\log h)$), then our algorithm is optimal. Previously, the best algorithm computes such an $L_1$ shortest path map in $O(n\log n)$ time and O(n) space. Our techniques can be extended to obtain improved results for other related problems, e.g., computing the $L_1$ geodesic Voronoi diagram for a set of point sites in a polygonal domain, finding shortest paths with fixed orientations, finding approximate Euclidean shortest paths, etc.
Intelligent Car System
Venue: arXiv cs.RO 2012
Year: 2012

In modern life the road safety has becomes the core issue. One single move of a driver can cause horrifying accident. The main goal of intelligent car system is to make communication with other cars on the road. The system is able to control to speed, direction and the distance between the cars the intelligent car system is able to recognize traffic light and is able to take decision according to it. This paper presents a framework of the intelligent car system. I validate several aspect of our system using simulation.
Computer applications in clinical psychology
Venue: arXiv cs.OH 2012
Year: 2012

The computer-assisted analysis is not currently a novelty, but a necessity in all areas of psychology. A number of studies that examine the limits of the computer assisted and analyzed interpretations, also its advantages. A series of studies aim to assess how the computer assisting programs are able to establish a diagnosis referring to the presence of certain mental disorders. We will present the results of one computer application in clinical psychology regarding the assessment of Theory of Mind capacity by animation.
Normal Form Bisimulations for Delimited-Control Operators
Venue: arXiv cs.PL 2012
Year: 2012

We define a notion of normal form bisimilarity for the untyped call-by-value lambda calculus extended with the delimited-control operators shift and reset. Normal form bisimilarities are simple, easy-to-use behavioral equivalences which relate terms without having to test them within all contexts (like contextual equivalence), or by applying them to function arguments (like applicative bisimilarity). We prove that the normal form bisimilarity for shift and reset is sound but not complete w.r.t. contextual equivalence and we define up-to techniques that aim at simplifying bisimulation proofs. Finally, we illustrate the simplicity of the techniques we develop by proving several equivalences on terms.
Exact Gap Computation for Code Coverage Metrics in ISO-C
Venue: arXiv cs.SE 2012
Year: 2012

Test generation and test data selection are difficult tasks for model based testing. Tests for a program can be meld to a test suite. A lot of research is done to quantify the quality and improve a test suite. Code coverage metrics estimate the quality of a test suite. This quality is fine, if the code coverage value is high or 100%. Unfortunately it might be impossible to achieve 100% code coverage because of dead code for example. There is a gap between the feasible and theoretical maximal possible code coverage value. Our review of the research indicates, none of current research is concerned with exact gap computation. This paper presents a framework to compute such gaps exactly in an ISO-C compatible semantic and similar languages. We describe an efficient approximation of the gap in all the other cases. Thus, a tester can decide if more tests might be able or necessary to achieve better coverage.
Rule-based Test Generation with Mind Maps
Venue: arXiv cs.SE 2012
Year: 2012

This paper introduces basic concepts of rule based test generation with mind maps, and reports experiences learned from industrial application of this technique in the domain of smart card testing by Giesecke & Devrient GmbH over the last years. It describes the formalization of test selection criteria used by our test generator, our test generation architecture and test generation framework.
D-iteration: evaluation of the update algorithm
Venue: arXiv cs.DM 2012
Year: 2012

The aim of this paper is to analyse the gain of the update algorithm associated to the recently proposed D-iteration: the D-iteration is a fluid diffusion based new iterative method. It exploits a simple intuitive decomposition of the product matrix-vector as elementary operations of fluid diffusion (forward scheme) associated to a new algebraic representation. We show through experimentations on real datasets how much this approach can improve the computation efficiency in presence of the graph evolution.
Optimized on-line computation of PageRank algorithm
Venue: arXiv cs.DM 2012
Year: 2012

In this paper we present new ideas to accelerate the computation of the eigenvector of the transition matrix associated to the PageRank algorithm. New ideas are based on the decomposition of the matrix-vector product that can be seen as a fluid diffusion model, associated to new algebraic equations. We show through experiments on synthetic data and on real data-sets how much this approach can improve the computation efficiency.
E-learning and use of computer in forensic field
Venue: arXiv cs.CY 2012
Year: 2012

In the Romanian penitentiary establishments and those of other European countries one talks about the formal and informal education. Since the correspondence education system, important steps have been made towards the e-learning didactics which are reflected by the modern teaching methods (through ICT) used even by the penitentiary system. The Moodle platform, the web site with certain specific, and the forum represent the means used as an interface between the educator and the student, their benefits being clearly demonstrated.
Diagonalization Matrix Method of Solving the First Problem of Hidden Markov Model in Speech Recognition System
Venue: arXiv cs.DS 2012
Year: 2012

This paper proposes a computationally efficient method of solving evaluation problem of Hidden Markov Model (HMM) with a given set of discrete observation symbols, number of states and probability distribution matrices. The observation probability for a given HMM model is evaluated using an approach in which the probability evaluation is reduced to the problem of evaluating the product of matrices with different powers and formed out of state transition probabilities and observation probabilities. Finding powers of a matrix is done by using the computationally efficient diagonalization method thereby reducing the overall computational effort for evaluating the Evaluation problem of HMM.The proposed method is compared with the existing direct method. It is found that evaluating matrix power by diagnolisation method is more suitable than that of the direct, method.
Theorem proving for prenex Gödel logic with Delta: checking validity and unsatisfiability
Venue: arXiv cs.LO 2012
Year: 2012

Gödel logic with the projection operator Delta (G_Delta) is an important many-valued as well as intermediate logic. In contrast to classical logic, the validity and the satisfiability problems of G_Delta are not directly dual to each other. We nevertheless provide a uniform, computational treatment of both problems for prenex formulas by describing appropriate translations into sets of order clauses that can be subjected to chaining resolution. For validity a version of Herbrand's Theorem allows us to show the soundness of standard Skolemization. For satisfiability the translation involves a novel, extended Skolemization method.
Signal Shaping for BICM at Low SNR
Venue: arXiv cs.IT 2012
Year: 2012

The mutual information of bit-interleaved coded modulation (BICM) systems, sometimes called the BICM capacity, is investigated at low signal-to-noise ratio (SNR), i.e., in the wideband regime. A new linear transform that depends on bits' probabilities is introduced. This transform is used to prove the asymptotical equivalence between certain BICM systems with uniform and nonuniform input distributions. Using known results for BICM systems with a uniform input distribution, we completely characterize the combinations of input alphabet, input distribution, and binary labeling that achieve the Shannon limit -1.59 dB. The main conclusion is that a BICM system achieves the Shannon limit at low SNR if and only if it can be represented as a zero-mean linear projection of a hypercube, which is the same condition as for uniform input distributions. Hence, probabilistic shaping offers no extra degrees of freedom to optimize the low-SNR mutual information of BICM systems, in addition to what is provided by geometrical shaping. These analytical conclusions are confirmed by numerical results, which also show that for a fixed input alphabet, probabilistic shaping of BICM can improve the mutual information in the low and medium SNR range over any coded modulation system with a uniform input distribution.