OpenRaiser/Intern-Atlas huggingface dataset:
Predicate Logic with Definitions
Venue: arXiv cs.LO 1999
Year: 1999

Predicate Logic with Definitions (PLD or D-logic) is a modification of first-order logic intended mostly for practical formalization of mathematics. The main syntactic constructs of D-logic are terms, formulas and definitions. A definition is a definition of variables, a definition of constants, or a composite definition (D-logic has also abbreviation definitions called abbreviations). Definitions can be used inside terms and formulas. This possibility alleviates introducing new quantifier-like names. Composite definitions allow constructing new definitions from existing ones.
A Newton method without evaluation of nonlinear function values
Venue: arXiv cs.CE 1999
Year: 1999

The present author recently proposed and proved a relationship theorem between nonlinear polynomial equations and the corresponding Jacobian matrix. By using this theorem, this paper derives a Newton iterative formula without requiring the evaluation of nonlinear function values in the solution of nonlinear polynomial-only problems.
Learning Transformation Rules to Find Grammatical Relations
Venue: arXiv cs.CL 1999
Year: 1999

Grammatical relationships are an important level of natural language processing. We present a trainable approach to find these relationships through transformation sequences and error-driven learning. Our approach finds grammatical relationships between core syntax groups and bypasses much of the parsing phase. On our training and test set, our procedure achieves 63.6% recall and 77.3% precision (f-score = 69.8).
Reconstructing Polyatomic Structures from Discrete X-Rays: NP-Completeness Proof for Three Atoms
Venue: arXiv cs.DS 1999
Year: 1999

We address a discrete tomography problem that arises in the study of the atomic structure of crystal lattices. A polyatomic structure T can be defined as an integer lattice in dimension D>=2, whose points may be occupied by $c$ distinct types of atoms. To ``analyze'' T, we conduct ell measurements that we call_discrete X-rays_. A discrete X-ray in direction xi determines the number of atoms of each type on each line parallel to xi. Given ell such non-parallel X-rays, we wish to reconstruct T. The complexity of the problem for c=1 (one atom type) has been completely determined by Gardner, Gritzmann and Prangenberg, who proved that the problem is NP-complete for any dimension D>=2 and ell>=3 non-parallel X-rays, and that it can be solved in polynomial time otherwise. The NP-completeness result above clearly extends to any c>=2, and therefore when studying the polyatomic case we can assume that ell=2. As shown in another article by the same authors, this problem is also NP-complete for c>=6 atoms, even for dimension D=2 and axis-parallel X-rays. They conjecture that the problem remains NP-complete for c=3,4,5, although, as they point out, the proof idea does not seem to extend to c<=5. We resolve the conjecture by proving that the problem is indeed NP-complete for c>=3 in 2D, even for axis-parallel X-rays. Our construction relies heavily on some structure results for the realizations of 0-1 matrices with given row and column sums.
Resolving Part-of-Speech Ambiguity in the Greek Language Using Learning Techniques
Venue: arXiv cs.CL 1999
Year: 1999

This article investigates the use of Transformation-Based Error-Driven learning for resolving part-of-speech ambiguity in the Greek language. The aim is not only to study the performance, but also to examine its dependence on different thematic domains. Results are presented here for two different test cases: a corpus on "management succession events" and a general-theme corpus. The two experiments show that the performance of this method does not depend on the thematic domain of the corpus, and its accuracy for the Greek language is around 95%.
Events in Linear-Time Properties
Venue: arXiv cs.SE 1999
Year: 1999

For over a decade, researchers in formal methods tried to create formalisms that permit natural specification of systems and allow mathematical reasoning about their correctness. The availability of fully-automated reasoning tools enables more non-specialists to use formal methods effectively --- their responsibility reduces to just specifying the model and expressing the desired properties. Thus, it is essential that these properties be represented in a language that is easy to use and sufficiently expressive. Linear-time temporal logic is a formalism that has been extensively used by researchers for specifying properties of systems. When such properties are closed under stuttering, i.e. their interpretation is not modified by transitions that leave the system in the same state, verification tools can utilize a partial-order reduction technique to reduce the size of the model and thus analyze larger systems. If LTL formulas do not contain the ``next'' operator, the formulas are closed under stuttering, but the resulting language is not expressive enough to capture many important properties, e.g., properties involving events. Determining if an arbitrary LTL formula is closed under stuttering is hard --- it has been proven to be PSPACE-complete. In this paper we relax the restriction on LTL that guarantees closure under stuttering, introduce the notion of edges in the context of LTL, and provide theorems that enable syntactic reasoning about closure under stuttering of LTL formulas.
Microsoft TerraServer: A Spatial Data Warehouse
Venue: arXiv cs.DB 1999
Year: 1999

The TerraServer stores aerial, satellite, and topographic images of the earth in a SQL database available via the Internet. It is the world's largest online atlas, combining five terabytes of image data from the United States Geological Survey (USGS) and SPIN-2. This report describes the system-redesign based on our experience over the last year. It also reports usage and operations results over the last year -- over 2 billion web hits and over 20 Terabytes of imagry served over the Internet. Internet browsers provide intuitive spatial and text interfaces to the data. Users need no special hardware, software, or knowledge to locate and browse imagery. This paper describes how terabytes of "Internet unfriendly" geo-spatial images were scrubbed and edited into hundreds of millions of "Internet friendly" image tiles and loaded into a SQL data warehouse. Microsoft TerraServer demonstrates that general-purpose relational database technology can manage large scale image repositories, and shows that web browsers can be a good geospatial image presentation system.
Generalized linearization in nonlinear modeling of data
Venue: arXiv cs.CE 1999
Year: 1999

The principal innovative idea in this paper is to transform the original complex nonlinear modeling problem into a combination of linear problem and very simple nonlinear problems. The key step is the generalized linearization of nonlinear terms. This paper only presents the introductory strategy of this methodology. The practical numerical experiments will be provided subsequently.
The union of unit balls has quadratic complexity, even if they all contain the origin
Venue: arXiv cs.CG 1999
Year: 1999

We provide a lower bound construction showing that the union of unit balls in three-dimensional space has quadratic complexity, even if they all contain the origin. This settles a conjecture of Sharir.
Mixing representation levels: The hybrid approach to automatic text generation
Venue: arXiv cs.CL 1999
Year: 1999

Natural language generation systems (NLG) map non-linguistic representations into strings of words through a number of steps using intermediate representations of various levels of abstraction. Template based systems, by contrast, tend to use only one representation level, i.e. fixed strings, which are combined, possibly in a sophisticated way, to generate the final text. In some circumstances, it may be profitable to combine NLG and template based techniques. The issue of combining generation techniques can be seen in more abstract terms as the issue of mixing levels of representation of different degrees of linguistic abstraction. This paper aims at defining a reference architecture for systems using mixed representations. We argue that mixed representations can be used without abandoning a linguistically grounded approach to language generation.
A Probabilistic Analysis of the Power of Arithmetic Filters
Venue: arXiv cs.CG 1999
Year: 1999

The assumption of real-number arithmetic, which is at the basis of conventional geometric algorithms, has been seriously challenged in recent years, since digital computers do not exhibit such capability. A geometric predicate usually consists of evaluating the sign of some algebraic expression. In most cases, rounded computations yield a reliable result, but sometimes rounded arithmetic introduces errors which may invalidate the algorithms. The rounded arithmetic may produce an incorrect result only if the exact absolute value of the algebraic expression is smaller than some (small) varepsilon, which represents the largest error that may arise in the evaluation of the expression. The threshold varepsilon depends on the structure of the expression and on the adopted computer arithmetic, assuming that the input operands are error-free. A pair (arithmetic engine,threshold) is an "arithmetic filter". In this paper we develop a general technique for assessing the efficacy of an arithmetic filter. The analysis consists of evaluating both the threshold and the probability of failure of the filter. To exemplify the approach, under the assumption that the input points be chosen randomly in a unit ball or unit cube with uniform density, we analyze the two important predicates "which-side" and "insphere". We show that the probability that the absolute values of the corresponding determinants be no larger than some positive value V, with emphasis on small V, is Theta(V) for the which-side predicate, while for the insphere predicate it is Theta(V^(2/3)) in dimension 1, O(sqrt(V)) in dimension 2, and O(sqrt(V) ln(1/V)) in higher dimensions. Constants are small, and are given in the paper.
Algorithms for Coloring Quadtrees
Venue: arXiv cs.CG 1999
Year: 1999

We describe simple linear time algorithms for coloring the squares of balanced and unbalanced quadtrees so that no two adjacent squares are given the same color. If squares sharing sides are defined as adjacent, we color balanced quadtrees with three colors, and unbalanced quadtrees with four colors; these results are both tight, as some quadtrees require this many colors. If squares sharing corners are defined as adjacent, we color balanced or unbalanced quadtrees with six colors; for some quadtrees, at least five colors are required.
After Compilers and Operating Systems : The Third Advance in Application Support
Venue: arXiv cs.PL 1999
Year: 1999

After compilers and operating systems, TSIAs are the third advance in application support. A compiler supports a high level application definition in a programming language. An operating system supports a high level interface to the resources used by an application execution. A Task System and Item Architecture (TSIA) provides an application with a transparent reliable, distributed, heterogeneous, adaptive, dynamic, real-time, interactive, parallel, secure or other execution. In addition to supporting the application execution, a TSIA also supports the application definition. This run-time support for the definition is complementary to the compile-time support of a compiler. For example, this allows a language similar to Fortran or C to deliver features promised by functional computing. While many TSIAs exist, they previously have not been recognized as such and have served only a particular type of application. Existing TSIAs and other projects demonstrate that TSIAs are feasible for most applications. As the next paradigm for application support, the TSIA simplifies and unifies existing computing practice and research. By solving many outstanding problems, the TSIA opens many, many new opportunities for computing.
Secure Multicast in a WAN
Venue: arXiv cs.CR 1999
Year: 1999

A secure reliable multicast protocol enables a process to send a message to a group of recipients such that all correct destinations receive the same message, despite the malicious efforts of fewer than a third of the total number of processes, including the sender. This has been sh own to be a useful tool in building secure distributed services, albeit with a cost that typically grows linearly with the size of the system. For very large networks, for which this is prohibitive, we present two approaches for reducing the cost: First, we show a protocol whose cost is on the order of the number of tolerated failures. Secondly, we show how relaxing the consistency requirement to a probabilistic guarantee can reduce the associated cost, effectively to a constant.
A Differential Invariant for Zooming
Venue: arXiv cs.CV 1999
Year: 1999

This paper presents an invariant under scaling and linear brightness change. The invariant is based on differentials and therefore is a local feature. Rotationally invariant 2-d differential Gaussian operators up to third order are proposed for the implementation of the invariant. The performance is analyzed by simulating a camera zoom-out.
Motion Planning of Legged Robots
Venue: arXiv cs.CG 1999
Year: 1999

We study the problem of computing the free space F of a simple legged robot called the spider robot. The body of this robot is a single point and the legs are attached to the body. The robot is subject to two constraints: each leg has a maximal extension R (accessibility constraint) and the body of the robot must lie above the convex hull of its feet (stability constraint). Moreover, the robot can only put its feet on some regions, called the foothold regions. The free space F is the set of positions of the body of the robot such that there exists a set of accessible footholds for which the robot is stable. We present an efficient algorithm that computes F in O(n2 log n) time using O(n2 alpha(n)) space for n discrete point footholds where alpha(n) is an extremely slowly growing function (alpha(n) <= 3 for any practical value of n). We also present an algorithm for computing F when the foothold regions are pairwise disjoint polygons with n edges in total. This algorithm computes F in O(n2 alpha8(n) log n) time using O(n2 alpha8(n)) space (alpha8(n) is also an extremely slowly growing function). These results are close to optimal since Omega(n2) is a lower bound for the size of F.
Automatic Generation of Constraint Propagation Algorithms for Small Finite Domains
Venue: arXiv cs.AI 1999
Year: 1999

We study here constraint satisfaction problems that are based on predefined, explicitly given finite constraints. To solve them we propose a notion of rule consistency that can be expressed in terms of rules derived from the explicit representation of the initial constraints. This notion of local consistency is weaker than arc consistency for constraints of arbitrary arity but coincides with it when all domains are unary or binary. For Boolean constraints rule consistency coincides with the closure under the well-known propagation rules for Boolean constraints. By generalizing the format of the rules we obtain a characterization of arc consistency in terms of so-called inclusion rules. The advantage of rule consistency and this rule based characterization of the arc consistency is that the algorithms that enforce both notions can be automatically generated, as CHR rules. So these algorithms could be integrated into constraint logic programming systems such as Eclipse. We illustrate the usefulness of this approach to constraint propagation by discussing the implementations of both algorithms and their use on various examples, including Boolean constraints, three valued logic of Kleene, constraints dealing with Waltz's language for describing polyhedreal scenes, and Allen's qualitative approach to temporal logic.
Finding an ordinary conic and an ordinary hyperplane
Venue: arXiv cs.CG 1999
Year: 1999

Given a finite set of non-collinear points in the plane, there exists a line that passes through exactly two points. Such a line is called an ordinary line. An efficient algorithm for computing such a line was proposed by Mukhopadhyay et al. In this note we extend this result in two directions. We first show how to use this algorithm to compute an ordinary conic, that is, a conic passing through exactly five points, assuming that all the points do not lie on the same conic. Both our proofs of existence and the consequent algorithms are simpler than previous ones. We next show how to compute an ordinary hyperplane in three and higher dimensions.
Knowledge in Multi-Agent Systems: Initial Configurations and Broadcast
Venue: arXiv cs.LO 1999
Year: 1999

The semantic framework for the modal logic of knowledge due to Halpern and Moses provides a way to ascribe knowledge to agents in distributed and multi-agent systems. In this paper we study two special cases of this framework: full systems and hypercubes. Both model static situations in which no agent has any information about another agent's state. Full systems and hypercubes are an appropriate model for the initial configurations of many systems of interest. We establish a correspondence between full systems and hypercube systems and certain classes of Kripke frames. We show that these classes of systems correspond to the same logic. Moreover, this logic is also the same as that generated by the larger class of weakly directed frames. We provide a sound and complete axiomatization, S5WDn, of this logic. Finally, we show that under certain natural assumptions, in a model where knowledge evolves over time, S5WDn characterizes the properties of knowledge not just at the initial configuration, but also at all later configurations. In particular, this holds for homogeneous broadcast systems, which capture settings in which agents are initially ignorant of each others local states, operate synchronously, have perfect recall and can communicate only by broadcasting.
Query Order
Venue: arXiv cs.CC 1999
Year: 1999

We study the effect of query order on computational power, and show that $\pjk$-the languages computable via a polynomial-time machine given one query to the jth level of the boolean hierarchy followed by one query to the kth level of the boolean hierarchy-equals $\redttnp{j+2k-1}$ if j is even and k is odd, and equals $\redttnp{j+2k}$ otherwise. Thus, unless the polynomial hierarchy collapses, it holds that for each $1\leq j \leq k$: $\pjk = \pkj \iff (j=k) \lor (j{is even} \land k=j+1)$. We extend our analysis to apply to more general query classes.
Decoupling Control from Data for TCP Congestion Control
Venue: arXiv cs.NI 1999
Year: 1999

Many applications want to use TCP congestion control to regulate the transmission rate of a data packet stream. A natural way to achieve this goal is to transport the data packet stream on a TCP connection. However, because TCP implements both congestion and error control, transporting a data packet stream directly using a TCP connection forces the data packet stream to be subject to TCP's other properties caused by TCP error control, which may be inappropriate for these applications. The TCP decoupling approach proposed in this thesis is a novel way of applying TCP congestion control to a data packet stream without actually transporting the data packet stream on a TCP connection. Instead, a TCP connection using the same network path as the data packet stream is set up separately and the transmission rate of the data packet stream is then associated with that of the TCP packets. Since the transmission rate of these TCP packets is under TCP congestion control, so is that of the data packet stream. Furthermore, since the data packet stream is not transported on a TCP connection, the regulated data packet stream is not subject to TCP error control. Because of this flexibility, the TCP decoupling approach opens up many new opportunities, solves old problems, and improves the performance of some existing applications. All of these advantages will be demonstrated in the thesis. This thesis presents the design, implementation, and analysis of the TCP decoupling approach, and its successful applications in TCP trunking, wireless communication, and multimedia streaming.
Practical experiments with regular approximation of context-free languages
Venue: arXiv cs.CL 1999
Year: 1999

Several methods are discussed that construct a finite automaton given a context-free grammar, including both methods that lead to subsets and those that lead to supersets of the original context-free language. Some of these methods of regular approximation are new, and some others are presented here in a more refined form with respect to existing literature. Practical experiments with the different methods of regular approximation are performed for spoken-language input: hypotheses from a speech recognizer are filtered through a finite automaton.
One-Way Functions in Worst-Case Cryptography: Algebraic and Security Properties
Venue: arXiv cs.CC 1999
Year: 1999

We survey recent developments in the study of (worst-case) one-way functions having strong algebraic and security properties. According to [RS93], this line of research was initiated in 1984 by Rivest and Sherman who designed two-party secret-key agreement protocols that use strongly noninvertible, total, associative one-way functions as their key building blocks. If commutativity is added as an ingredient, these protocols can be used by more than two parties, as noted by Rabi and Sherman [RS93] who also developed digital signature protocols that are based on such enhanced one-way functions. Until recently, it was an open question whether one-way functions having the algebraic and security properties that these protocols require could be created from any given one-way function. Recently, Hemaspaandra and Rothe [HR99] resolved this open issue in the affirmative, by showing that one-way functions exist if and only if strong, total, commutative, associative one-way functions exist. We discuss this result, and the work of Rabi, Rivest, and Sherman, and recent work of Homan [Hom99] that makes progress on related issues.
PushPush is NP-hard in 3D
Venue: arXiv cs.CG 1999
Year: 1999

We prove that a particular pushing-blocks puzzle is intractable in 3D. The puzzle, inspired by the game PushPush, consists of unit square blocks on an integer lattice. An agent may push blocks (but never pull them) in attempting to move between given start and goal positions. In the PushPush version, the agent can only push one block at a time, and moreover, each block, when pushed, slides the maximal extent of its free range. We prove this version is NP-hard in 3D by reduction from SAT. The corresponding problem in 2D remains open.
An Example-Based Approach to Japanese-to-English Translation of Tense, Aspect, and Modality
Venue: arXiv cs.CL 1999
Year: 1999

We have developed a new method for Japanese-to-English translation of tense, aspect, and modality that uses an example-based method. In this method the similarity between input and example sentences is defined as the degree of semantic matching between the expressions at the ends of the sentences. Our method also uses the k-nearest neighbor method in order to exclude the effects of noise; for example, wrongly tagged data in the bilingual corpora. Experiments show that our method can translate tenses, aspects, and modalities more accurately than the top-level MT software currently available on the market can. Moreover, it does not require hand-craft rules.