OpenRaiser/Intern-Atlas huggingface dataset:
Connecting Gröbner Bases Programs with Coq to do Proofs in Algebra, Geometry and Arithmetics
Venue: arXiv cs.SC 2010
Year: 2010

We describe how we connected three programs that compute Groebner bases to Coq, to do automated proofs on algebraic, geometrical and arithmetical expressions. The result is a set of Coq tactics and a certificate mechanism (downloadable at http://www-sop.inria.fr/marelle/Loic.Pottier/gb-keappa.tgz). The programs are: F4, GB \, and gbcoq. F4 and GB are the fastest (up to our knowledge) available programs that compute Groebner bases. Gbcoq is slow in general but is proved to be correct (in Coq), and we adapted it to our specific problem to be efficient. The automated proofs concern equalities and non-equalities on polynomials with coefficients and indeterminates in R or Z, and are done by reducing to Groebner computation, via Hilbert's Nullstellensatz. We adapted also the results of Harrison, to allow to prove some theorems about modular arithmetics. The connection between Coq and the programs that compute Groebner bases is done using the "external" tactic of Coq that allows to call arbitrary programs accepting xml inputs and outputs. We also produce certificates in order to make the proof scripts independant from the external programs.
A Performance Evaluation of Mobile Web Services Security
Venue: arXiv cs.NI 2010
Year: 2010

It is now feasible to host basic web services on a smart phone due to the advances in wireless devices and mobile communication technologies. The market capture of mobile web services also has increased significantly, in the past years. While the applications are quite welcoming, the ability to provide secure and reliable communication in the vulnerable and volatile mobile ad-hoc topologies is vastly becoming necessary. Even though a lot of standardized security specifications like WS-Security, SAML exist for web services in the wired networks, not much has been analyzed and standardized in the wireless environments. In this paper we give our analysis of adapting some of the security standards, especially WS-Security to the cellular domain, with performance statistics. The performance latencies are obtained and analyzed while observing the performance and quality of service of our Mobile Host.
Logic Programming for Finding Models in the Logics of Knowledge and its Applications: A Case Study
Venue: arXiv cs.AI 2010
Year: 2010

The logics of knowledge are modal logics that have been shown to be effective in representing and reasoning about knowledge in multi-agent domains. Relatively few computational frameworks for dealing with computation of models and useful transformations in logics of knowledge (e.g., to support multi-agent planning with knowledge actions and degrees of visibility) have been proposed. This paper explores the use of logic programming (LP) to encode interesting forms of logics of knowledge and compute Kripke models. The LP modeling is expanded with useful operators on Kripke structures, to support multi-agent planning in the presence of both world-altering and knowledge actions. This results in the first ever implementation of a planner for this type of complex multi-agent domains.
FO(FD): Extending classical logic with rule-based fixpoint definitions
Venue: arXiv cs.LO 2010
Year: 2010

We introduce fixpoint definitions, a rule-based reformulation of fixpoint constructs. The logic FO(FD), an extension of classical logic with fixpoint definitions, is defined. We illustrate the relation between FO(FD) and FO(ID), which is developed as an integration of two knowledge representation paradigms. The satisfiability problem for FO(FD) is investigated by first reducing FO(FD) to difference logic and then using solvers for difference logic. These reductions are evaluated in the computation of models for FO(FD) theories representing fairness conditions and we provide potential applications of FO(FD).
The State-Dependent Multiple-Access Channel with States Available at a Cribbing Encoder
Venue: arXiv cs.IT 2010
Year: 2010

The two-user discrete memoryless state-dependent multiple-access channel (MAC) models a scenario in which two encoders transmit independent messages to a single receiver via a MAC whose channel law is governed by the pair of encoders' inputs and by an i.i.d. state random variable. In the cooperative state-dependent MAC model it is further assumed that Message 1 is shared by both encoders whereas Message 2 is known only to Encoder 2 - the cognitive transmitter. The capacity of the cooperative state-dependent MAC where the realization of the state sequence is known non-causally to the cognitive encoder has been derived by Somekh-Baruch et. al. In this work we dispense of the assumption that Message 1 is shared a-priori by both encoders. Instead, we study the case in which Encoder 2 cribs causally from Encoder 1. We determine the capacity region for both, the case where Encoder 2 cribs strictly causal and the case where Encoder 2 cribs causally from Encoder 1.
Ear Identification by Fusion of Segmented Slice Regions using Invariant Features: An Experimental Manifold with Dual Fusion Approach
Venue: arXiv cs.CV 2010
Year: 2010

This paper proposes a robust ear identification system which is developed by fusing SIFT features of color segmented slice regions of an ear. The proposed ear identification method makes use of Gaussian mixture model (GMM) to build ear model with mixture of Gaussian using vector quantization algorithm and K-L divergence is applied to the GMM framework for recording the color similarity in the specified ranges by comparing color similarity between a pair of reference ear and probe ear. SIFT features are then detected and extracted from each color slice region as a part of invariant feature extraction. The extracted keypoints are then fused separately by the two fusion approaches, namely concatenation and the Dempster-Shafer theory. Finally, the fusion approaches generate two independent augmented feature vectors which are used for identification of individuals separately. The proposed identification technique is tested on IIT Kanpur ear database of 400 individuals and is found to achieve 98.25% accuracy for identification while top 5 matched criteria is set for each subject.
Swapping Evaluation: A Memory-Scalable Solution for Answer-On-Demand Tabling
Venue: arXiv cs.PL 2010
Year: 2010

One of the differences among the various approaches to suspension-based tabled evaluation is the scheduling strategy. The two most popular strategies are local and batched evaluation. The former collects all the solutions to a tabled predicate before making any one of them available outside the tabled computation. The latter returns answers one by one before computing them all, which in principle is better if only one answer (or a subset of the answers) is desired. Batched evaluation is closer to SLD evaluation in that it computes solutions lazily as they are demanded, but it may need arbitrarily more memory than local evaluation, which is able to reclaim memory sooner. Some programs which in practice can be executed under the local strategy quickly run out of memory under batched evaluation. This has led to the general adoption of local evaluation at the expense of the more depth-first batched strategy. In this paper we study the reasons for the high memory consumption of batched evaluation and propose a new scheduling strategy which we have termed swapping evaluation. Swapping evaluation also returns answers one by one before completing a tabled call, but its memory usage can be orders of magnitude less than batched evaluation. An experimental implementation in the XSB system shows that swapping evaluation is a feasible memory-scalable strategy that need not compromise execution speed.
On the (non-)existence of polynomial kernels for Pl-free edge modification problems
Venue: arXiv cs.DS 2010
Year: 2010

Given a graph G = (V,E) and an integer k, an edge modification problem for a graph property P consists in deciding whether there exists a set of edges F of size at most k such that the graph H = (V,E \vartriangle F) satisfies the property P. In the P edge-completion problem, the set F of edges is constrained to be disjoint from E; in the P edge-deletion problem, F is a subset of E; no constraint is imposed on F in the P edge-edition problem. A number of optimization problems can be expressed in terms of graph modification problems which have been extensively studied in the context of parameterized complexity. When parameterized by the size k of the edge set F, it has been proved that if P is an hereditary property characterized by a finite set of forbidden induced subgraphs, then the three P edge-modification problems are FPT. It was then natural to ask whether these problems also admit a polynomial size kernel. Using recent lower bound techniques, Kratsch and Wahlstrom answered this question negatively. However, the problem remains open on many natural graph classes characterized by forbidden induced subgraphs. Kratsch and Wahlstrom asked whether the result holds when the forbidden subgraphs are paths or cycles and pointed out that the problem is already open in the case of P4-free graphs (i.e. cographs). This paper provides positive and negative results in that line of research. We prove that parameterized cograph edge modification problems have cubic vertex kernels whereas polynomial kernels are unlikely to exist for the Pl-free and Cl-free edge-deletion problems for large enough l.
A Tutorial on the Implementation of Ad-hoc On Demand Distance Vector (AODV) Protocol in Network Simulator (NS-2)
Venue: arXiv cs.NI 2010
Year: 2010

The Network Simulator (NS-2) is a most widely used network simulator. It has the capabilities to simulate a range of networks including wired and wireless networks. In this tutorial, we present the implementation of Ad Hoc On-Demand Distance Vector (AODV) Protocol in NS-2. This tutorial is targeted to the novice user who wants to understand the implementation of AODV Protocol in NS-2.
Sorting of Permutations by Cost-Constrained Transpositions
Venue: arXiv cs.IT 2010
Year: 2010

We address the problem of finding the minimum decomposition of a permutation in terms of transpositions with non-uniform cost. For arbitrary non-negative cost functions, we describe polynomial-time, constant-approximation decomposition algorithms. For metric-path costs, we describe exact polynomial-time decomposition algorithms. Our algorithms represent a combination of Viterbi-type algorithms and graph-search techniques for minimizing the cost of individual transpositions, and dynamic programing algorithms for finding minimum cost cycle decompositions. The presented algorithms have applications in information theory, bioinformatics, and algebra.
Abstracting Abstract Machines
Venue: arXiv cs.PL 2010
Year: 2010

We describe a derivational approach to abstract interpretation that yields novel and transparently sound static analyses when applied to well-established abstract machines. To demonstrate the technique and support our claim, we transform the CEK machine of Felleisen and Friedman, a lazy variant of Krivine's machine, and the stack-inspecting CM machine of Clements and Felleisen into abstract interpretations of themselves. The resulting analyses bound temporal ordering of program events; predict return-flow and stack-inspection behavior; and approximate the flow and evaluation of by-need parameters. For all of these machines, we find that a series of well-known concrete machine refactorings, plus a technique we call store-allocated continuations, leads to machines that abstract into static analyses simply by bounding their stores. We demonstrate that the technique scales up uniformly to allow static analysis of realistic language features, including tail calls, conditionals, side effects, exceptions, first-class continuations, and even garbage collection.
Competitive Analysis of Minimum-Cut Maximum Flow Algorithms in Vision Problems
Venue: arXiv cs.CV 2010
Year: 2010

Rapid advances in image acquisition and storage technology underline the need for algorithms that are capable of solving large scale image processing and computer-vision problems. The minimum cut problem plays an important role in processing many of these imaging problems such as, image and video segmentation, stereo vision, multi-view reconstruction and surface fitting. While several min-cut/max-flow algorithms can be found in the literature, their performance in practice has been studied primarily outside the scope of computer vision. We present here the results of a comprehensive computational study, in terms of execution times and memory utilization, of four recently published algorithms, which optimally solve the {\em s-t} cut and maximum flow problems: (i) Goldberg's and Tarjan's {\em Push-Relabel}; (ii) Hochbaum's {\em pseudoflow}; (iii) Boykov's and Kolmogorov's {\em augmenting paths}; and (iv) Goldberg's {\em partial augment-relabel}. Our results demonstrate that the {\em Hochbaum's pseudoflow} algorithm, is faster and utilizes less memory than the other algorithms on all problem instances investigated.
Broadcast Approach and Oblivious Cooperative Strategies for the Wireless Relay Channel - Part II: Block-Markov Decode-and-Forward (BMDF)
Venue: arXiv cs.IT 2010
Year: 2010

This is the second in a two part series of papers on incorporation of the broadcast approach into oblivious protocols for the relay channel where the source and the relay are collocated. Part I described the broadcast approach and its benefits in terms of achievable rates when used with the sequential decode- and-forward (SDF) scheme. Part II investigates yet another oblivious scheme, the Block-Markov decode- and-forward (BMDF) under the single and two-layered transmissions. For the single layer, previously reported results are enhanced and a conjecture regarding the optimal correlation coefficient between the source and the relay's transmission is established. For the discrete multi-layer transmission of two or more layers, it is shown that perfect cooperation (2x1 MISO) rates are attained even with low collocation gains at the expense of a longer delay, improving upon those achievable by the SDF.
About functions where function input describes inner working of the function
Venue: arXiv cs.CC 2010
Year: 2010

This paper argues an existence of a class of functions where function own input makes function description. That fact have impact to the wide spectrum of phenomena such as negative findings of Random Oracle Model in cryptography, complexity in some rules of cellular automata (Wolfram rule 30) and determinism in the true randomness to name just a few.
Detecting influenza outbreaks by analyzing Twitter messages
Venue: arXiv cs.IR 2010
Year: 2010

We analyze over 500 million Twitter messages from an eight month period and find that tracking a small number of flu-related keywords allows us to forecast future influenza rates with high accuracy, obtaining a 95% correlation with national health statistics. We then analyze the robustness of this approach to spurious keyword matches, and we propose a document classification component to filter these misleading messages. We find that this document classifier can reduce error rates by over half in simulated false alarm experiments, though more research is needed to develop methods that are robust in cases of extremely high noise.
How fractional counting affects the Impact Factor: Normalization in terms of differences in citation potentials among fields of science
Venue: arXiv cs.DL 2010
Year: 2010

The ISI-Impact Factors suffer from a number of drawbacks, among them the statistics-why should one use the mean and not the median?-and the incomparability among fields of science because of systematic differences in citation behavior among fields. Can these drawbacks be counteracted by counting citation weights fractionally instead of using whole numbers in the numerators? (i) Fractional citation counts are normalized in terms of the citing sources and thus would take into account differences in citation behavior among fields of science. (ii) Differences in the resulting distributions can be tested statistically for their significance at different levels of aggregation. (iii) Fractional counting can be generalized to any document set including journals or groups of journals, and thus the significance of differences among both small and large sets can be tested. A list of fractionally counted Impact Factors for 2008 is available online at http://www.leydesdorff.net/weighted_if/weighted_if.xls. The in-between group variance among the thirteen fields of science identified in the U.S. Science and Engineering Indicators is not statistically significant after this normalization. Although citation behavior differs largely between disciplines, the reflection of these differences in fractionally counted citation distributions could not be used as a reliable instrument for the classification.
A Program-Level Approach to Revising Logic Programs under the Answer Set Semantics
Venue: arXiv cs.AI 2010
Year: 2010

An approach to the revision of logic programs under the answer set semantics is presented. For programs P and Q, the goal is to determine the answer sets that correspond to the revision of P by Q, denoted P * Q. A fundamental principle of classical (AGM) revision, and the one that guides the approach here, is the success postulate. In AGM revision, this stipulates that A is in K * A. By analogy with the success postulate, for programs P and Q, this means that the answer sets of Q will in some sense be contained in those of P * Q. The essential idea is that for P * Q, a three-valued answer set for Q, consisting of positive and negative literals, is first determined. The positive literals constitute a regular answer set, while the negated literals make up a minimal set of naf literals required to produce the answer set from Q. These literals are propagated to the program P, along with those rules of Q that are not decided by these literals. The approach differs from work in update logic programs in two main respects. First, we ensure that the revising logic program has higher priority, and so we satisfy the success postulate; second, for the preference implicit in a revision P * Q, the program Q as a whole takes precedence over P, unlike update logic programs, since answer sets of Q are propagated to P. We show that a core group of the AGM postulates are satisfied, as are the postulates that have been proposed for update logic programs.
Implementing Distributed Controllers for Systems with Priorities
Venue: arXiv cs.DC 2010
Year: 2010

Implementing a component-based system in a distributed way so that it ensures some global constraints is a challenging problem. We consider here abstract specifications consisting of a composition of components and a controller given in the form of a set of interactions and a priority order amongst them. In the context of distributed systems, such a controller must be executed in a distributed fashion while still respecting the global constraints imposed by interactions and priorities. We present in this paper an implementation of an algorithm that allows a distributed execution of systems with (binary) interactions and priorities. We also present a comprehensive simulation analysis that shows how sensitive to changes our algorithm is, in particular changes related to the degree of conflict in the system.
Stable marriage problems with quantitative preferences
Venue: arXiv cs.AI 2010
Year: 2010

The stable marriage problem is a well-known problem of matching men to women so that no man and woman, who are not married to each other, both prefer each other. Such a problem has a wide variety of practical applications, ranging from matching resident doctors to hospitals, to matching students to schools or more generally to any two-sided market. In the classical stable marriage problem, both men and women express a strict preference order over the members of the other sex, in a qualitative way. Here we consider stable marriage problems with quantitative preferences: each man (resp., woman) provides a score for each woman (resp., man). Such problems are more expressive than the classical stable marriage problems. Moreover, in some real-life situations it is more natural to express scores (to model, for example, profits or costs) rather than a qualitative preference ordering. In this context, we define new notions of stability and optimality, and we provide algorithms to find marriages which are stable and/or optimal according to these notions. While expressivity greatly increases by adopting quantitative preferences, we show that in most cases the desired solutions can be found by adapting existing algorithms for the classical stable marriage problem.
Examining Requirements Change Rework Effort: A Study
Venue: arXiv cs.SE 2010
Year: 2010

Although software managers are generally good at new project estimation, their experience of scheduling rework tends to be poor. Inconsistent or incorrect effort estimation can increase the risk that the completion time for a project will be problematic. To continually alter software maintenance schedules during software maintenance is a daunting task. Our proposed framework, validated in a case study confirms that the variables resulting from requirements changes suffer from a number of problems, e.g., the coding used, end user involvement and user documentation. Our results clearly show a significant impact on rework effort as a result of unexpected errors that correlate with 1) weak characteristics and attributes as described in the program's source lines of code, especially in data declarations and data statements, 2) lack of communication between developers and users on a change effects, and 3) unavailability of user documentation. To keep rework effort under control, new criteria in change request forms are proposed. These criteria are shown in a proposed framework; the more case studies that are validated, the more reliable the result will be in determining the outcome of effort rework estimation.
An Efficient Automatic Mass Classification Method In Digitized Mammograms Using Artificial Neural Network
Venue: arXiv cs.CV 2010
Year: 2010

In this paper we present an efficient computer aided mass classification method in digitized mammograms using Artificial Neural Network (ANN), which performs benign-malignant classification on region of interest (ROI) that contains mass. One of the major mammographic characteristics for mass classification is texture. ANN exploits this important factor to classify the mass into benign or malignant. The statistical textural features used in characterizing the masses are mean, standard deviation, entropy, skewness, kurtosis and uniformity. The main aim of the method is to increase the effectiveness and efficiency of the classification process in an objective manner to reduce the numbers of false-positive of malignancies. Three layers artificial neural network (ANN) with seven features was proposed for classifying the marked regions into benign and malignant and 90.91% sensitivity and 83.87% specificity is achieved that is very much promising compare to the radiologist's sensitivity 75%.