OpenRaiser/Intern-Atlas huggingface dataset:
Pattern Matching for sets of segments
Venue: arXiv cs.CG 2000
Year: 2000

In this paper we present algorithms for a number of problems in geometric pattern matching where the input consist of a collections of segments in the plane. Our work consists of two main parts. In the first, we address problems and measures that relate to collections of orthogonal line segments in the plane. Such collections arise naturally from problems in mapping buildings and robot exploration. We propose a new measure of segment similarity called a \emph{coverage measure}, and present efficient algorithms for maximising this measure between sets of axis-parallel segments under translations. Our algorithms run in time $O(n^3\polylog n)$ in the general case, and run in time $O(n^2\polylog n)$ for the case when all segments are horizontal. In addition, we show that when restricted to translations that are only vertical, the Hausdorff distance between two sets of horizontal segments can be computed in time roughly $O(n^{3/2}{\sl polylog}n)$. These algorithms form significant improvements over the general algorithm of Chew et al. that takes time $O(n^4 \log^2 n)$. In the second part of this paper we address the problem of matching polygonal chains. We study the well known \Frd, and present the first algorithm for computing the \Frd under general translations. Our methods also yield algorithms for computing a generalization of the \Fr distance, and we also present a simple approximation algorithm for the \Frd that runs in time $O(n^2\polylog n)$.
Combining Linguistic and Spatial Information for Document Analysis
Venue: arXiv cs.CL 2000
Year: 2000

We present a framework to analyze color documents of complex layout. In addition, no assumption is made on the layout. Our framework combines in a content-driven bottom-up approach two different sources of information: textual and spatial. To analyze the text, shallow natural language processing tools, such as taggers and partial parsers, are used. To infer relations of the logical layout we resort to a qualitative spatial calculus closely related to Allen's calculus. We evaluate the system against documents from a color journal and present the results of extracting the reading order from the journal's pages. In this case, our analysis is successful as it extracts the intended reading order from the document.
Nimrod/G: An Architecture of a Resource Management and Scheduling System in a Global Computational Grid
Venue: arXiv cs.DC 2000
Year: 2000

The availability of powerful microprocessors and high-speed networks as commodity components has enabled high performance computing on distributed systems (wide-area cluster computing). In this environment, as the resources are usually distributed geographically at various levels (department, enterprise, or worldwide) there is a great challenge in integrating, coordinating and presenting them as a single resource to the user; thus forming a computational grid. Another challenge comes from the distributed ownership of resources with each resource having its own access policy, cost, and mechanism. The proposed Nimrod/G grid-enabled resource management and scheduling system builds on our earlier work on Nimrod and follows a modular and component-based architecture enabling extensibility, portability, ease of development, and interoperability of independently developed components. It uses the Globus toolkit services and can be easily extended to operate with any other emerging grid middleware services. It focuses on the management and scheduling of computations over dynamic resources scattered geographically across the Internet at department, enterprise, or global level with particular emphasis on developing scheduling schemes based on the concept of computational economy for a real test bed, namely, the Globus testbed (GUSTO).
Toward the Rectilinear Crossing Number of $K_n$: New Drawings, Upper Bounds, and Asymptotics
Venue: arXiv cs.DM 2000
Year: 2000

Scheinerman and Wilf (1994) assert that `an important open problem in the study of graph embeddings is to determine the rectilinear crossing number of the complete graph K_n.' A rectilinear drawing of K_n is an arrangement of n vertices in the plane, every pair of which is connected by an edge that is a line segment. We assume that no three vertices are collinear, and that no three edges intersect in a point unless that point is an endpoint of all three. The rectilinear crossing number of K_n is the fewest number of edge crossings attainable over all rectilinear drawings of K_n. For each n we construct a rectilinear drawing of K_n that has the fewest number of edge crossings and the best asymptotics known to date. Moreover, we give some alternative infinite families of drawings of K_n with good asymptotics. Finally, we mention some old and new open problems.
The Concurrent Language Aldwych
Venue: arXiv cs.PL 2000
Year: 2000

Aldwych is proposed as the foundation of a general purpose language for parallel applications. It works on a rule-based principle, and has aspects variously of concurrent functional, logic and object-oriented languages, yet it forms an integrated whole. It is intended to be applicable both for small-scale parallel programming, and for large-scale open systems.
Noise Effects in Fuzzy Modelling Systems
Venue: arXiv cs.NE 2000
Year: 2000

Noise is source of ambiguity for fuzzy systems. Although being an important aspect, the effects of noise in fuzzy modeling have been little investigated. This paper presents a set of tests using three well-known fuzzy modeling algorithms. These evaluate perturbations in the extracted rule-bases caused by noise polluting the learning data, and the corresponding deformations in each learned functional relation. We present results to show: 1) how these fuzzy modeling systems deal with noise; 2) how the established fuzzy model structure influences noise sensitivity of each algorithm; and 3) whose characteristics of the learning algorithms are relevant to noise attenuation.
Torque Ripple Minimization in a Switched Reluctance Drive by Neuro-Fuzzy Compensation
Venue: arXiv cs.RO 2000
Year: 2000

Simple power electronic drive circuit and fault tolerance of converter are specific advantages of SRM drives, but excessive torque ripple has limited its use to special applications. It is well known that controlling the current shape adequately can minimize the torque ripple. This paper presents a new method for shaping the motor currents to minimize the torque ripple, using a neuro-fuzzy compensator. In the proposed method, a compensating signal is added to the output of a PI controller, in a current-regulated speed control loop. Numerical results are presented in this paper, with an analysis of the effects of changing the form of the membership function of the neuro-fuzzy compensator.
Towards a Theory of Cache-Efficient Algorithms
Venue: arXiv cs.AR 2000
Year: 2000

We describe a model that enables us to analyze the running time of an algorithm in a computer with a memory hierarchy with limited associativity, in terms of various cache parameters. Our model, an extension of Aggarwal and Vitter's I/O model, enables us to establish useful relationships between the cache complexity and the I/O complexity of computations. As a corollary, we obtain cache-optimal algorithms for some fundamental problems like sorting, FFT, and an important subclass of permutations in the single-level cache model. We also show that ignoring associativity concerns could lead to inferior performance, by analyzing the average-case cache behavior of mergesort. We further extend our model to multiple levels of cache with limited associativity and present optimal algorithms for matrix transpose and sorting. Our techniques may be used for systematic exploitation of the memory hierarchy starting from the algorithm design stage, and dealing with the hitherto unresolved problem of limited associativity.
The Light Lexicographic path Ordering
Venue: arXiv cs.PL 2000
Year: 2000

We introduce syntactic restrictions of the lexicographic path ordering to obtain the Light Lexicographic Path Ordering. We show that the light lexicographic path ordering leads to a characterisation of the functions computable in space bounded by a polynomial in the size of the inputs.
Finding consensus in speech recognition: word error minimization and other applications of confusion networks
Venue: arXiv cs.CL 2000
Year: 2000

We describe a new framework for distilling information from word lattices to improve the accuracy of speech recognition and obtain a more perspicuous representation of a set of alternative hypotheses. In the standard MAP decoding approach the recognizer outputs the string of words corresponding to the path with the highest posterior probability given the acoustics and a language model. However, even given optimal models, the MAP decoder does not necessarily minimize the commonly used performance metric, word error rate (WER). We describe a method for explicitly minimizing WER by extracting word hypotheses with the highest posterior probabilities from word lattices. We change the standard problem formulation by replacing global search over a large set of sentence hypotheses with local search over a small set of word candidates. In addition to improving the accuracy of the recognizer, our method produces a new representation of the set of candidate hypotheses that specifies the sequence of word-level confusions in a compact lattice format. We study the properties of confusion networks and examine their use for other tasks, such as lattice compression, word spotting, confidence annotation, and reevaluation of recognition hypotheses using higher-level knowledge sources.
On Exponential-Time Completeness of the Circularity Problem for Attribute Grammars
Venue: arXiv cs.PL 2000
Year: 2000

Attribute grammars (AGs) are a formal technique for defining semantics of programming languages. Existing complexity proofs on the circularity problem of AGs are based on automata theory, such as writing pushdown acceptor and alternating Turing machines. They reduced the acceptance problems of above automata, which are exponential-time (EXPTIME) complete, to the AG circularity problem. These proofs thus show that the circularity problem is EXPTIME-hard, at least as hard as the most difficult problems in EXPTIME. However, none has given a proof for the EXPTIME-completeness of the problem. This paper first presents an alternating Turing machine for the circularity problem. The alternating Turing machine requires polynomial space. Thus, the circularity problem is in EXPTIME and is then EXPTIME-complete.
Internet Packet Filter Management and Rectangle Geometry
Venue: arXiv cs.CG 2000
Year: 2000

We consider rule sets for internet packet routing and filtering, where each rule consists of a range of source addresses, a range of destination addresses, a priority, and an action. A given packet should be handled by the action from the maximum priority rule that matches its source and destination. We describe new data structures for quickly finding the rule matching an incoming packet, in near-linear space, and a new algorithm for determining whether a rule set contains any conflicts, in time O(n^{3/2}).
Sequence-Based Abstract Interpretation of Prolog
Venue: arXiv cs.LO 2000
Year: 2000

Many abstract interpretation frameworks and analyses for Prolog have been proposed, which seek to extract information useful for program optimization. Although motivated by practical considerations, notably making Prolog competitive with imperative languages, such frameworks fail to capture some of the control structures of existing implementations of the language. In this paper we propose a novel framework for the abstract interpretation of Prolog which handles the depth-first search rule and the cut operator. It relies on the notion of substitution sequence to model the result of the execution of a goal. The framework consists of (i) a denotational concrete semantics, (ii) a safe abstraction of the concrete semantics defined in terms of a class of post-fixpoints, and (iii) a generic abstract interpretation algorithm. We show that traditional abstract domains of substitutions may easily be adapted to the new framework, and provide experimental evidence of the effectiveness of our approach. We also show that previous work on determinacy analysis, that was not expressible by existing abstract interpretation frameworks, can be seen as an instance of our framework.
Opportunity Cost Algorithms for Combinatorial Auctions
Venue: arXiv cs.CE 2000
Year: 2000

Two general algorithms based on opportunity costs are given for approximating a revenue-maximizing set of bids an auctioneer should accept, in a combinatorial auction in which each bidder offers a price for some subset of the available goods and the auctioneer can only accept non-intersecting bids. Since this problem is difficult even to approximate in general, the algorithms are most useful when the bids are restricted to be connected node subsets of an underlying object graph that represents which objects are relevant to each other. The approximation ratios of the algorithms depend on structural properties of this graph and are small constants for many interesting families of object graphs. The running times of the algorithms are linear in the size of the bid graph, which describes the conflicts between bids. Extensions of the algorithms allow for efficient processing of additional constraints, such as budget constraints that associate bids with particular bidders and limit how many bids from a particular bidder can be accepted.
A Formal Framework for Linguistic Annotation (revised version)
Venue: arXiv cs.CL 2000
Year: 2000

`Linguistic annotation' covers any descriptive or analytic notations applied to raw language data. The basic data may be in the form of time functions - audio, video and/or physiological recordings - or it may be textual. The added notations may include transcriptions of all sorts (from phonetic features to discourse structures), part-of-speech and sense tagging, syntactic analysis, `named entity' identification, co-reference annotation, and so on. While there are several ongoing efforts to provide formats and tools for such annotations and to publish annotated linguistic databases, the lack of widely accepted standards is becoming a critical problem. Proposed standards, to the extent they exist, have focused on file formats. This paper focuses instead on the logical structure of linguistic annotations. We survey a wide variety of existing annotation formats and demonstrate a common conceptual core, the annotation graph. This provides a formal framework for constructing, maintaining and searching linguistic annotations, while remaining consistent with many alternative data structures and file formats.
Lattice Structure and Convergence of a Game of Cards
Venue: arXiv cs.DM 2000
Year: 2000

This paper is devoted to the study of the dynamics of a discrete system related to some self stabilizing protocol on a ring of processors.
On the relationship between fuzzy logic and four-valued relevance logic
Venue: arXiv cs.AI 2000
Year: 2000

In fuzzy propositional logic, to a proposition a partial truth in [0,1] is assigned. It is well known that under certain circumstances, fuzzy logic collapses to classical logic. In this paper, we will show that under dual conditions, fuzzy logic collapses to four-valued (relevance) logic, where propositions have truth-value true, false, unknown, or contradiction. As a consequence, fuzzy entailment may be considered as ``in between'' four-valued (relevance) entailment and classical entailment.
Anonymous Oblivious Transfer
Venue: arXiv cs.CR 2000
Year: 2000

In this short note we want to introduce {\em anonymous oblivious transfer} a new cryptographic primitive which can be proven to be strictly more powerful than oblivious transfer. We show that all functions can be robustly realized by multi party protocols with {\em anonymous oblivious transfer}. No assumption about possible collusions of cheaters or disruptors have to be made. Furthermore we shortly discuss how to realize anonymous oblivious transfer with oblivious broadcast or by quantum cryptography. The protocol of anonymous oblivious transfer was inspired by a quantum protocol: the anonymous quantum channel.
Non-intrusive on-the-fly data race detection using execution replay
Venue: arXiv cs.SE 2000
Year: 2000

This paper presents a practical solution for detecting data races in parallel programs. The solution consists of a combination of execution replay (RecPlay) with automatic on-the-fly data race detection. This combination enables us to perform the data race detection on an unaltered execution (almost no probe effect). Furthermore, the usage of multilevel bitmaps and snooped matrix clocks limits the amount of memory used. As the record phase of RecPlay is highly efficient, there is no need to switch it off, hereby eliminating the possibility of Heisenbugs because tracing can be left on all the time.
Small Maximal Independent Sets and Faster Exact Graph Coloring
Venue: arXiv cs.DS 2000
Year: 2000

We show that, for any n-vertex graph G and integer parameter k, there are at most 3^{4k-n}4^{n-3k} maximal independent sets I \subset G with |I| <= k, and that all such sets can be listed in time O(3^{4k-n} 4^{n-3k}). These bounds are tight when n/4 <= k <= n/3. As a consequence, we show how to compute the exact chromatic number of a graph in time O((4/3 + 3^{4/3}/4)^n) ~= 2.4150^n, improving a previous O((1+3^{1/3})^n) ~= 2.4422^n algorithm of Lawler (1976).
EquiX---A Search and Query Language for XML
Venue: arXiv cs.DB 2000
Year: 2000

EquiX is a search language for XML that combines the power of querying with the simplicity of searching. Requirements for such languages are discussed and it is shown that EquiX meets the necessary criteria. Both a graphical abstract syntax and a formal concrete syntax are presented for EquiX queries. In addition, the semantics is defined and an evaluation algorithm is presented. The evaluation algorithm is polynomial under combined complexity. EquiX combines pattern matching, quantification and logical expressions to query both the data and meta-data of XML documents. The result of a query in EquiX is a set of XML documents. A DTD describing the result documents is derived automatically from the query.
Support for Debugging Automatically Parallelized Programs
Venue: arXiv cs.SE 2000
Year: 2000

We describe a system that simplifies the process of debugging programs produced by computer-aided parallelization tools. The system uses relative debugging techniques to compare serial and parallel executions in order to show where the computations begin to differ. If the original serial code is correct, errors due to parallelization will be isolated by the comparison. One of the primary goals of the system is to minimize the effort required of the user. To that end, the debugging system uses information produced by the parallelization tool to drive the comparison process. In particular, the debugging system relies on the parallelization tool to provide information about where variables may have been modified and how arrays are distributed across multiple processes. User effort is also reduced through the use of dynamic instrumentation. This allows us to modify the program execution without changing the way the user builds the executable. The use of dynamic instrumentation also permits us to compare the executions in a fine-grained fashion and only involve the debugger when a difference has been detected. This reduces the overhead of executing instrumentation.
Slicing of Constraint Logic Programs
Venue: arXiv cs.SE 2000
Year: 2000

Slicing is a program analysis technique originally developed for imperative languages. It facilitates understanding of data flow and debugging. This paper discusses slicing of Constraint Logic Programs. Constraint Logic Programming (CLP) is an emerging software technology with a growing number of applications. Data flow in constraint programs is not explicit, and for this reason the concepts of slice and the slicing techniques of imperative languages are not directly applicable. This paper formulates declarative notions of slice suitable for CLP. They provide a basis for defining slicing techniques (both dynamic and static) based on variable sharing. The techniques are further extended by using groundness information. A prototype dynamic slicer of CLP programs implementing the presented ideas is briefly described together with the results of some slicing experiments.
Natural Deduction as Higher-Order Resolution
Venue: arXiv cs.LO 2000
Year: 2000

An interactive theorem prover, Isabelle, is under development. In LCF, each inference rule is represented by one function for forwards proof and another (a tactic) for backwards proof. In Isabelle, each inference rule is represented by a Horn clause. Resolution gives both forwards and backwards proof, supporting a large class of logics. Isabelle has been used to prove theorems in Martin-Löf's Constructive Type Theory. Quantifiers pose several difficulties: substitution, bound variables, Skolemization. Isabelle's representation of logical syntax is the typed lambda-calculus, requiring higher- order unification. It may have potential for logic programming. Depth-first subgoaling along inference rules constitutes a higher-order Prolog.
Isabelle: The Next 700 Theorem Provers
Venue: arXiv cs.LO 2000
Year: 2000

Isabelle is a generic theorem prover, designed for interactive reasoning in a variety of formal theories. At present it provides useful proof procedures for Constructive Type Theory, various first-order logics, Zermelo-Fraenkel set theory, and higher-order logic. This survey of Isabelle serves as an introduction to the literature. It explains why generic theorem proving is beneficial. It gives a thorough history of Isabelle, beginning with its origins in the LCF system. It presents an account of how logics are represented, illustrated using classical logic. The approach is compared with the Edinburgh Logical Framework. Several of the Isabelle object-logics are presented.
A Formulation of the Simple Theory of Types (for Isabelle)
Venue: arXiv cs.LO 2000
Year: 2000

Simple type theory is formulated for use with the generic theorem prover Isabelle. This requires explicit type inference rules. There are function, product, and subset types, which may be empty. Descriptions (the eta-operator) introduce the Axiom of Choice. Higher-order logic is obtained through reflection between formulae and terms of type bool. Recursive types and functions can be formally constructed. Isabelle proof procedures are described. The logic appears suitable for general mathematics as well as computational problems.
Set Theory for Verification: II. Induction and Recursion
Venue: arXiv cs.LO 2000
Year: 2000

A theory of recursive definitions has been mechanized in Isabelle's Zermelo-Fraenkel (ZF) set theory. The objective is to support the formalization of particular recursive definitions for use in verification, semantics proofs and other computational reasoning. Inductively defined sets are expressed as least fixedpoints, applying the Knaster-Tarski Theorem over a suitable set. Recursive functions are defined by well-founded recursion and its derivatives, such as transfinite recursion. Recursive data structures are expressed by applying the Knaster-Tarski Theorem to a set, such as V[omega], that is closed under Cartesian product and disjoint sum. Worked examples include the transitive closure of a relation, lists, variable-branching trees and mutually recursive trees and forests. The Schröder-Bernstein Theorem and the soundness of propositional logic are proved in Isabelle sessions.