OpenRaiser/Intern-Atlas huggingface dataset:
Analytic Tableaux for Simple Type Theory and its First-Order Fragment
Venue: arXiv cs.LO 2010
Year: 2010

We study simple type theory with primitive equality (STT) and its first-order fragment EFO, which restricts equality and quantification to base types but retains lambda abstraction and higher-order variables. As deductive system we employ a cut-free tableau calculus. We consider completeness, compactness, and existence of countable models. We prove these properties for STT with respect to Henkin models and for EFO with respect to standard models. We also show that the tableau system yields a decision procedure for three EFO fragments.
Equilibrium Point in Quantum Physics and its Inspiration to Game Theory
Venue: arXiv cs.GT 2010
Year: 2010

Most of atoms and molecule found in nature are capable of evolving towards and staying at their ground states, the lowest energy states. This paper offers a global optimization approach to understand the ground state as the equilibrium point of an $n$-player game under cooperation. With the same approach, Nash equilibrium can be viewed as the equilibrium point under competition. The former can offer higher payoffs and stability of game playing than the later. It is truly an inspiration from nature for us to build societies for quality and stability under cooperation rather than competition.
XOR at a Single Vertex -- Artificial Dendrites
Venue: arXiv cs.NE 2010
Year: 2010

New to neuroscience with implications for AI, the exclusive OR, or any other Boolean gate may be biologically accomplished within a single region where active dendrites merge. This is demonstrated below using dynamic circuit analysis. Medical knowledge aside, this observation points to the possibility of specially coated conductors to accomplish artificial dendrites.
An Optimal Coding Strategy for the Binary Multi-Way Relay Channel
Venue: arXiv cs.IT 2010
Year: 2010

We derive the capacity of the binary multi-way relay channel, in which multiple users exchange messages at a common rate through a relay. The capacity is achieved using a novel functional-decode-forward coding strategy. In the functional-decode-forward coding strategy, the relay decodes functions of the users' messages without needing to decode individual messages. The functions to be decoded by the relay are defined such that when the relay broadcasts the functions back to the users, every user is able to decode the messages of all other users.
Dynamical Jumping Real-Time Fault-Tolerant Routing Protocol for Wireless Sensor Networks
Venue: arXiv cs.NI 2010
Year: 2010

In time-critical wireless sensor network (WSN) applications, a high degree of reliability is commonly required. A dynamical jumping real-time fault-tolerant routing protocol (DMRF) is proposed in this paper. Each node utilizes the remaining transmission time of the data packets and the state of the forwarding candidate node set to dynamically choose the next hop. Once node failure, network congestion or void region occurs, the transmission mode will switch to jumping transmission mode, which can reduce the transmission time delay, guaranteeing the data packets to be sent to the destination node within the specified time limit. By using feedback mechanism, each node dynamically adjusts the jumping probabilities to increase the ratio of successful transmission. Simulation results show that DMRF can not only efficiently reduce the effects of failure nodes, congestion and void region, but also yield higher ratio of successful transmission, smaller transmission delay and reduced number of control packets.
Achievable Rate Regions for Dirty Tape Channels and "Joint Writing on Dirty Paper and Dirty Tape"
Venue: arXiv cs.IT 2010
Year: 2010

We consider the Gaussian Dirty Tape Channel (DTC) Y=X+S+Z, where S is an additive Gaussian interference known causally to the transmitter. The general expression [max]\_top(P_U,f(.),X=f(U,S))I(U;Y) is presented for the capacity of this channel. For linear assignment to f(.), i.e. X=U-βS, this expression leads to the compensation strategy proposed previously by Willems to obtain an achievable rate for the DTC. We show that linear assignment to f(.) is optimal, under the condition that there exists a real number β^* such that the pair (X+β^* S,U) is independent of interference S. Furthermore, by applying a time-sharing technique to the achievable rate derived by linear assignment to f(.), an improved lower bound on the capacity of DTC is obtained. We also consider the Gaussian multiple access channel with additive interference, and study two different scenarios for this system. In the first case, both transmitters know interference causally while in the second, one transmitter has access to the interference noncausally and the other causally. Achievable rate regions for these two scenarios are then established.
A Geometric Approach to the Problem of Unique Decomposition of Processes
Venue: arXiv cs.LO 2010
Year: 2010

This paper proposes a geometric solution to the problem of prime decomposability of concurrent processes first explored by R. Milner and F. Moller in [MM93]. Concurrent programs are given a geometric semantics using cubical areas, for which a unique factorization theorem is proved. An effective factorization method which is correct and complete with respect to the geometric semantics is derived from the factorization theorem. This algorithm is implemented in the static analyzer ALCOOL.
Clustering with diversity
Venue: arXiv cs.DS 2010
Year: 2010

We consider the {\em clustering with diversity} problem: given a set of colored points in a metric space, partition them into clusters such that each cluster has at least $\ell$ points, all of which have distinct colors. We give a 2-approximation to this problem for any $\ell$ when the objective is to minimize the maximum radius of any cluster. We show that the approximation ratio is optimal unless $\mathbf{P=NP}$, by providing a matching lower bound. Several extensions to our algorithm have also been developed for handling outliers. This problem is mainly motivated by applications in privacy-preserving data publication.
Enumeration of the Monomials of a Polynomial and Related Complexity Classes
Venue: arXiv cs.CC 2010
Year: 2010

We study the problem of generating monomials of a polynomial in the context of enumeration complexity. In this setting, the complexity measure is the delay between two solutions and the total time. We present two new algorithms for restricted classes of polynomials, which have a good delay and the same global running time as the classical ones. Moreover they are simple to describe, use little evaluation points and one of them is parallelizable. We introduce three new complexity classes, TotalPP, IncPP and DelayPP, which are probabilistic counterparts of the most common classes for enumeration problems, hoping that randomization will be a tool as strong for enumeration as it is for decision. Our interpolation algorithms proves that a lot of interesting problems are in these classes like the enumeration of the spanning hypertrees of a 3-uniform hypergraph. Finally we give a method to interpolate a degree 2 polynomials with an acceptable (incremental) delay. We also prove that finding a specified monomial in a degree 2 polynomial is hard unless RP = NP. It suggests that there is no algorithm with a delay as good (polynomial) as the one we achieve for multilinear polynomials.
Uses of randomness in computation
Venue: arXiv cs.DS 2010
Year: 2010

Random number generators are widely used in practical algorithms. Examples include simulation, number theory (primality testing and integer factorization), fault tolerance, routing, cryptography, optimization by simulated annealing, and perfect hashing. Complexity theory usually considers the worst-case behaviour of deterministic algorithms, but it can also consider average-case behaviour if it is assumed that the input data is drawn randomly from a given distribution. Rabin popularised the idea of "probabilistic" algorithms, where randomness is incorporated into the algorithm instead of being assumed in the input data. Yao showed that there is a close connection between the complexity of probabilistic algorithms and the average-case complexity of deterministic algorithms. We give examples of the uses of randomness in computation, discuss the contributions of Rabin, Yao and others, and mention some open questions. This is the text of an invited talk presented at "Theory Day", University of NSW, Sydney, 22 April 1994.
A fast vectorised implementation of Wallace's normal random number generator
Venue: arXiv cs.DS 2010
Year: 2010

Wallace has proposed a new class of pseudo-random generators for normal variates. These generators do not require a stream of uniform pseudo-random numbers, except for initialisation. The inner loops are essentially matrix-vector multiplications and are very suitable for implementation on vector processors or vector/parallel processors such as the Fujitsu VPP300. In this report we outline Wallace's idea, consider some variations on it, and describe a vectorised implementation RANN4 which is more than three times faster than its best competitors (the Polar and Box-Muller methods) on the Fujitsu VP2200 and VPP300.
The Complexity of Finding Reset Words in Finite Automata
Venue: arXiv cs.FL 2010
Year: 2010

We study several problems related to finding reset words in deterministic finite automata. In particular, we establish that the problem of deciding whether a shortest reset word has length k is complete for the complexity class DP. This result answers a question posed by Volkov. For the search problems of finding a shortest reset word and the length of a shortest reset word, we establish membership in the complexity classes FP^NP and FP^NP[log], respectively. Moreover, we show that both these problems are hard for FP^NP[log]. Finally, we observe that computing a reset word of a given length is FNP-complete.
Offline Handwriting Recognition using Genetic Algorithm
Venue: arXiv cs.CV 2010
Year: 2010

Handwriting Recognition enables a person to scribble something on a piece of paper and then convert it into text. If we look into the practical reality there are enumerable styles in which a character may be written. These styles can be self combined to generate more styles. Even if a small child knows the basic styles a character can be written, he would be able to recognize characters written in styles intermediate between them or formed by their mixture. This motivates the use of Genetic Algorithms for the problem. In order to prove this, we made a pool of images of characters. We converted them to graphs. The graph of every character was intermixed to generate styles intermediate between the styles of parent character. Character recognition involved the matching of the graph generated from the unknown character image with the graphs generated by mixing. Using this method we received an accuracy of 98.44%.
Modelling of Human Glottis in VLSI for Low Power Architectures
Venue: arXiv cs.OH 2010
Year: 2010

The Glottal Source is an important component of voice as it can be considered as the excitation signal to the voice apparatus. Nowadays, new techniques of speech processing such as speech recognition and speech synthesis use the glottal closure and opening instants. Current models of the glottal waves derive their shape from approximate information rather than from exactly measured data. General method concentrate on assessment of the glottis opening using optical, acoustical methods, or on visualization of the larynx position using ultrasound, computer tomography or magnetic resonance imaging techniques. In this work, circuit model of Human Glottis using MOS is designed by exploiting fluid volume velocity to current, fluid pressure to voltage, and linear and nonlinear mechanical impedances to linear and nonlinear electrical impedances. The glottis modeled as current source includes linear, non-linear impedances to represent laminar and turbulent flow respectively, in vocal tract. The MOS modelling and simulation results of glottal circuit has been carried out on BSIM 3v3 model in TSMC 0.18 micrometer technology using ELDO simulator.
Sampling and Recovery of Pulse Streams
Venue: arXiv cs.IT 2010
Year: 2010

Compressive Sensing (CS) is a new technique for the efficient acquisition of signals, images, and other data that have a sparse representation in some basis, frame, or dictionary. By sparse we mean that the N-dimensional basis representation has just K<<N significant coefficients; in this case, the CS theory maintains that just M = K log N random linear signal measurements will both preserve all of the signal information and enable robust signal reconstruction in polynomial time. In this paper, we extend the CS theory to pulse stream data, which correspond to S-sparse signals/images that are convolved with an unknown F-sparse pulse shape. Ignoring their convolutional structure, a pulse stream signal is K=SF sparse. Such signals figure prominently in a number of applications, from neuroscience to astronomy. Our specific contributions are threefold. First, we propose a pulse stream signal model and show that it is equivalent to an infinite union of subspaces. Second, we derive a lower bound on the number of measurements M required to preserve the essential information present in pulse streams. The bound is linear in the total number of degrees of freedom S + F, which is significantly smaller than the naive bound based on the total signal sparsity K=SF. Third, we develop an efficient signal recovery algorithm that infers both the shape of the impulse response as well as the locations and amplitudes of the pulses. The algorithm alternatively estimates the pulse locations and the pulse shape in a manner reminiscent of classical deconvolution algorithms. Numerical experiments on synthetic and real data demonstrate the advantages of our approach over standard CS.
A Pedagogical Evaluation and Discussion about the Lack of Cohesion in Method (LCOM) Metric Using Field Experiment
Venue: arXiv cs.SE 2010
Year: 2010

Chidamber and Kemerer first defined a cohesion measure for object-oriented software - the Lack of Cohesion in Methods (LCOM) metric. This paper presents a pedagogic evaluation and discussion about the LCOM metric using field data from three industrial systems. System 1 has 34 classes, System 2 has 383 classes and System 3 has 1055 classes. The main objectives of the study were to determine if the LCOM metric was appropriate in the measurement of class cohesion and the determination of properly and improperly designed classes in the studied systems. Chidamber and Kemerer's suite of metric was used as metric tool. Descriptive statistics was used to analyze results. The result of the study showed that in System 1, 78.8% (26 classes) were cohesive; System 2 54% (207 classes) were cohesive; System 3 30% (317 classes) were cohesive. We suggest that the LCOM metric measures class cohesiveness and was appropriate in the determination of properly and improperly designed classes in the studied system.
Publishing Math Lecture Notes as Linked Data
Venue: arXiv cs.DL 2010
Year: 2010

We mark up a corpus of LaTeX lecture notes semantically and expose them as Linked Data in XHTML+MathML+RDFa. Our application makes the resulting documents interactively browsable for students. Our ontology helps to answer queries from students and lecturers, and paves the path towards an integration of our corpus with external sites.
An Achievability Scheme for the Compound Channel with State Noncausally Available at the Encoder
Venue: arXiv cs.IT 2010
Year: 2010

A new achievability scheme for the compound channel with discrete memoryless (DM) state noncausally available at the encoder is established. Achievability is proved using superposition coding, Marton coding, joint typicality encoding, and indirect decoding. The scheme is shown to achieve strictly higher rate than the straightforward extension of the Gelfand-Pinsker coding scheme for a single DMC with DM state, and is optimal for some classes of channels.
Convergent discrete Laplace-Beltrami operators over surfaces
Venue: arXiv cs.CG 2010
Year: 2010

The convergence problem of the Laplace-Beltrami operators plays an essential role in the convergence analysis of the numerical simulations of some important geometric partial differential equations which involve the operator. In this note we present a new effective and convergent algorithm to compute discrete Laplace-Beltrami operators acting on functions over surfaces. We prove a convergence theorem for our discretization. To our knowledge, this is the first convergent algorithm of discrete Laplace-Beltrami operators over surfaces for functions on general surfaces. Our algorithm is conceptually simple and easy to compute. Indeed, the convergence rate of our new algorithm of discrete Laplace-Beltrami operators over surfaces is $O(r)$ where r represents the size of the mesh of discretization of the surface.
Signature Region of Interest using Auto cropping
Venue: arXiv cs.CV 2010
Year: 2010

A new approach for signature region of interest pre-processing was presented. It used new auto cropping preparation on the basis of the image content, where the intensity value of pixel is the source of cropping. This approach provides both the possibility of improving the performance of security systems based on signature images, and also the ability to use only the region of interest of the used image to suit layout design of biometric systems. Underlying the approach is a novel segmentation method which identifies the exact region of foreground of signature for feature extraction usage. Evaluation results of this approach shows encouraging prospects by eliminating the need for false region isolating, reduces the time cost associated with signature false points detection, and addresses enhancement issues. A further contribution of this paper is an automated cropping stage in bio-secure based systems.
An Economic-based Resource Management and Scheduling for Grid Computing Applications
Venue: arXiv cs.DC 2010
Year: 2010

Resource management and scheduling plays a crucial role in achieving high utilization of resources in grid computing environments. Due to heterogeneity of resources, scheduling an application is significantly complicated and challenging task in grid system. Most of the researches in this area are mainly focused on to improve the performance of the grid system. There were some allocation model has been proposed based on divisible load theory with different type of workloads and a single originating processor. In this paper we introduce a new resource allocation model with multiple load originating processors as an economic model. Solutions for an optimal allocation of fraction of loads to nodes obtained to minimize the cost of the grid users via linear programming approach. It is found that the resource allocation model can efficiently and effectively allocate workloads to proper resources. Experimental results showed that the proposed model obtained the better solution in terms of cost and time.
On Practical Algorithms for Entropy Estimation and the Improved Sample Complexity of Compressed Counting
Venue: arXiv cs.DS 2010
Year: 2010

Estimating the p-th frequency moment of data stream is a very heavily studied problem. The problem is actually trivial when p = 1, assuming the strict Turnstile model. The sample complexity of our proposed algorithm is essentially O(1) near p=1. This is a very large improvement over the previously believed O(1/eps^2) bound. The proposed algorithm makes the long-standing problem of entropy estimation an easy task, as verified by the experiments included in the appendix.
Automated Verification of Practical Garbage Collectors
Venue: arXiv cs.PL 2010
Year: 2010

Garbage collectors are notoriously hard to verify, due to their low-level interaction with the underlying system and the general difficulty in reasoning about reachability in graphs. Several papers have presented verified collectors, but either the proofs were hand-written or the collectors were too simplistic to use on practical applications. In this work, we present two mechanically verified garbage collectors, both practical enough to use for real-world C# benchmarks. The collectors and their associated allocators consist of x86 assembly language instructions and macro instructions, annotated with preconditions, postconditions, invariants, and assertions. We used the Boogie verification generator and the Z3 automated theorem prover to verify this assembly language code mechanically. We provide measurements comparing the performance of the verified collector with that of the standard Bartok collectors on off-the-shelf C# benchmarks, demonstrating their competitiveness.
Resolving the Complexity of Some Data Privacy Problems
Venue: arXiv cs.CC 2010
Year: 2010

We formally study two methods for data sanitation that have been used extensively in the database community: k-anonymity and l-diversity. We settle several open problems concerning the difficulty of applying these methods optimally, proving both positive and negative results: 1. 2-anonymity is in P. 2. The problem of partitioning the edges of a triangle-free graph into 4-stars (degree-three vertices) is NP-hard. This yields an alternative proof that 3-anonymity is NP-hard even when the database attributes are all binary. 3. 3-anonymity with only 27 attributes per record is MAX SNP-hard. 4. For databases with n rows, k-anonymity is in O(4^n poly(n)) time for all k > 1. 5. For databases with n rows and l <= log_{2c+2} log n attributes over an alphabet of cardinality c = O(1), k-anonymity is in P. Assuming c, l = O(1), k-anonymity is in O(n). 6. 3-diversity with binary attributes is NP-hard, with one sensitive attribute. 7. 2-diversity with binary attributes is NP-hard, with three sensitive attributes.
An Oracle Strongly Separating Deterministic Time from Nondeterministic Time, via Kolmogorov Complexity
Venue: arXiv cs.CC 2010
Year: 2010

Hartmanis used Kolmogorov complexity to provide an alternate proof of the classical result of Baker, Gill, and Solovay that there is an oracle relative to which P is not NP. We refine the technique to strengthen the result, constructing an oracle relative to which a conjecture of Lipton is false.
Graph Triangulations and the Compatibility of Unrooted Phylogenetic Trees
Venue: arXiv cs.DM 2010
Year: 2010

We characterize the compatibility of a collection of unrooted phylogenetic trees as a question of determining whether a graph derived from these trees --- the display graph --- has a specific kind of triangulation, which we call legal. Our result is a counterpart to the well known triangulation-based characterization of the compatibility of undirected multi-state characters.