OpenRaiser/Intern-Atlas huggingface dataset:
Interactive Realizability, Monads and Witness Extraction
Venue: arXiv cs.LO 2013
Year: 2013

In this dissertation we collect some results about "interactive realizability", a realizability semantics that extends the Brouwer-Heyting-Kolmogorov interpretation to (sub-)classical logic, more precisely to first-order intuitionistic arithmetic (Heyting Arithmetic, HA) extended by the law of the excluded middle restricted to simply existential formulas formulas (EM1), a system motivated by its interest in proof mining. We describe the interactive interpretation of a classical proof involving real numbers. The statement we prove is a simple but non-trivial fact about points in the real plane. The proof employs EM1 to deduce properties of the ordering on the real numbers, which is undecidable and thus problematic from a constructive point of view. We present a new set of reductions for derivations in natural deduction that can extract witnesses from closed derivations of simply existential formulas in HA + EM1. The reduction we present are inspired by the informal idea of learning by making falsifiable hypothesis and checking them, and by the interactive realizability interpretation. We extract the witnesses directly from derivations in HA + EM1 by reduction, without encoding derivations by a realizability interpretation. We give a new presentation of interactive realizability with a more explicit syntax. We express interactive realizers by means of an abstract framework that applies the monadic approach used in functional programming to modified realizability, in order to obtain less strict notions of realizability that are suitable to classical logic. In particular we use a combination of the state and exception monads in order to capture the learning-from-mistakes nature of interactive realizers.
Simplifying Multiple Sums in Difference Fields
Venue: arXiv cs.SC 2013
Year: 2013

In this survey article we present difference field algorithms for symbolic summation. Special emphasize is put on new aspects in how the summation problems are rephrased in terms of difference fields, how the problems are solved there, and how the derived results in the given difference field can be reinterpreted as solutions of the input problem. The algorithms are illustrated with the Mathematica package \SigmaP\ by discovering and proving new harmonic number identities extending those from (Paule and Schneider, 2003). In addition, the newly developed package \texttt{EvaluateMultiSums} is introduced that combines the presented tools. In this way, large scale summation problems for the evaluation of Feynman diagrams in QCD (Quantum ChromoDynamics) can be solved completely automatically.
Graph Logics with Rational Relations
Venue: arXiv cs.FL 2013
Year: 2013

We investigate some basic questions about the interaction of regular and rational relations on words. The primary motivation comes from the study of logics for querying graph topology, which have recently found numerous applications. Such logics use conditions on paths expressed by regular languages and relations, but they often need to be extended by rational relations such as subword or subsequence. Evaluating formulae in such extended graph logics boils down to checking nonemptiness of the intersection of rational relations with regular or recognizable relations (or, more generally, to the generalized intersection problem, asking whether some projections of a regular relation have a nonempty intersection with a given rational relation). We prove that for several basic and commonly used rational relations, the intersection problem with regular relations is either undecidable (e.g., for subword or suffix, and some generalizations), or decidable with non-primitive-recursive complexity (e.g., for subsequence and its generalizations). These results are used to rule out many classes of graph logics that freely combine regular and rational relations, as well as to provide the simplest problem related to verifying lossy channel systems that has non-primitive-recursive complexity. We then prove a dichotomy result for logics combining regular conditions on individual paths and rational relations on paths, by showing that the syntactic form of formulae classifies them into either efficiently checkable or undecidable cases. We also give examples of rational relations for which such logics are decidable even without syntactic restrictions.
The Webdamlog System Managing Distributed Knowledge on the Web
Venue: arXiv cs.DB 2013
Year: 2013

We study the use of WebdamLog, a declarative high-level lan- guage in the style of datalog, to support the distribution of both data and knowledge (i.e., programs) over a network of au- tonomous peers. The main novelty of WebdamLog compared to datalog is its use of delegation, that is, the ability for a peer to communicate a program to another peer. We present results of a user study, showing that users can write WebdamLog programs quickly and correctly, and with a minimal amount of training. We present an implementation of the WebdamLog inference engine relying on the Bud dat- alog engine. We describe an experimental evaluation of the WebdamLog engine, demonstrating that WebdamLog can be im- plemented efficiently. We conclude with a discussion of ongoing and future work.
Green Power Control in Cognitive Wireless Networks
Venue: arXiv cs.IT 2013
Year: 2013

A decentralized network of cognitive and non-cognitive transmitters where each transmitter aims at maximizing his energy-efficiency is considered. The cognitive transmitters are assumed to be able to sense the transmit power of their non-cognitive counterparts and the former have a cost for sensing. The Stackelberg equilibrium analysis of this $2-$level hierarchical game is conducted, which allows us to better understand the effects of cognition on energy-efficiency. In particular, it is proven that the network energy-efficiency is maximized when only a given fraction of terminals are cognitive. Then, we study a sensing game where all the transmitters are assumed to take the decision whether to sense (namely to be cognitive) or not. This game is shown to be a weighted potential game and its set of equilibria is studied. Playing the sensing game in a first phase (e.g., of a time-slot) and then playing the power control game is shown to be more efficient individually for all transmitters than playing a game where a transmitter would jointly optimize whether to sense and his power level, showing the existence of a kind of Braess paradox. The derived results are illustrated by numerical results and provide some insights on how to deploy cognitive radios in heterogeneous networks in terms of sensing capabilities. Keywords: Power Control, Stackelberg Equilibrium, Energy-Efficiency.
The planar directed k-Vertex-Disjoint Paths problem is fixed-parameter tractable
Venue: arXiv cs.DM 2013
Year: 2013

Given a graph G and k pairs of vertices (s_1,t_1), ..., (s_k,t_k), the k-Vertex-Disjoint Paths problem asks for pairwise vertex-disjoint paths P_1, ..., P_k such that P_i goes from s_i to t_i. Schrijver [SICOMP'94] proved that the k-Vertex-Disjoint Paths problem on planar directed graphs can be solved in time n^{O(k)}. We give an algorithm with running time 2^{2^{O(k^2)}} n^{O(1)} for the problem, that is, we show the fixed-parameter tractability of the problem.
A Web-based Multilingual Intelligent Tutor System based on Jackson's Learning Styles Profiler and Expert Systems
Venue: arXiv cs.CY 2013
Year: 2013

Nowadays, Intelligent Tutoring Systems (ITSs) are so regarded in order to improve education quality via new technologies in this area. One of the problems is that the language of ITSs is different from the learner's. It forces the learners to learn the system language. This paper tries to remove this necessity by using an Automatic Translator Component in system structure like Google Translate API. This system carry out a pre-test and post-test by using Expert System and Jackson Model before and after of training a concept. It constantly updates learner model to save all changes in learning process. So this paper offers an E-Learning system which is web-based, intelligent, adaptive, multilingual and remotely accessible where tutors and learners can have non-identical language. It is also applicable Every Time and Every Where (ETEW). Furthermore, it trains the concepts in the best method with any language and low cost.
Polar Codes: Speed of polarization and polynomial gap to capacity
Venue: arXiv cs.IT 2013
Year: 2013

We prove that, for all binary-input symmetric memoryless channels, polar codes enable reliable communication at rates within $ε> 0$ of the Shannon capacity with a block length, construction complexity, and decoding complexity all bounded by a {\em polynomial} in $1/ε$. Polar coding gives the {\em first known explicit construction} with rigorous proofs of all these properties; previous constructions were not known to achieve capacity with less than $\exp(1/ε)$ decoding complexity except for erasure channels. We establish the capacity-achieving property of polar codes via a direct analysis of the underlying martingale of conditional entropies, without relying on the martingale convergence theorem. This step gives rough polarization (noise levels $\approx ε$ for the "good" channels), which can then be adequately amplified by tracking the decay of the channel Bhattacharyya parameters. Our effective bounds imply that polar codes can have block length (and encoding/decoding complexity) bounded by a polynomial in $1/ε$. The generator matrix of such polar codes can be constructed in polynomial time by algorithmically computing an adequate approximation of the polarization process.
Mining to Compact CNF Propositional Formulae
Venue: arXiv cs.AI 2013
Year: 2013

In this paper, we propose a first application of data mining techniques to propositional satisfiability. Our proposed Mining4SAT approach aims to discover and to exploit hidden structural knowledge for reducing the size of propositional formulae in conjunctive normal form (CNF). Mining4SAT combines both frequent itemset mining techniques and Tseitin's encoding for a compact representation of CNF formulae. The experiments of our Mining4SAT approach show interesting reductions of the sizes of many application instances taken from the last SAT competitions.
Simplified Compute-and-Forward and Its Performance Analysis
Venue: arXiv cs.IT 2013
Year: 2013

The compute-and-forward (CMF) method has shown a great promise as an innovative approach to exploit interference toward achieving higher network throughput. The CMF was primarily introduced by means of information theory tools. While there have been some recent works discussing different aspects of efficient and practical implementation of CMF, there are still some issues that are not covered. In this paper, we first introduce a method to decrease the implementation complexity of the CMF method. We then evaluate the exact outage probability of our proposed simplified CMF scheme, and hereby provide an upper bound on the outage probability of the optimum CMF in all SNR values, and a close approximation of its outage probability in low SNR regimes. We also evaluate the effect of the channel estimation error (CEE) on the performance of both optimum and our proposed simplified CMF by simulations. Our simulation results indicate that the proposed method is more robust against CEE than the optimum CMF method for the examples considered.
The Deterministic Multicast Capacity of 4-Node Relay Networks
Venue: arXiv cs.IT 2013
Year: 2013

In this paper, we completely characterize the deterministic capacity region of a four-node relay network with no direct links between the nodes, where each node communicates with the three other nodes via a relay. Towards this end, we develop an upper bound on the deterministic capacity region, based on the notion of a one-sided genie. To establish achievability, we use the detour schemes that achieve the upper bound by routing specific bits via indirect paths instead of sending them directly.
Abstraction and Acceleration in SMT-based Model-Checking for Array Programs
Venue: arXiv cs.LO 2013
Year: 2013

Abstraction (in its various forms) is a powerful established technique in model-checking; still, when unbounded data-structures are concerned, it cannot always cope with divergence phenomena in a satisfactory way. Acceleration is an approach which is widely used to avoid divergence, but it has been applied mostly to integer programs. This paper addresses the problem of accelerating transition relations for unbounded arrays with the ultimate goal of avoiding divergence during reachability analysis of abstract programs. For this, we first design a format to compute accelerations in this domain; then we show how to adapt the so-called 'monotonic abstraction' technique to efficiently handle complex formulas with nested quantifiers generated by the acceleration preprocessing. Notably, our technique can be easily plugged-in into abstraction/refinement loops, and strongly contributes to avoid divergence: experiments conducted with the MCMT model checker attest the effectiveness of our approach on programs with unbounded arrays, where acceleration and abstraction/refinement technologies fail if applied alone.
A New Perspective on Vertex Connectivity
Venue: arXiv cs.DM 2013
Year: 2013

Edge connectivity and vertex connectivity are two fundamental concepts in graph theory. Although by now there is a good understanding of the structure of graphs based on their edge connectivity, our knowledge in the case of vertex connectivity is much more limited. An essential tool in capturing edge connectivity are edge-disjoint spanning trees. The famous results of Tutte and Nash-Williams show that a graph with edge connectivity $λ$ contains $\floor{λ/2}$ edge-disjoint spanning trees. We present connected dominating set (CDS) partition and packing as tools that are analogous to edge-disjoint spanning trees and that help us to better grasp the structure of graphs based on their vertex connectivity. The objective of the CDS partition problem is to partition the nodes of a graph into as many connected dominating sets as possible. The CDS packing problem is the corresponding fractional relaxation, where CDSs are allowed to overlap as long as this is compensated by assigning appropriate weights. CDS partition and CDS packing can be viewed as the counterparts of the well-studied edge-disjoint spanning trees, focusing on vertex disjointedness rather than edge disjointness. We constructively show that every $k$-vertex-connected graph with $n$ nodes has a CDS packing of size $Ω(k/\log n)$ and a CDS partition of size $Ω(k/\log^5 n)$. We prove that the $Ω(k/\log n)$ CDS packing bound is existentially optimal. Using CDS packing, we show that if vertices of a $k$-vertex-connected graph are independently sampled with probability $p$, then the graph induced by the sampled vertices has vertex connectivity $\tildeΩ(kp^2)$. Moreover, using our $Ω(k/\log n)$ CDS packing, we get a store-and-forward broadcast algorithm with optimal throughput in the networking model where in each round, each node can send one bounded-size message to all its neighbors.
Speckle Reduction in Polarimetric SAR Imagery with Stochastic Distances and Nonlocal Means
Venue: arXiv cs.IT 2013
Year: 2013

This paper presents a technique for reducing speckle in Polarimetric Synthetic Aperture Radar (PolSAR) imagery using Nonlocal Means and a statistical test based on stochastic divergences. The main objective is to select homogeneous pixels in the filtering area through statistical tests between distributions. This proposal uses the complex Wishart model to describe PolSAR data, but the technique can be extended to other models. The weights of the location-variant linear filter are function of the p-values of tests which verify the hypothesis that two samples come from the same distribution and, therefore, can be used to compute a local mean. The test stems from the family of (h-phi) divergences which originated in Information Theory. This novel technique was compared with the Boxcar, Refined Lee and IDAN filters. Image quality assessment methods on simulated and real data are employed to validate the performance of this approach. We show that the proposed filter also enhances the polarimetric entropy and preserves the scattering information of the targets.
Tracking of Fingertips and Centres of Palm using KINECT
Venue: arXiv cs.CV 2013
Year: 2013

Hand Gesture is a popular way to interact or control machines and it has been implemented in many applications. The geometry of hand is such that it is hard to construct in virtual environment and control the joints but the functionality and DOF encourage researchers to make a hand like instrument. This paper presents a novel method for fingertips detection and centres of palms detection distinctly for both hands using MS KINECT in 3D from the input image. KINECT facilitates us by providing the depth information of foreground objects. The hands were segmented using the depth vector and centres of palms were detected using distance transformation on inverse image. This result would be used to feed the inputs to the robotic hands to emulate human hands operation.
Coding for Memory with Stuck-at Defects
Venue: arXiv cs.IT 2013
Year: 2013

In this paper, we propose an encoding scheme for partitioned linear block codes (PLBC) which mask the stuck-at defects in memories. In addition, we derive an upper bound and the estimate of the probability that masking fails. Numerical results show that PLBC can efficiently mask the defects with the proposed encoding scheme. Also, we show that our upper bound is very tight by using numerical results.
Polygon Matching and Indexing Under Affine Transformations
Venue: arXiv cs.CV 2013
Year: 2013

Given a collection $\{Z_1,Z_2,\ldots,Z_m\}$ of $n$-sided polygons in the plane and a query polygon $W$ we give algorithms to find all $Z_\ell$ such that $W=f(Z_\ell)$ with $f$ an unknown similarity transformation in time independent of the size of the collection. If $f$ is a known affine transformation, we show how to find all $Z_\ell$ such that $W=f(Z_\ell)$ in $O(n+\log(m))$ time. For a pair $W,W^\prime$ of polygons we can find all the pairs $Z_\ell,Z_{\ell^\prime}$ such that $W=f(Z_\ell)$ and $W^\prime=f(Z_{\ell^\prime})$ for an unknown affine transformation $f$ in $O(m+n)$ time. For the case of triangles we also give bounds for the problem of matching triangles with variable vertices, which is equivalent to affine matching triangles in noisy conditions.
Expressando Atributos Não-Funcionais em Workflows Científicos
Venue: arXiv cs.CE 2013
Year: 2013

In this paper we present OSC, a scientific workflow specification language based on software architecture principles. In contrast with other approaches, OSC employs connectors as first-class constructs. In this way, we leverage reusability and compositionality in the workflow modeling process, specially in the configuration of mechanisms that manage non-functional attributes.
Improving Resource Location with Locally Precomputed Partial Random Walks
Venue: arXiv cs.NI 2013
Year: 2013

Random walks can be used to search complex networks for a desired resource. To reduce search lengths, we propose a mechanism based on building random walks connecting together partial walks (PW) previously computed at each network node. Resources found in each PW are registered. Searches can then jump over PWs where the resource is not located. However, we assume that perfect recording of resources may be costly, and hence, probabilistic structures like Bloom filters are used. Then, unnecessary hops may come from false positives at the Bloom filters. Two variations of this mechanism have been considered, depending on whether we first choose a PW in the current node and then check it for the resource, or we first check all PWs and then choose one. In addition, PWs can be either simple random walks or self-avoiding random walks. Analytical models are provided to predict expected search lengths and other magnitudes of the resulting four mechanisms. Simulation experiments validate these predictions and allow us to compare these techniques with simple random walk searches, finding very large reductions of expected search lengths.
The Least Degraded and the Least Upgraded Channel with respect to a Channel Family
Venue: arXiv cs.IT 2013
Year: 2013

Given a family of binary-input memoryless output-symmetric (BMS) channels having a fixed capacity, we derive the BMS channel having the highest (resp. lowest) capacity among all channels that are degraded (resp. upgraded) with respect to the whole family. We give an explicit characterization of this channel as well as an explicit formula for the capacity of this channel.
Applications of Dynamical Systems in Engineering
Venue: arXiv cs.SY 2013
Year: 2013

This paper presents the current possible applications of Dynamical Systems in Engineering. The applications of chaos, fractals have proven to be an exciting and fruitful endeavor. These applications are highly diverse ranging over such fields as Electrical, Electronics and Computer Engineering. Dynamical Systems theory describes general patterns found in the solution of systems of nonlinear equations. The theory focuses upon those equations representing the change of processes in time. This paper offers the issue of applying dynamical systems methods to a wider circle of Engineering problems. There are three components to our approach: ongoing and possible applications of Fractals, Chaos Theory and Dynamical Systems. Some basic and useful computer simulation of Dynamical System related problems have been shown also.
Solving WCSP by Extraction of Minimal Unsatisfiable Cores
Venue: arXiv cs.AI 2013
Year: 2013

Usual techniques to solve WCSP are based on cost transfer operations coupled with a branch and bound algorithm. In this paper, we focus on an approach integrating extraction and relaxation of Minimal Unsatisfiable Cores in order to solve this problem. We decline our approach in two ways: an incomplete, greedy, algorithm and a complete one.
A SAT Approach to Clique-Width
Venue: arXiv cs.DS 2013
Year: 2013

Clique-width is a graph invariant that has been widely studied in combinatorics and computer science. However, computing the clique-width of a graph is an intricate problem, the exact clique-width is not known even for very small graphs. We present a new method for computing the clique-width of graphs based on an encoding to propositional satisfiability (SAT) which is then evaluated by a SAT solver. Our encoding is based on a reformulation of clique-width in terms of partitions that utilizes an efficient encoding of cardinality constraints. Our SAT-based method is the first to discover the exact clique-width of various small graphs, including famous graphs from the literature as well as random graphs of various density. With our method we determined the smallest graphs that require a small pre-described clique-width.
Analysing Mood Patterns in the United Kingdom through Twitter Content
Venue: arXiv cs.SI 2013
Year: 2013

Social Media offer a vast amount of geo-located and time-stamped textual content directly generated by people. This information can be analysed to obtain insights about the general state of a large population of users and to address scientific questions from a diversity of disciplines. In this work, we estimate temporal patterns of mood variation through the use of emotionally loaded words contained in Twitter messages, possibly reflecting underlying circadian and seasonal rhythms in the mood of the users. We present a method for computing mood scores from text using affective word taxonomies, and apply it to millions of tweets collected in the United Kingdom during the seasons of summer and winter. Our analysis results in the detection of strong and statistically significant circadian patterns for all the investigated mood types. Seasonal variation does not seem to register any important divergence in the signals, but a periodic oscillation within a 24-hour period is identified for each mood type. The main common characteristic for all emotions is their mid-morning peak, however their mood score patterns differ in the evenings.