OpenRaiser/Intern-Atlas huggingface dataset:
Computation in an algebra of test selection criteria
Venue: arXiv cs.SE 1999
Year: 1999

One of the key concepts in testing is that of adequate test sets. A test selection criterion decides which test sets are adequate. In this paper, a language schema for specifying a large class of test selection criteria is developed; the schema is based on two operations for building complex criteria from simple ones. Basic algebraic properties of the two operations are derived. In the second part of the paper, a simple language-an instance of the general schema-is studied in detail, with the goal of generating small adequate test sets automatically. It is shown that one version of the problem is intractable, while another is solvable by an efficient algorithm. An implementation of the algorithm is described.
Effect of different packet sizes on RED performance
Venue: arXiv cs.NI 2000
Year: 2000

We consider the adaptation of random early detection (RED) as an active queue management algorithm for TCP traffic in Internet gateways where different maximum transfer units (MTUs) are used. We studied the two existing RED variants and point out a weakness in both. The first variant where the drop probability is independent from the packet size discriminates connections with smaller MTUs. The second variant results in a very high Packet Loss Ratio (PLR), and as a consequence low goodput, for connections with higher MTUs. We show that fairness in terms of loss and goodput can be supplied through an appropriate setting of the RED algorithm.
RED behavior with different packet sizes
Venue: arXiv cs.NI 2000
Year: 2000

We consider the adaptation of random early detection (RED) as a buffer management algorithm for TCP traffic in Internet gateways where different maximum transfer units (MTUs) are used. We studied the two RED variants described in [4] and point out a weakness in both. The first variant where drop probability is independent from the packet size discriminates connections with smaller MTUs. The second variant results in a very high packet loss ratio (PLR), and as a consequence low goodput, for connections with higher MTUs. We show that fairness in terms of loss and goodput can be supplied through an appropriate setting of the RED algorithm.
Multi-Agent Only Knowing
Venue: arXiv cs.AI 2000
Year: 2000

Levesque introduced a notion of ``only knowing'', with the goal of capturing certain types of nonmonotonic reasoning. Levesque's logic dealt with only the case of a single agent. Recently, both Halpern and Lakemeyer independently attempted to extend Levesque's logic to the multi-agent case. Although there are a number of similarities in their approaches, there are some significant differences. In this paper, we reexamine the notion of only knowing, going back to first principles. In the process, we simplify Levesque's completeness proof, and point out some problems with the earlier definitions. This leads us to reconsider what the properties of only knowing ought to be. We provide an axiom system that captures our desiderata, and show that it has a semantics that corresponds to it. The axiom system has an added feature of interest: it includes a modal operator for satisfiability, and thus provides a complete axiomatization for satisfiability in the logic K45.
Take-home Complexity
Venue: arXiv cs.CY 2000
Year: 2000

We discuss the use of projects in first-year graduate complexity theory courses.
PushPush is NP-hard in 2D
Venue: arXiv cs.CG 2000
Year: 2000

We prove that a particular pushing-blocks puzzle is intractable in 2D, improving an earlier result that established intractability in 3D [OS99]. 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 2D by reduction from SAT.
Computing large and small stable models
Venue: arXiv cs.LO 2000
Year: 2000

In this paper, we focus on the problem of existence and computing of small and large stable models. We show that for every fixed integer k, there is a linear-time algorithm to decide the problem LSM (large stable models problem): does a logic program P have a stable model of size at least |P|-k. In contrast, we show that the problem SSM (small stable models problem) to decide whether a logic program P has a stable model of size at most k is much harder. We present two algorithms for this problem but their running time is given by polynomials of order depending on k. We show that the problem SSM is fixed-parameter intractable by demonstrating that it is W[2]-hard. This result implies that it is unlikely, an algorithm exists to compute stable models of size at most k that would run in time O(n^c), where c is a constant independent of k. We also provide an upper bound on the fixed-parameter complexity of the problem SSM by showing that it belongs to the class W[3].
On The Closest String and Substring Problems
Venue: arXiv cs.CE 2000
Year: 2000

The problem of finding a center string that is `close' to every given string arises and has many applications in computational biology and coding theory. This problem has two versions: the Closest String problem and the Closest Substring problem. Assume that we are given a set of strings ${\cal S}=\{s_1, s_2, ..., s_n\}$ of strings, say, each of length $m$. The Closest String problem asks for the smallest $d$ and a string $s$ of length $m$ which is within Hamming distance $d$ to each $s_i\in {\cal S}$. This problem comes from coding theory when we are looking for a code not too far away from a given set of codes. The problem is NP-hard. Berman et al give a polynomial time algorithm for constant $d$. For super-logarithmic $d$, Ben-Dor et al give an efficient approximation algorithm using linear program relaxation technique. The best polynomial time approximation has ratio 4/3 for all $d$ given by Lanctot et al and Gasieniec et al. The Closest Substring problem looks for a string $t$ which is within Hamming distance $d$ away from a substring of each $s_i$. This problem only has a $2- \frac{2}{2|Σ|+1}$ approximation algorithm previously Lanctot et al and is much more elusive than the Closest String problem, but it has many applications in finding conserved regions, genetic drug target identification, and genetic probes in molecular biology. Whether there are efficient approximation algorithms for both problems are major open questions in this area. We present two polynomial time approxmation algorithms with approximation ratio $1+ ε$ for any small $ε$ to settle both questions.
Defeasible Reasoning in OSCAR
Venue: arXiv cs.AI 2000
Year: 2000

This is a system description for the OSCAR defeasible reasoner.
Abductive and Consistency-Based Diagnosis Revisited: a Modeling Perspective
Venue: arXiv cs.AI 2000
Year: 2000

Diagnostic reasoning has been characterized logically as consistency-based reasoning or abductive reasoning. Previous analyses in the literature have shown, on the one hand, that choosing the (in general more restrictive) abductive definition may be appropriate or not, depending on the content of the knowledge base [Console&Torasso91], and, on the other hand, that, depending on the choice of the definition the same knowledge should be expressed in different form [Poole94]. Since in Model-Based Diagnosis a major problem is finding the right way of abstracting the behavior of the system to be modeled, this paper discusses the relation between modeling, and in particular abstraction in the model, and the notion of diagnosis.
Description of GADEL
Venue: arXiv cs.AI 2000
Year: 2000

This article describes the first implementation of the GADEL system : a Genetic Algorithm for Default Logic. The goal of GADEL is to compute extensions in Reiter's default logic. It accepts every kind of finite propositional default theories and is based on evolutionary principles of Genetic Algorithms. Its first experimental results on certain instances of the problem show that this new approach of the problem can be successful.
Extending Classical Logic with Inductive Definitions
Venue: arXiv cs.LO 2000
Year: 2000

The goal of this paper is to extend classical logic with a generalized notion of inductive definition supporting positive and negative induction, to investigate the properties of this logic, its relationships to other logics in the area of non-monotonic reasoning, logic programming and deductive databases, and to show its application for knowledge representation by giving a typology of definitional knowledge.
SLDNFA-system
Venue: arXiv cs.AI 2000
Year: 2000

The SLDNFA-system results from the LP+ project at the K.U.Leuven, which investigates logics and proof procedures for these logics for declarative knowledge representation. Within this project inductive definition logic (ID-logic) is used as representation logic. Different solvers are being developed for this logic and one of these is SLDNFA. A prototype of the system is available and used for investigating how to solve efficiently problems represented in ID-logic.
QUIP - A Tool for Computing Nonmonotonic Reasoning Tasks
Venue: arXiv cs.AI 2000
Year: 2000

In this paper, we outline the prototype of an automated inference tool, called QUIP, which provides a uniform implementation for several nonmonotonic reasoning formalisms. The theoretical basis of QUIP is derived from well-known results about the computational complexity of nonmonotonic logics and exploits a representation of the different reasoning tasks in terms of quantified boolean formulae.
Automatic Classification of Text Databases through Query Probing
Venue: arXiv cs.DB 2000
Year: 2000

Many text databases on the web are "hidden" behind search interfaces, and their documents are only accessible through querying. Search engines typically ignore the contents of such search-only databases. Recently, Yahoo-like directories have started to manually organize these databases into categories that users can browse to find these valuable resources. We propose a novel strategy to automate the classification of search-only text databases. Our technique starts by training a rule-based document classifier, and then uses the classifier's rules to generate probing queries. The queries are sent to the text databases, which are then classified based on the number of matches that they produce for each query. We report some initial exploratory experiments that show that our approach is promising to automatically characterize the contents of text databases accessible on the web.
Termination Proofs for Logic Programs with Tabling
Venue: arXiv cs.LO 2000
Year: 2000

Tabled logic programming is receiving increasing attention in the Logic Programming community. It avoids many of the shortcomings of SLD execution and provides a more flexible and often extremely efficient execution mechanism for logic programs. In particular, tabled execution of logic programs terminates more often than execution based on SLD-resolution. In this article, we introduce two notions of universal termination of logic programming with Tabling: quasi-termination and (the stronger notion of) LG-termination. We present sufficient conditions for these two notions of termination, namely quasi-acceptability and LG-acceptability, and we show that these conditions are also necessary in case the tabling is well-chosen. Starting from these conditions, we give modular termination proofs, i.e., proofs capable of combining termination proofs of separate programs to obtain termination proofs of combined programs. Finally, in the presence of mode information, we state sufficient conditions which form the basis for automatically proving termination in a constraint-based way.
dcs: An Implementation of DATALOG with Constraints
Venue: arXiv cs.AI 2000
Year: 2000

Answer-set programming (ASP) has emerged recently as a viable programming paradigm. We describe here an ASP system, DATALOG with constraints or DC, based on non-monotonic logic. Informally, DC theories consist of propositional clauses (constraints) and of Horn rules. The semantics is a simple and natural extension of the semantics of the propositional logic. However, thanks to the presence of Horn rules in the system, modeling of transitive closure becomes straightforward. We describe the syntax, use and implementation of DC and provide experimental results.
A Polyvariant Binding-Time Analysis for Off-line Partial Deduction
Venue: arXiv cs.PL 2000
Year: 2000

We study the notion of binding-time analysis for logic programs. We formalise the unfolding aspect of an on-line partial deduction system as a Prolog program. Using abstract interpretation, we collect information about the run-time behaviour of the program. We use this information to make the control decisions about the unfolding at analysis time and to turn the on-line system into an off-line system. We report on some initial experiments.
Deciding first-order properties of locally tree-decomposable structures
Venue: arXiv cs.DS 2000
Year: 2000

We introduce the concept of a class of graphs, or more generally, relational structures, being locally tree-decomposable. There are numerous examples of locally tree-decomposable classes, among them the class of planar graphs and all classes of bounded valence or of bounded tree-width. We also consider a slightly more general concept of a class of structures having bounded local tree-width. We show that for each property P of structures that is definable in first-order logic and for each locally tree-decomposable class C of graphs, there is a linear time algorithm deciding whether a given structure A in C has property P. For classes C of bounded local tree-width, we show that for every k\ge 1 there is an algorithm that solves the same problem in time O(n^{1+(1/k)}) (where n is the cardinality of the input structure).
On the Scalability of the Answer Extraction System "ExtrAns"
Venue: arXiv cs.CL 2000
Year: 2000

This paper reports on the scalability of the answer extraction system ExtrAns. An answer extraction system locates the exact phrases in the documents that contain the explicit answers to the user queries. Answer extraction systems are therefore more convenient than document retrieval systems in situations where the user wants to find specific information in limited time. ExtrAns performs answer extraction over UNIX manpages. It has been constructed by combining available linguistic resources and implementing only a few modules from scratch. A resolution procedure between the minimal logical form of the user query and the minimal logical forms of the manpage sentences finds the answers to the queries. These answers are displayed to the user, together with pointers to the respective manpages, and the exact phrases that contribute to the answer are highlighted. This paper shows that the increase in response times is not a big issue when scaling the system up from 30 to 500 documents, and that the response times for 500 documents are still acceptable for a real-time answer extraction system.
The SAT Phase Transition
Venue: arXiv cs.AI 2000
Year: 2000

Phase transition is an important feature of SAT problem. For random k-SAT model, it is proved that as r (ratio of clauses to variables) increases, the structure of solutions will undergo a sudden change like satisfiability phase transition when r reaches a threshold point. This phenomenon shows that the satisfying truth assignments suddenly shift from being relatively different from each other to being very similar to each other.
Multimethods and separate static typechecking in a language with C++-like object model
Venue: arXiv cs.PL 2000
Year: 2000

The goal of this paper is the description and analysis of multimethod implementation in a new object-oriented, class-based programming language called OOLANG. The implementation of the multimethod typecheck and selection, deeply analyzed in the paper, is performed in two phases in order to allow static typechecking and separate compilation of modules. The first phase is performed at compile time, while the second is executed at link time and does not require the modules' source code. OOLANG has syntax similar to C++; the main differences are the absence of pointers and the realization of polymorphism through subsumption. It adopts the C++ object model and supports multiple inheritance as well as virtual base classes. For this reason, it has been necessary to define techniques for realigning argument and return value addresses when performing multimethod invocations.
Light Affine Logic (Proof Nets, Programming Notation, P-Time Correctness and Completeness)
Venue: arXiv cs.LO 2000
Year: 2000

This paper is a structured introduction to Light Affine Logic, and to its intuitionistic fragment. Light Affine Logic has a polynomially costing cut elimination (P-Time correctness), and encodes all P-Time Turing machines (P-Time completeness). P-Time correctness is proved by introducing the Proof nets for Intuitionistic Light Affine Logic. P-Time completeness is demonstrated in full details thanks to a very compact program notation. On one side, the proof of P-Time correctness describes how the complexity of cut elimination is controlled, thanks to a suitable cut elimination strategy that exploits structural properties of the Proof nets. This allows to have a good catch on the meaning of the ``paragraph'' modality, which is a peculiarity of light logics. On the other side, the proof of P-Time completeness, together with a lot of programming examples, gives a flavor of the non trivial task of programming with resource limitations, using Intuitionistic Light Affine Logic derivations as programs.
UNIX Resource Managers: Capacity Planning and Resource Issues
Venue: arXiv cs.PF 2000
Year: 2000

The latest implementations of commercial UNIX to offer mainframe style capacity management on enterprise servers include: AIX Workload Manager (WLM), HP-UX Process Resource Manager (PRM), Solaris Resource Manager (SRM), as well as SGI and Compaq. The ability to manage server capacity is achieved by making significant modifications to the standard UNIX operating system so that processes are inherently tied to specific users. Those users, in turn, are granted only a certain fraction of system resources. Resource usage is monitored and compared with each users grant to ensure that the assigned entitlement constraints are met. In this paper, we begin by clearing up some of the confusion that has surrounded the motivation and the terminology behind the new technology. The common theme across each of the commercial implementations is the introduction of the fair-share scheduler. After reviewing some potential performance pitfalls, we present capacity planning guidelines for migrating to automated UNIX resource management.
Turning Speech Into Scripts
Venue: arXiv cs.CL 2000
Year: 2000

We describe an architecture for implementing spoken natural language dialogue interfaces to semi-autonomous systems, in which the central idea is to transform the input speech signal through successive levels of representation corresponding roughly to linguistic knowledge, dialogue knowledge, and domain knowledge. The final representation is an executable program in a simple scripting language equivalent to a subset of Cshell. At each stage of the translation process, an input is transformed into an output, producing as a byproduct a "meta-output" which describes the nature of the transformation performed. We show how consistent use of the output/meta-output distinction permits a simple and perspicuous treatment of apparently diverse topics including resolution of pronouns, correction of user misconceptions, and optimization of scripts. The methods described have been concretely realized in a prototype speech interface to a simulation of the Personal Satellite Assistant.
Multicast-based Architecture for IP Mobility: Simulation Analysis and Comparison with Basic Mobile IP
Venue: arXiv cs.NI 2000
Year: 2000

With the introduction of a newer generation of wireless devices and technologies, the need for an efficient architecture for IP mobility is becoming more apparent. Several architectures have been proposed to support IP mobility. Most studies, however, show that current architectures, in general, fall short from satisfying the performance requirements for wireless applications, mainly audio. Other studies have shown performance improvement by using multicast to reduce latency and packet loss during handoff. In this study, we propose a multicast-based architecture to support IP mobility. We evaluate our approach through simulation, and we compare it to mainstream approaches for IP mobility, mainly, the Mobile IP protocol. Comparison is performed according to the required performance criteria, such as smooth handoff and efficient routing. Our simulation results show significant improvement for the proposed architecture. On average, basic Mobile IP consumes almost twice as much network bandwidth, and experiences more than twice as much end-to-end and handoff delays, as does our proposed architecture. Furthermore, we propose an extension to Mobile IP to support our architecture with minimal modification.
Online Correction of Dispersion Error in 2D Waveguide Meshes
Venue: arXiv cs.SD 2000
Year: 2000

An elastic ideal 2D propagation medium, i.e., a membrane, can be simulated by models discretizing the wave equation on the time-space grid (finite difference methods), or locally discretizing the solution of the wave equation (waveguide meshes). The two approaches provide equivalent computational structures, and introduce numerical dispersion that induces a misalignment of the modes from their theoretical positions. Prior literature shows that dispersion can be arbitrarily reduced by oversizing and oversampling the mesh, or by adpting offline warping techniques. In this paper we propose to reduce numerical dispersion by embedding warping elements, i.e., properly tuned allpass filters, in the structure. The resulting model exhibits a significant reduction in dispersion, and requires less computational resources than a regular mesh structure having comparable accuracy.
Using a Diathesis Model for Semantic Parsing
Venue: arXiv cs.CL 2000
Year: 2000

This paper presents a semantic parsing approach for unrestricted texts. Semantic parsing is one of the major bottlenecks of Natural Language Understanding (NLU) systems and usually requires building expensive resources not easily portable to other domains. Our approach obtains a case-role analysis, in which the semantic roles of the verb are identified. In order to cover all the possible syntactic realisations of a verb, our system combines their argument structure with a set of general semantic labelled diatheses models. Combining them, the system builds a set of syntactic-semantic patterns with their own role-case representation. Once the patterns are build, we use an approximate tree pattern-matching algorithm to identify the most reliable pattern for a sentence. The pattern matching is performed between the syntactic-semantic patterns and the feature-structure tree representing the morphological, syntactical and semantic information of the analysed sentence. For sentences assigned to the correct model, the semantic parsing system we are presenting identifies correctly more than 73% of possible semantic case-roles.
Constraint compiling into rules formalism constraint compiling into rules formalism for dynamic CSPs computing
Venue: arXiv cs.AI 2000
Year: 2000

In this paper we present a rule based formalism for filtering variables domains of constraints. This formalism is well adapted for solving dynamic CSP. We take diagnosis as an instance problem to illustrate the use of these rules. A diagnosis problem is seen like finding all the minimal sets of constraints to be relaxed in the constraint network that models the device to be diagnosed