OpenRaiser/Intern-Atlas huggingface dataset:
Constructing Recursion Operators in Intuitionistic Type Theory
Venue: arXiv cs.LO 2000
Year: 2000

Martin-Löf's Intuitionistic Theory of Types is becoming popular for formal reasoning about computer programs. To handle recursion schemes other than primitive recursion, a theory of well-founded relations is presented. Using primitive recursion over higher types, induction and recursion are formally derived for a large class of well-founded relations. Included are < on natural numbers, and relations formed by inverse images, addition, multiplication, and exponentiation of other relations. The constructions are given in full detail to allow their use in theorem provers for Type Theory, such as Nuprl. The theory is compared with work in the field of ordinal recursion over higher types.
The Foundation of a Generic Theorem Prover
Venue: arXiv cs.LO 2000
Year: 2000

Isabelle is an interactive theorem prover that supports a variety of logics. It represents rules as propositions (not as functions) and builds proofs by combining rules. These operations constitute a meta-logic (or `logical framework') in which the object-logics are formalized. Isabelle is now based on higher-order logic -- a precise and well-understood foundation. Examples illustrate use of this meta-logic to formalize logics and proofs. Axioms for first-order logic are shown sound and complete. Backwards proof is formalized by meta-reasoning about object-level entailment. Higher-order logic has several practical advantages over other meta-logics. Many proof techniques are known, such as Huet's higher-order unification procedure.
Incremental and Decremental Maintenance of Planar Width
Venue: arXiv cs.CG 2000
Year: 2000

We present an algorithm for maintaining the width of a planar point set dynamically, as points are inserted or deleted. Our algorithm takes time O(kn^epsilon) per update, where k is the amount of change the update causes in the convex hull, n is the number of points in the set, and epsilon is any arbitrarily small constant. For incremental or decremental update sequences, the amortized time per update is O(n^epsilon).
Clausal Temporal Resolution
Venue: arXiv cs.LO 2000
Year: 2000

In this article, we examine how clausal resolution can be applied to a specific, but widely used, non-classical logic, namely discrete linear temporal logic. Thus, we first define a normal form for temporal formulae and show how arbitrary temporal formulae can be translated into the normal form, while preserving satisfiability. We then introduce novel resolution rules that can be applied to formulae in this normal form, provide a range of examples and examine the correctness and complexity of this approach is examined and. This clausal resolution approach. Finally, we describe related work and future developments concerning this work.
Communication Complexity Lower Bounds by Polynomials
Venue: arXiv cs.CC 2000
Year: 2000

The quantum version of communication complexity allows the two communicating parties to exchange qubits and/or to make use of prior entanglement (shared EPR-pairs). Some lower bound techniques are available for qubit communication complexity, but except for the inner product function, no bounds are known for the model with unlimited prior entanglement. We show that the log-rank lower bound extends to the strongest model (qubit communication + unlimited prior entanglement). By relating the rank of the communication matrix to properties of polynomials, we are able to derive some strong bounds for exact protocols. In particular, we prove both the "log-rank conjecture" and the polynomial equivalence of quantum and classical communication complexity for various classes of functions. We also derive some weaker bounds for bounded-error quantum protocols.
On Modular Termination Proofs of General Logic Programs
Venue: arXiv cs.LO 2001
Year: 2001

We propose a modular method for proving termination of general logic programs (i.e., logic programs with negation). It is based on the notion of acceptable programs, but it allows us to prove termination in a truly modular way. We consider programs consisting of a hierarchy of modules and supply a general result for proving termination by dealing with each module separately. For programs which are in a certain sense well-behaved, namely well-moded or well-typed programs, we derive both a simple verification technique and an iterative proof method. Some examples show how our system allows for greatly simplified proofs.
Kima - an Automated Error Correction System for Concurrent Logic Programs
Venue: arXiv cs.SE 2001
Year: 2001

We have implemented Kima, an automated error correction system for concurrent logic programs. Kima corrects near-misses such as wrong variable occurrences in the absence of explicit declarations of program properties. Strong moding/typing and constraint-based analysis are turning to play fundamental roles in debugging concurrent logic programs as well as in establishing the consistency of communication protocols and data types. Mode/type analysis of Moded Flat GHC is a constraint satisfaction problem with many simple mode/type constraints, and can be solved efficiently. We proposed a simple and efficient technique which, given a non-well-moded/typed program, diagnoses the ``reasons'' of inconsistency by finding minimal inconsistent subsets of mode/type constraints. Since each constraint keeps track of the symbol occurrence in the program, a minimal subset also tells possible sources of program errors. Kima realizes automated correction by replacing symbol occurrences around the possible sources and recalculating modes and types of the rewritten programs systematically. As long as bugs are near-misses, Kima proposes a rather small number of alternatives that include an intended program.
A Knowledge-based Automated Debugger in Learning System
Venue: arXiv cs.SE 2001
Year: 2001

Currently, programming instructors continually face the problem of helping to debug students' programs. Although there currently exist a number of debuggers and debugging tools in various platforms, most of these projects or products are crafted through the needs of software maintenance, and not through the perspective of teaching of programming. Moreover, most debuggers are too general, meant for experts as well as not user-friendly. We propose a new knowledge-based automated debugger to be used as a user-friendly tool by the students to self-debug their own programs. Stereotyped code (cliche) and bugs cliche will be stored as library of plans in the knowledge-base. Recognition of correct code or bugs is based on pattern matching and constraint satisfaction. Given a syntax error-free program and its specification, this debugger called Adil (Automated Debugger in Learning system) will be able locate, pinpoint and explain logical errors of programs. If there are no errors, it will be able to explain the meaning of the program. Adil is based on the design of the Conceiver, an automated program understanding system developed at Universiti Kebangsaan Malaysia.
Generation of and Debugging with Logical Pre and Postconditions
Venue: arXiv cs.PL 2001
Year: 2001

This paper shows the debugging facilities provided by the SLAM system. The SLAM system includes i) a specification language that integrates algebraic specifications and model-based specifications using the object oriented model. Class operations are defined by using rules each of them with logical pre and postconditions but with a functional flavour. ii) A development environment that, among other features, is able to generate readable code in a high level object oriented language. iii) The generated code includes (part of) the pre and postconditions as assertions, that can be automatically checked in the debug mode execution of programs. We focus on this last aspect. The SLAM language is expressive enough to describe many useful properties and these properties are translated into a Prolog program that is linked (via an adequate interface) with the user program. The debugging execution of the program interacts with the Prolog engine which is responsible for checking properties.
GPCG: A Case Study in the Performance and Scalability of Optimization Algorithms
Venue: arXiv cs.MS 2001
Year: 2001

GPCG is an algorithm within the Toolkit for Advanced Optimization (TAO) for solving bound constrained, convex quadratic problems. Originally developed by More' and Toraldo, this algorithm was designed for large-scale problems but had been implemented only for a single processor. The TAO implementation is available for a wide range of high-performance architecture, and has been tested on up to 64 processors to solve problems with over 2.5 million variables.
Properties of Input-Consuming Derivations
Venue: arXiv cs.PL 2001
Year: 2001

We study the properties of input-consuming derivations of moded logic programs. Input-consuming derivations can be used to model the behavior of logic programs using dynamic scheduling and employing constructs such as delay declarations. We consider the class of nicely-moded programs and queries. We show that for these programs a weak version of the well-known switching lemma holds also for input-consuming derivations. Furthermore, we show that, under suitable conditions, there exists an algebraic characterization of termination of input-consuming derivations.
Tap Tips: Lightweight Discovery of Touchscreen Targets
Venue: arXiv cs.HC 2001
Year: 2001

We describe tap tips, a technique for providing touch-screen target location hints. Tap tips are lightweight in that they are non-modal, appear only when needed, require a minimal number of user gestures, and do not add to the standard touchscreen gesture vocabulary. We discuss our implementation of tap tips in an electronic guidebook system and some usability test results.
Cavity Matchings, Label Compressions, and Unrooted Evolutionary Trees
Venue: arXiv cs.CE 2001
Year: 2001

We present an algorithm for computing a maximum agreement subtree of two unrooted evolutionary trees. It takes O(n^{1.5} log n) time for trees with unbounded degrees, matching the best known time complexity for the rooted case. Our algorithm allows the input trees to be mixed trees, i.e., trees that may contain directed and undirected edges at the same time. Our algorithm adopts a recursive strategy exploiting a technique called label compression. The backbone of this technique is an algorithm that computes the maximum weight matchings over many subgraphs of a bipartite graph as fast as it takes to compute a single matching.
Total Protection of Analytic Invariant Information in Cross Tabulated Tables
Venue: arXiv cs.CR 2001
Year: 2001

To protect sensitive information in a cross tabulated table, it is a common practice to suppress some of the cells in the table. An analytic invariant is a power series in terms of the suppressed cells that has a unique feasible value and a convergence radius equal to +\infty. Intuitively, the information contained in an invariant is not protected even though the values of the suppressed cells are not disclosed. This paper gives an optimal linear-time algorithm for testing whether there exist nontrivial analytic invariants in terms of the suppressed cells in a given set of suppressed cells. This paper also presents NP-completeness results and an almost linear-time algorithm for the problem of suppressing the minimum number of cells in addition to the sensitive ones so that the resulting table does not leak analytic invariant information about a given set of suppressed cells.
A Price Dynamics in Bandwidth Markets for Point-to-point Connections
Venue: arXiv cs.NI 2001
Year: 2001

We simulate a network of N routers and M network users making concurrent point-to-point connections by buying and selling router capacity from each other. The resources need to be acquired in complete sets, but there is only one spot market for each router. In order to describe the internal dynamics of the market, we model the observed prices by N-dimensional Ito-processes. Modeling using stochastic processes is novel in this context of describing interactions between end-users in a system with shared resources, and allows a standard set of mathematical tools to be applied. The derived models can also be used to price contingent claims on network capacity and thus to price complex network services such as quality of service levels, multicast, etc.
P-Immune Sets with Holes Lack Self-Reducibility Properties
Venue: arXiv cs.CC 2001
Year: 2001

No P-immune set having exponential gaps is positive-Turing self-reducible.
An Effective Fixpoint Semantics for Linear Logic Programs
Venue: arXiv cs.PL 2001
Year: 2001

In this paper we investigate the theoretical foundation of a new bottom-up semantics for linear logic programs, and more precisely for the fragment of LinLog that consists of the language LO enriched with the constant 1. We use constraints to symbolically and finitely represent possibly infinite collections of provable goals. We define a fixpoint semantics based on a new operator in the style of Tp working over constraints. An application of the fixpoint operator can be computed algorithmically. As sufficient conditions for termination, we show that the fixpoint computation is guaranteed to converge for propositional LO. To our knowledge, this is the first attempt to define an effective fixpoint semantics for linear logic programs. As an application of our framework, we also present a formal investigation of the relations between LO and Disjunctive Logic Programming. Using an approach based on abstract interpretation, we show that DLP fixpoint semantics can be viewed as an abstraction of our semantics for LO. We prove that the resulting abstraction is correct and complete for an interesting class of LO programs encoding Petri Nets.
Flexible Software Framework for Modal Synthesis
Venue: arXiv cs.SD 2001
Year: 2001

Modal synthesis is an important area of physical modeling whose exploration in the past has been held back by a large number of control parameters, the scarcity of general-purpose design tools and the difficulty of obtaining the computational power required for real-time synthesis. This paper presents an overview of a flexible software framework facilitating the design and control of instruments based on modal synthesis. The framework is designed as a hierarchy of polymorphic synthesis objects, representing modal structures of various complexity. As a method of generalizing all interactions among the elements of a modal system, an abstract notion of {\it energy} is introduced, and a set of energy transfer functions is provided. Such abstraction leads to a design where the dynamics of interactions can be largely separated from the specifics of particular modal structures, yielding an easily configurable and expandable system. A real-time version of the framework has been implemented as a set of C++ classes along with an integrating shell and a GUI, and is currently being used to design and play modal instruments, as well as to survey fundamental properties of various modal algorithms.
Fitness Uniform Selection to Preserve Genetic Diversity
Venue: arXiv cs.AI 2001
Year: 2001

In evolutionary algorithms, the fitness of a population increases with time by mutating and recombining individuals and by a biased selection of more fit individuals. The right selection pressure is critical in ensuring sufficient optimization progress on the one hand and in preserving genetic diversity to be able to escape from local optima on the other. We propose a new selection scheme, which is uniform in the fitness values. It generates selection pressure towards sparsely populated fitness regions, not necessarily towards higher fitness, as is the case for all other selection schemes. We show that the new selection scheme can be much more effective than standard selection schemes.
Bootstrapping Structure using Similarity
Venue: arXiv cs.LG 2001
Year: 2001

In this paper a new similarity-based learning algorithm, inspired by string edit-distance (Wagner and Fischer, 1974), is applied to the problem of bootstrapping structure from scratch. The algorithm takes a corpus of unannotated sentences as input and returns a corpus of bracketed sentences. The method works on pairs of unstructured sentences or sentences partially bracketed by the algorithm that have one or more words in common. It finds parts of sentences that are interchangeable (i.e. the parts of the sentences that are different in both sentences). These parts are taken as possible constituents of the same type. While this corresponds to the basic bootstrapping step of the algorithm, further structure may be learned from comparison with other (similar) sentences. We used this method for bootstrapping structure from the flat sentences of the Penn Treebank ATIS corpus, and compared the resulting structured sentences to the structured sentences in the ATIS corpus. Similarly, the algorithm was tested on the OVIS corpus. We obtained 86.04 % non-crossing brackets precision on the ATIS corpus and 89.39 % non-crossing brackets precision on the OVIS corpus.
Evaluating Recommendation Algorithms by Graph Analysis
Venue: arXiv cs.IR 2001
Year: 2001

We present a novel framework for evaluating recommendation algorithms in terms of the `jumps' that they make to connect people to artifacts. This approach emphasizes reachability via an algorithm within the implicit graph structure underlying a recommender dataset, and serves as a complement to evaluation in terms of predictive accuracy. The framework allows us to consider questions relating algorithmic parameters to properties of the datasets. For instance, given a particular algorithm `jump,' what is the average path length from a person to an artifact? Or, what choices of minimum ratings and jumps maintain a connected graph? We illustrate the approach with a common jump called the `hammock' using movie recommender datasets.
Man [and Woman] vs. Machine: A Case Study in Base Noun Phrase Learning
Venue: arXiv cs.CL 2001
Year: 2001

A great deal of work has been done demonstrating the ability of machine learning algorithms to automatically extract linguistic knowledge from annotated corpora. Very little work has gone into quantifying the difference in ability at this task between a person and a machine. This paper is a first step in that direction.
Reverse Engineering from Assembler to Formal Specifications via Program Transformations
Venue: arXiv cs.SE 2001
Year: 2001

The FermaT transformation system, based on research carried out over the last sixteen years at Durham University, De Montfort University and Software Migrations Ltd., is an industrial-strength formal transformation engine with many applications in program comprehension and language migration. This paper is a case study which uses automated plus manually-directed transformations and abstractions to convert an IBM 370 Assembler code program into a very high-level abstract specification.
Probabilistic top-down parsing and language modeling
Venue: arXiv cs.CL 2001
Year: 2001

This paper describes the functioning of a broad-coverage probabilistic top-down parser, and its application to the problem of language modeling for speech recognition. The paper first introduces key notions in language modeling and probabilistic parsing, and briefly reviews some previous approaches to using syntactic structure for language modeling. A lexicalized probabilistic top-down parser is then presented, which performs very well, in terms of both the accuracy of returned parses and the efficiency with which they are found, relative to the best broad-coverage statistical parsers. A new language model which utilizes probabilistic top-down parsing is then outlined, and empirical results show that it improves upon previous work in test corpus perplexity. Interpolation with a trigram model yields an exceptional improvement relative to the improvement observed by other models, demonstrating the degree to which the information captured by our parsing model is orthogonal to that captured by a trigram model. A small recognition experiment also demonstrates the utility of the model.
Bounds on sample size for policy evaluation in Markov environments
Venue: arXiv cs.LG 2001
Year: 2001

Reinforcement learning means finding the optimal course of action in Markovian environments without knowledge of the environment's dynamics. Stochastic optimization algorithms used in the field rely on estimates of the value of a policy. Typically, the value of a policy is estimated from results of simulating that very policy in the environment. This approach requires a large amount of simulation as different points in the policy space are considered. In this paper, we develop value estimators that utilize data gathered when using one policy to estimate the value of using another policy, resulting in much more data-efficient algorithms. We consider the question of accumulating a sufficient experience and give PAC-style bounds.
Disjunctive Logic Programs with Inheritance
Venue: arXiv cs.LO 2001
Year: 2001

The paper proposes a new knowledge representation language, called DLP<, which extends disjunctive logic programming (with strong negation) by inheritance. The addition of inheritance enhances the knowledge modeling features of the language providing a natural representation of default reasoning with exceptions. A declarative model-theoretic semantics of DLP< is provided, which is shown to generalize the Answer Set Semantics of disjunctive logic programs. The knowledge modeling features of the language are illustrated by encoding classical nonmonotonic problems in DLP<. The complexity of DLP< is analyzed, proving that inheritance does not cause any computational overhead, as reasoning in DLP< has exactly the same complexity as reasoning in disjunctive logic programming. This is confirmed by the existence of an efficient translation from DLP< to plain disjunctive logic programming. Using this translation, an advanced KR system supporting the DLP< language has been implemented on top of the DLV system and has subsequently been integrated into DLV.
A note on radial basis function computing
Venue: arXiv cs.CE 2001
Year: 2001

This note carries three purposes involving our latest advances on the radial basis function (RBF) approach. First, we will introduce a new scheme employing the boundary knot method (BKM) to nonlinear convection-diffusion problem. It is stressed that the new scheme directly results in a linear BKM formulation of nonlinear problems by using response point-dependent RBFs, which can be solved by any linear solver. Then we only need to solve a single nonlinear algebraic equation for desirable unknown at some inner node of interest. The numerical results demonstrate high accuracy and efficiency of this nonlinear BKM strategy. Second, we extend the concepts of distance function, which include time-space and variable transformation distance functions. Finally, we demonstrate that if the nodes are symmetrically placed, the RBF coefficient matrices have either centrosymmetric or skew centrosymmetric structures. The factorization features of such matrices lead to a considerable reduction in the RBF computing effort. A simple approach is also presented to reduce the ill-conditioning of RBF interpolation matrices in general cases.