OpenRaiser/Intern-Atlas huggingface dataset:
Easy Proofs of Löwenheim-Skolem Theorems by Means of Evaluation Games
Venue: arXiv cs.CY 2015
Year: 2015

We propose a proof of the downward Löwenheim-Skolem that relies on strategies deriving from evaluation games instead of the Skolem normal forms. This proof is simpler, and easily understood by the students, although it requires, when defining the semantics of first-order logic to introduce first a few notions inherited from game theory such as the one of an evaluation game.
The Sequent Calculus Trainer - Helping Students to Correctly Construct Proofs
Venue: arXiv cs.CY 2015
Year: 2015

We present the Sequent Calculus Trainer, a tool that supports students in learning how to correctly construct proofs in the sequent calculus for first-order logic with equality. It is a proof assistant fostering the understanding of all the syntactic principles that need to be obeyed in constructing correct proofs. It does not provide any help in finding good proof strategies. Instead it aims at understanding the sequent calculus on a lower syntactic level that needs to be mastered before one can consider proof strategies. Its main feature is a proper feedback system embedded in a graphical user interface. We also report on some empirical findings that indicate how the Sequent Calculus Trainer can improve the students' success in learning sequent calculus for full first-order logic.
Set theory and tableaux for teaching propositional logic
Venue: arXiv cs.CY 2015
Year: 2015

In this work we suggest the use of a set-theoretical interpretation of semantic tableaux for teaching propositional logic. If the student has previous notions of basic set theory, this approach to semantical tableaux can clarify her the way semantic trees operate, linking the syntactical and semantical sides of the process. Also, it may be useful for the introduction of more advanced topics in logic, like modal logic.
Teaching Logic for Computer Science: Are We Teaching the Wrong Narrative?
Venue: arXiv cs.CY 2015
Year: 2015

In this paper I discuss what, according to my long experience, every computer scientist should know from logic. We concentrate on issues of modeling, interpretability and levels of abstraction. We discuss what the minimal toolbox of logic tools should look like for a computer scientist who is involved in designing and analyzing reliable systems. We shall conclude that many classical topics dear to logicians are less important than usually presented, and that less-known ideas from logic may be more useful for the working computer scientist.
How to prove it in Natural Deduction: A Tactical Approach
Venue: arXiv cs.CY 2015
Year: 2015

The motivation for this paper comes out of our experience with teaching natural deduction (ND) and with the way this formal system is implemented by the \textsc{Coq} proof assistant, namely by means of so-called tactics, which are heuristics that transform a goal formula into a sequence of subgoals whose provability implies that of the original formula. We aim at capturing some of these tactics into a system of ND for minimal logic. Our goal is twofold: formal and didactic. The former delivers a formal system with its underlying heuristics to build proofs, which in turn serves our latter purpose, that of making an ideal system for the teaching of ND at an undergraduate level in a computer science program.
Transitioning to Proof
Venue: arXiv cs.CY 2015
Year: 2015

This paper describes some strategies used in a `transition' course. Such courses help undergraduate mathematics majors move from learning procedures to learning to function as critical mathematicians in order to understand and work with abstract concepts. One of the co-authors of this paper was a student of Leon Henkin. His influence on her helped shape the strategies used in the course, and is described at the end of the paper.
Http-Burst: Improving HTTP Efficiency in the Era of Bandwidth Hungry Web Applications
Venue: arXiv cs.NI 2015
Year: 2015

The Hypertext Transfer Protocol (HTTP), a key building block of the World Wide Web, has succeeded to enable information exchange worldwide. Since its first version in 1996, HTTP/1.0, the average number of inlined objects and average total bytes per webpage have been increasing significantly for desktops and mobiles, from 1-10 objects in 1996 to more than 100 objects in June 2014. Even if the retrieving of inlined objects can be parallelized as a given Hypertext Markup Language (HTML) document is streamed, a maximum number of connections is allocated, and thus as the number of inlined objects increases, the overall webpage load duration grows, and the HTTP servers loading also gets higher. To overcome this issue, we propose a new HTTP method called BURST, which allows to retrieve the missing inlined objects of a webpage efficiently by requesting sets of web objects. We experimentally demonstrate the potential via a proof-of-concept demonstration, by comparing the regular HTTP to proposed HTTP-Burst using a virtual private server and real HTTP client and server over the Internet. The results indicate a latency reduction of webpage load duration compared to HTTP as high as 52 % under the considered configurations.
On Probabilistic Completeness of Probabilistic Cell Decomposition
Venue: arXiv cs.RO 2015
Year: 2015

Probabilistic Cell Decomposition (PCD) is a probabilistic path planning method combining the concepts of approximate cell decomposition with probabilistic sampling. It has been shown that the use of lazy evaluation techniques and supervised sampling in important areas result in a high performance path planning method. Even if it was postulated before that PCD is probabilistically complete, we present a detailed proof of probabilistic completeness here for the first time.
Monitoring in IOT enabled devices
Venue: arXiv cs.NI 2015
Year: 2015

As network size continues to grow exponentially, there has been a proportionate increase in the number of nodes in the corresponding network. With the advent of Internet of things (IOT), it is assumed that many more devices will be connected to the existing network infrastructure. As a result, monitoring is expected to get more complex for administrators as networks tend to become more heterogeneous. Moreover, the addressing for IOTs would be more complex given the scale at which devices will be added to the network and hence monitoring is bound to become an uphill task due to management of larger range of addresses. This paper will throw light on what kind of monitoring mechanisms can be deployed in internet of things (IOTs) and their overall effectiveness.
Planning as Tabled Logic Programming
Venue: arXiv cs.AI 2015
Year: 2015

This paper describes Picat's planner, its implementation, and planning models for several domains used in International Planning Competition (IPC) 2014. Picat's planner is implemented by use of tabling. During search, every state encountered is tabled, and tabled states are used to effectively perform resource-bounded search. In Picat, structured data can be used to avoid enumerating all possible permutations of objects, and term sharing is used to avoid duplication of common state data. This paper presents several modeling techniques through the example models, ranging from designing state representations to facilitate data sharing and symmetry breaking, encoding actions with operations for efficient precondition checking and state updating, to incorporating domain knowledge and heuristics. Broadly, this paper demonstrates the effectiveness of tabled logic programming for planning, and argues the importance of modeling despite recent significant progress in domain-independent PDDL planners.
Fuzzy Overlapping Community Quality Metrics
Venue: arXiv cs.SI 2015
Year: 2015

Modularity is widely used to effectively measure the strength of the disjoint community structure found by community detection algorithms. Several overlapping extensions of modularity were proposed to measure the quality of overlapping community structure. However, all these extensions differ just in the way they define the belonging coefficient and belonging function. Yet, there is lack of systematic comparison of different extensions. To fill this gap, we overview overlapping extensions of modularity and generalize them with a uniform definition enabling application of different belonging coefficients and belonging functions to select the best. In addition, we extend localized modularity, modularity density, and eight local community quality metrics to enable their usages for overlapping communities. The experimental results on a large number of real networks and synthetic networks using overlapping extensions of modularity, overlapping modularity density, and local metrics show that the best results are obtained when the product of the belonging coefficients of two nodes is used as the belonging function. Moreover, the results may be used to guide researchers on which metrics to adopt when measuring the quality of overlapping community structure.
Distance labeling schemes for trees
Venue: arXiv cs.DS 2015
Year: 2015

We consider distance labeling schemes for trees: given a tree with $n$ nodes, label the nodes with binary strings such that, given the labels of any two nodes, one can determine, by looking only at the labels, the distance in the tree between the two nodes. A lower bound by Gavoille et. al. (J. Alg. 2004) and an upper bound by Peleg (J. Graph Theory 2000) establish that labels must use $Θ(\log^2 n)$ bits\footnote{Throughout this paper we use $\log$ for $\log_2$.}. Gavoille et. al. (ESA 2001) show that for very small approximate stretch, labels use $Θ(\log n \log \log n)$ bits. Several other papers investigate various variants such as, for example, small distances in trees (Alstrup et. al., SODA'03). We improve the known upper and lower bounds of exact distance labeling by showing that $\frac{1}{4} \log^2 n$ bits are needed and that $\frac{1}{2} \log^2 n$ bits are sufficient. We also give ($1+ε$)-stretch labeling schemes using $Θ(\log n)$ bits for constant $ε>0$. ($1+ε$)-stretch labeling schemes with polylogarithmic label size have previously been established for doubling dimension graphs by Talwar (STOC 2004). In addition, we present matching upper and lower bounds for distance labeling for caterpillars, showing that labels must have size $2\log n - Θ(\log\log n)$. For simple paths with $k$ nodes and edge weights in $[1,n]$, we show that labels must have size $\frac{k-1}{k}\log n+Θ(\log k)$.
Associative Measures and Multi-word Unit Extraction in Turkish
Venue: arXiv cs.CL 2015
Year: 2015

Associative measures are "mathematical formulas determining the strength of association between two or more words based on their occurrences and cooccurrences in a text corpus" (Pecina, 2010, p. 138). The purpose of this paper is to test the 12 associative measures that Text-NSP (Banerjee & Pedersen, 2003) contains on a 10-million-word subcorpus of Turkish National Corpus (TNC) (Aksan et.al., 2012). A statistical comparison of those measures is out of the scope of the study, and the measures will be evaluated according to the linguistic relevance of the rankings they provide. The focus of the study is basically on optimizing the corpus data, before applying the measures and then, evaluating the rankings produced by these measures as a whole, not on the linguistic relevance of individual n-grams. The findings include intra-linguistically relevant associative measures for a comma delimited, sentence splitted, lower-cased, well-balanced, representative, 10-million-word corpus of Turkish.
Relevance of Negative Links in Graph Partitioning: A Case Study Using Votes From the European Parliament
Venue: arXiv cs.SI 2015
Year: 2015

In this paper, we want to study the informative value of negative links in signed complex networks. For this purpose, we extract and analyze a collection of signed networks representing voting sessions of the European Parliament (EP). We first process some data collected by the VoteWatch Europe Website for the whole 7 th term (2009-2014), by considering voting similarities between Members of the EP to define weighted signed links. We then apply a selection of community detection algorithms, designed to process only positive links, to these data. We also apply Parallel Iterative Local Search (Parallel ILS), an algorithm recently proposed to identify balanced partitions in signed networks. Our results show that, contrary to the conclusions of a previous study focusing on other data, the partitions detected by ignoring or considering the negative links are indeed remarkably different for these networks. The relevance of negative links for graph partitioning therefore is an open question which should be further explored.
A numerical analysis of Quicksort: How many cases are bad cases?
Venue: arXiv cs.DS 2015
Year: 2015

We present numerical results for the probability of bad cases for Quicksort, i.e. cases of input data for which the sorting cost considerably exceeds that of the average. Dynamic programming was used to compute solutions of the recurrence for the frequency distributions of comparisons. From these solutions, probabilities of numbers of comparisons above certain thresholds relative to the average were extracted. Computations were done for array sizes up to n = 500 elements and for several methods to select the partitioning element, from a simple random selection to what we call "recursive median of three medians." We found that the probability strongly depends on the selection method: for n = 500 and a theshold 25% above the average number of comparisons it ranges from 2.2*10^(-3) to 3.0*10^(-23). A version of Quicksort based on the recursive median of medians approach is proposed, for which our data suggest a worst case time complexity of O(n^1.37).
Learning Boolean functions with concentrated spectra
Venue: arXiv cs.LG 2015
Year: 2015

This paper discusses the theory and application of learning Boolean functions that are concentrated in the Fourier domain. We first estimate the VC dimension of this function class in order to establish a small sample complexity of learning in this case. Next, we propose a computationally efficient method of empirical risk minimization, and we apply this method to the MNIST database of handwritten digits. These results demonstrate the effectiveness of our model for modern classification tasks. We conclude with a list of open problems for future investigation.
Bias and population structure in the actuation of sound change
Venue: arXiv cs.CL 2015
Year: 2015

Why do human languages change at some times, and not others? We address this longstanding question from a computational perspective, focusing on the case of sound change. Sound change arises from the pronunciation variability ubiquitous in every speech community, but most such variability does not lead to change. Hence, an adequate model must allow for stability as well as change. Existing theories of sound change tend to emphasize factors at the level of individual learners promoting one outcome or the other, such as channel bias (which favors change) or inductive bias (which favors stability). Here, we consider how the interaction of these biases can lead to both stability and change in a population setting. We find that population structure itself can act as a source of stability, but that both stability and change are possible only when both types of bias are active, suggesting that it is possible to understand why sound change occurs at some times and not others as the population-level result of the interplay between forces promoting each outcome in individual speakers. In addition, if it is assumed that learners learn from two or more teachers, the transition from stability to change is marked by a phase transition, consistent with the abrupt transitions seen in many empirical cases of sound change. The predictions of multiple-teacher models thus match empirical cases of sound change better than the predictions of single-teacher models, underscoring the importance of modeling language change in a population setting.
On Detecting Termination in Cognitive Radio Networks
Venue: arXiv cs.NI 2015
Year: 2015

The cognitive radio networks are an emerging wireless communication and computing paradigm. The cognitive radio nodes execute computations on multiple heterogeneous channels in the absence of licensed users (a.k.a. primary users) of those bands. Termination detection is a fundamental and non-trivial problem in distributed systems. In this paper, we propose a termination detection protocol for multi-hop cognitive radio networks where the cognitive radio nodes are allowed to tune to channels that are not currently occupied by primary users and to move to different locations during the protocol execution. The proposed protocol applies credit distribution and aggregation approach and maintains a new kind of logical structure, called the virtual tree-like structure. The virtual tree-like structure helps in decreasing the latency involved in announcing termination. Unlike conventional tree structures, the virtual tree-like structure does not require a specific node to act as the root node that has to stay involved in the computation until termination announcement; hence, the root node may become idle soon after finishing its computation. Also, the protocol is able to detect the presence of licensed users and announce strong or weak termination, whichever is possible.
Random Surfers on a Web Encyclopedia
Venue: arXiv cs.SI 2015
Year: 2015

The random surfer model is a frequently used model for simulating user navigation behavior on the Web. Various algorithms, such as PageRank, are based on the assumption that the model represents a good approximation of users browsing a website. However, the way users browse the Web has been drastically altered over the last decade due to the rise of search engines. Hence, new adaptations for the established random surfer model might be required, which better capture and simulate this change in navigation behavior. In this article we compare the classical uniform random surfer to empirical navigation and page access data in a Web Encyclopedia. Our high level contributions are (i) a comparison of stationary distributions of different types of the random surfer to quantify the similarities and differences between those models as well as (ii) new insights into the impact of search engines on traditional user navigation. Our results suggest that the behavior of the random surfer is almost similar to those of users - as long as users do not use search engines. We also find that classical website navigation structures, such as navigation hierarchies or breadcrumbs, only exercise limited influence on user navigation anymore. Rather, a new kind of navigational tools (e.g., recommendation systems) might be needed to better reflect the changes in browsing behavior of existing users.
Upper-Confidence-Bound Algorithms for Active Learning in Multi-Armed Bandits
Venue: arXiv cs.LG 2015
Year: 2015

In this paper, we study the problem of estimating uniformly well the mean values of several distributions given a finite budget of samples. If the variance of the distributions were known, one could design an optimal sampling strategy by collecting a number of independent samples per distribution that is proportional to their variance. However, in the more realistic case where the distributions are not known in advance, one needs to design adaptive sampling strategies in order to select which distribution to sample from according to the previously observed samples. We describe two strategies based on pulling the distributions a number of times that is proportional to a high-probability upper-confidence-bound on their variance (built from previous observed samples) and report a finite-sample performance analysis on the excess estimation error compared to the optimal allocation. We show that the performance of these allocation strategies depends not only on the variances but also on the full shape of the distributions.
Optimization of Demand Hotspot Capacities using Switched Multi-Element Antenna Equipped Small Cells
Venue: arXiv cs.NI 2015
Year: 2015

This paper presents switched Multi- Element Antennas (MEAs) as a simple, yet effective, method of enhancing the performance of small cell heterogeneous networks and compensating for the small cell base station sub-optimal placement. The switched MEA system is a low-cost system which enables the small cell to dynamically direct its transmission power toward locations of high user density, in other words demand hotspots. Our simulation results show that small cell base stations equipped with switched MEA systems offer greater performance than base stations equipped with omni-directional antennas in terms of both the number of users that can be served (and hence offloaded from the macrocell network) and in terms of overall network capacity. We also compare the performance of the switched MEA with fixed directional antennas and show that fixed-directional antennas can only outperform the switched MEA if the misalignment between their direction of transmission and the direction to the demand hotspot is less than 22.5 degrees.
The tree machine
Venue: arXiv cs.LO 2015
Year: 2015

A variant of Turing machines is introduced where the tape is replaced by a single tree which can be manipulated in a style akin to purely functional programming. This yields two benefits: first, the extra structure on the tape can be leveraged to write explicit constructions of machines much more easily than with Turing machines. Second, this new kind of machines models finely the asymptotic complexity of functional programming languages, and may allow to answer questions such as "is this problem inherently slower in functional languages".
On Information and Energy Cooperation in Energy Harvesting Cognitive Radio
Venue: arXiv cs.IT 2015
Year: 2015

This paper considers the cooperation between primary and secondary users at information and energy levels when both users are energy harvesting nodes. In particular, a secondary transmitter helps relaying the primary message, and in turn, gains the spectrum access as a reward. Also, the primary transmitter supplies energy to the secondary transmitter if the latter is energy-constrained, which facilitates an uninterrupted cooperation. We address this two-level cooperation over a finite horizon with the finite battery constraint at the secondary transmitter. While promising the rate-guaranteed service to both primary and secondary users, we aim to maximize the primary rate. We develop an iterative algorithm that obtains the optimal offline power policies for primary and secondary users. To acquire insights about the structure of the optimal solution, we examine specific scenarios. Furthermore, we investigate the effects of the secondary rate constraint and finite battery on the primary rate and the probability of cooperation. We show that the joint information and energy cooperation increases the chances of cooperation and achieves significant rate gains over only information cooperation.
Subspace selection for projection maximization with matroid constraints
Venue: arXiv cs.IT 2015
Year: 2015

Suppose that there is a ground set which consists of a large number of vectors in a Hilbert space. Consider the problem of selecting a subset of the ground set such that the projection of a vector of interest onto the subspace spanned by the vectors in the chosen subset reaches the maximum norm. This problem is generally NP-hard, and alternative approximation algorithms such as forward regression and orthogonal matching pursuit have been proposed as heuristic approaches. In this paper, we investigate bounds on the performance of these algorithms by introducing the notions of elemental curvatures. More specifically, we derive lower bounds, as functions of these elemental curvatures, for performance of the aforementioned algorithms with respect to that of the optimal solution under uniform and non-uniform matroid constraints, respectively. We show that if the elements in the ground set are mutually orthogonal, then these algorithms are optimal when the matroid is uniform and they achieve at least $1/2$-approximations of the optimal solution when the matroid is non-uniform.