OpenRaiser/Intern-Atlas huggingface dataset:
Disjunction and modular goal-directed proof search
Venue: arXiv cs.LO 2002
Year: 2002

This paper explores goal-directed proof search in first-order multi-modal logic. The key issue is to design a proof system that respects the modularity and locality of assumptions of many modal logics. By forcing ambiguities to be considered independently, modular disjunctions in particular can be used to construct efficiently executable specifications in reasoning tasks involving partial information that otherwise might require prohibitive search. To achieve this behavior requires prior proof-theoretic justifications of logic programming to be extended, strengthened, and combined with proof-theoretic analyses of modal deduction in a novel way.
A Logical Framework for Convergent Infinite Computations
Venue: arXiv cs.LO 2002
Year: 2002

Classical computations can not capture the essence of infinite computations very well. This paper will focus on a class of infinite computations called convergent infinite computations}. A logic for convergent infinite computations is proposed by extending first order theories using Cauchy sequences, which has stronger expressive power than the first order logic. A class of fixed points characterizing the logical properties of the limits can be represented by means of infinite-length terms defined by Cauchy sequences. We will show that the limit of sequence of first order theories can be defined in terms of distance, similar to the $ε-N$ style definition of limits in real analysis. On the basis of infinitary terms, a computation model for convergent infinite computations is proposed. Finally, the interpretations of logic programs are extended by introducing real Herbrand models of logic programs and a sufficient condition for computing a real Herbrand model of Horn logic programs using convergent infinite computation is given.
Classes of Terminating Logic Programs
Venue: arXiv cs.LO 2002
Year: 2002

Termination of logic programs depends critically on the selection rule, i.e. the rule that determines which atom is selected in each resolution step. In this article, we classify programs (and queries) according to the selection rules for which they terminate. This is a survey and unified view on different approaches in the literature. For each class, we present a sufficient, for most classes even necessary, criterion for determining that a program is in that class. We study six classes: a program strongly terminates if it terminates for all selection rules; a program input terminates if it terminates for selection rules which only select atoms that are sufficiently instantiated in their input positions, so that these arguments do not get instantiated any further by the unification; a program local delay terminates if it terminates for local selection rules which only select atoms that are bounded w.r.t. an appropriate level mapping; a program left-terminates if it terminates for the usual left-to-right selection rule; a program exists-terminates if there exists a selection rule for which it terminates; finally, a program has bounded nondeterminism if it only has finitely many refutations. We propose a semantics-preserving transformation from programs with bounded nondeterminism into strongly terminating programs. Moreover, by unifying different formalisms and making appropriate assumptions, we are able to establish a formal hierarchy between the different classes.
Randomized Two-Process Wait-Free Test-and-Set
Venue: arXiv cs.DC 2002
Year: 2002

We present the first explicit, and currently simplest, randomized algorithm for 2-process wait-free test-and-set. It is implemented with two 4-valued single writer single reader atomic variables. A test-and-set takes at most 11 expected elementary steps, while a reset takes exactly 1 elementary step. Based on a finite-state analysis, the proofs of correctness and expected length are compressed into one table.
A Note on Tiling under Tomographic Constraints
Venue: arXiv cs.CC 2002
Year: 2002

Given a tiling of a 2D grid with several types of tiles, we can count for every row and column how many tiles of each type it intersects. These numbers are called the_projections_. We are interested in the problem of reconstructing a tiling which has given projections. Some simple variants of this problem, involving tiles that are 1x1 or 1x2 rectangles, have been studied in the past, and were proved to be either solvable in polynomial time or NP-complete. In this note we make progress toward a comprehensive classification of various tiling reconstruction problems, by proving NP-completeness results for several sets of tiles.
How to Commission, Operate and Maintain a Large Future Accelerator Complex from Far Remote
Venue: arXiv cs.OH 2002
Year: 2002

A study on future large accelerators [1] has considered a facility, which is designed, built and operated by a worldwide collaboration of equal partner institutions, and which is remote from most of these institutions. The full range of operation was considered including commi-ssioning, machine development, maintenance, trouble shooting and repair. Experience from existing accele-rators confirms that most of these activities are already performed 'remotely'. The large high-energy physics ex-periments and astronomy projects, already involve inter-national collaborations of distant institutions. Based on this experience, the prospects for a machine operated remotely from far sites are encouraging. Experts from each laboratory would remain at their home institution but continue to participate in the operation of the machine after construction. Experts are required to be on site only during initial commissioning and for par-ticularly difficult problems. Repairs require an on-site non-expert maintenance crew. Most of the interventions can be made without an expert and many of the rest resolved with remote assistance. There appears to be no technical obstacle to controlling an accelerator from a distance. The major challenge is to solve the complex management and communication problems.
A Tight Upper Bound on the Number of Candidate Patterns
Venue: arXiv cs.DB 2002
Year: 2002

In the context of mining for frequent patterns using the standard levelwise algorithm, the following question arises: given the current level and the current set of frequent patterns, what is the maximal number of candidate patterns that can be generated on the next level? We answer this question by providing a tight upper bound, derived from a combinatorial result from the sixties by Kruskal and Katona. Our result is useful to reduce the number of database scans.
Analysis of Non-Gaussian Nature of Network Traffic
Venue: arXiv cs.NI 2002
Year: 2002

To study mechanisms that cause the non-Gaussian nature of network traffic, we analyzed IP flow statistics. For greedy flows in particular, we investigated the hop counts between source and destination nodes, and classified applications by the port number. We found that the main flows contributing to the non-Gaussian nature of network traffic were HTTP flows with relatively small hop counts compared with the average hop counts of all flows.
On the Importance of Having an Identity or, is Consensus really Universal?
Venue: arXiv cs.DC 2002
Year: 2002

We show that Naming-- the existence of distinct IDs known to all-- is a hidden but necessary assumption of Herlihy's universality result for Consensus. We then show in a very precise sense that Naming is harder than Consensus and bring to the surface some important differences existing between popular shared memory models.
Using Tree Automata and Regular Expressions to Manipulate Hierarchically Structured Data
Venue: arXiv cs.CL 2002
Year: 2002

Information, stored or transmitted in digital form, is often structured. Individual data records are usually represented as hierarchies of their elements. Together, records form larger structures. Information processing applications have to take account of this structuring, which assigns different semantics to different data elements or records. Big variety of structural schemata in use today often requires much flexibility from applications--for example, to process information coming from different sources. To ensure application interoperability, translators are needed that can convert one structure into another. This paper puts forward a formal data model aimed at supporting hierarchical data processing in a simple and flexible way. The model is based on and extends results of two classical theories, studying finite string and tree automata. The concept of finite automata and regular languages is applied to the case of arbitrarily structured tree-like hierarchical data records, represented as "structured strings." These automata are compared with classical string and tree automata; the model is shown to be a superset of the classical models. Regular grammars and expressions over structured strings are introduced. Regular expression matching and substitution has been widely used for efficient unstructured text processing; the model described here brings the power of this proven technique to applications that deal with information trees. A simple generic alternative is offered to replace today's specialised ad-hoc approaches. The model unifies structural and content transformations, providing applications with a single data type. An example scenario of how to build applications based on this theory is discussed. Further research directions are outlined.
Software Validation using Power Profiles
Venue: arXiv cs.SE 2002
Year: 2002

The validation of modern software systems incorporates both functional and quality requirements. This paper proposes a validation approach for software quality requirement - its power consumption. This approach validates whether the software produces the desired results with a minimum expenditure of energy. We present energy requirements and an approach for their validation using a power consumption model, test-case specification, software traces, and power measurements. Three different approaches for power data gathering are described. The power consumption of mobile phone applications is obtained and matched against the power consumption model.
Approximate Computation of Reach Sets in Hybrid Systems
Venue: arXiv cs.LO 2002
Year: 2002

One of the most important problems in hybrid systems is the {\em reachability problem}. The reachability problem has been shown to be undecidable even for a subclass of {\em linear} hybrid systems. In view of this, the main focus in the area of hybrid systems has been to find {\em effective} semi-decision procedures for this problem. Such an algorithmic approach involves finding methods of computation and representation of reach sets of the continuous variables within a discrete state of a hybrid system. In this paper, after presenting a brief introduction to hybrid systems and reachability problem, we propose a computational method for obtaining the reach sets of continuous variables in a hybrid system. In addition to this, we also describe a new algorithm to over-approximate with polyhedra the reach sets of the continuous variables with linear dynamics and polyhedral initial set. We illustrate these algorithms with typical interesting examples.
Linear Programming helps solving large multi-unit combinatorial auctions
Venue: arXiv cs.GT 2002
Year: 2002

Previous works suggested the use of Branch and Bound techniques for finding the optimal allocation in (multi-unit) combinatorial auctions. They remarked that Linear Programming could provide a good upper-bound to the optimal allocation, but they went on using lighter and less tight upper-bound heuristics, on the ground that LP was too time-consuming to be used repetitively to solve large combinatorial auctions. We present the results of extensive experiments solving large (multi-unit) combinatorial auctions generated according to distributions proposed by different researchers. Our surprising conclusion is that Linear Programming is worth using. Investing almost all of one's computing time in using LP to bound from above the value of the optimal solution in order to prune aggressively pays off. We present a way to save on the number of calls to the LP routine and experimental results comparing different heuristics for choosing the bid to be considered next. Those results show that the ordering based on the square root of the size of the bids that was shown to be theoretically optimal in a previous paper by the authors performs surprisingly better than others in practice. Choosing to deal first with the bid with largest coefficient (typically 1) in the optimal solution of the relaxed LP problem, is also a good choice. The gap between the lower bound provided by greedy heuristics and the upper bound provided by LP is typically small and pruning is therefore extensive. For most distributions, auctions of a few hundred goods among a few thousand bids can be solved in practice. All experiments were run on a PC under Matlab.
Nonmonotonic Reasoning, Preferential Models and Cumulative Logics
Venue: arXiv cs.AI 2002
Year: 2002

Many systems that exhibit nonmonotonic behavior have been described and studied already in the literature. The general notion of nonmonotonic reasoning, though, has almost always been described only negatively, by the property it does not enjoy, i.e. monotonicity. We study here general patterns of nonmonotonic reasoning and try to isolate properties that could help us map the field of nonmonotonic reasoning by reference to positive properties. We concentrate on a number of families of nonmonotonic consequence relations, defined in the style of Gentzen. Both proof-theoretic and semantic points of view are developed in parallel. The former point of view was pioneered by D. Gabbay, while the latter has been advocated by Y. Shoham in. Five such families are defined and characterized by representation theorems, relating the two points of view. One of the families of interest, that of preferential relations, turns out to have been studied by E. Adams. The "preferential" models proposed here are a much stronger tool than Adams' probabilistic semantics. The basic language used in this paper is that of propositional logic. The extension of our results to first order predicate calculi and the study of the computational complexity of the decision problems described in this paper will be treated in another paper.
What does a conditional knowledge base entail?
Venue: arXiv cs.AI 2002
Year: 2002

This paper presents a logical approach to nonmonotonic reasoning based on the notion of a nonmonotonic consequence relation. A conditional knowledge base, consisting of a set of conditional assertions of the type "if ... then ...", represents the explicit defeasible knowledge an agent has about the way the world generally behaves. We look for a plausible definition of the set of all conditional assertions entailed by a conditional knowledge base. In a previous paper, S. Kraus and the authors defined and studied "preferential" consequence relations. They noticed that not all preferential relations could be considered as reasonable inference procedures. This paper studies a more restricted class of consequence relations, "rational" relations. It is argued that any reasonable nonmonotonic inference procedure should define a rational relation. It is shown that the rational relations are exactly those that may be represented by a "ranked" preferential model, or by a (non-standard) probabilistic model. The rational closure of a conditional knowledge base is defined and shown to provide an attractive answer to the question of the title. Global properties of this closure operation are proved: it is a cumulative operation. It is also computationally tractable. This paper assumes the underlying language is propositional.
A Framework for Compiling Preferences in Logic Programs
Venue: arXiv cs.AI 2002
Year: 2002

We introduce a methodology and framework for expressing general preference information in logic programming under the answer set semantics. An ordered logic program is an extended logic program in which rules are named by unique terms, and in which preferences among rules are given by a set of atoms of form s < t where s and t are names. An ordered logic program is transformed into a second, regular, extended logic program wherein the preferences are respected, in that the answer sets obtained in the transformed program correspond with the preferred answer sets of the original program. Our approach allows the specification of dynamic orderings, in which preferences can appear arbitrarily within a program. Static orderings (in which preferences are external to a logic program) are a trivial restriction of the general dynamic case. First, we develop a specific approach to reasoning with preferences, wherein the preference ordering specifies the order in which rules are to be applied. We then demonstrate the wide range of applicability of our framework by showing how other approaches, among them that of Brewka and Eiter, can be captured within our framework. Since the result of each of these transformations is an extended logic program, we can make use of existing implementations, such as dlv and smodels. To this end, we have developed a publicly available compiler as a front-end for these programming systems.
Composing Programs in a Rewriting Logic for Declarative Programming
Venue: arXiv cs.LO 2002
Year: 2002

Constructor-Based Conditional Rewriting Logic is a general framework for integrating first-order functional and logic programming which gives an algebraic semantics for non-deterministic functional-logic programs. In the context of this formalism, we introduce a simple notion of program module as an open program which can be extended together with several mechanisms to combine them. These mechanisms are based on a reduced set of operations. However, the high expressiveness of these operations enable us to model typical constructs for program modularization like hiding, export/import, genericity/instantiation, and inheritance in a simple way. We also deal with the semantic aspects of the proposal by introducing an immediate consequence operator, and studying several alternative semantics for a program module, based on this operator, in the line of logic programming: the operator itself, its least fixpoint (the least model of the module), the set of its pre-fixpoints (term models of the module), and some other variations in order to find a compositional and fully abstract semantics wrt the set of operations and a natural notion of observability.
Computational Geometry Column 43
Venue: arXiv cs.CG 2002
Year: 2002

The concept of pointed pseudo-triangulations is defined and a few of its applications described.
SPINning Parallel Systems Software
Venue: arXiv cs.LO 2002
Year: 2002

We describe our experiences in using SPIN to verify parts of the Multi Purpose Daemon (MPD) parallel process management system. MPD is a distributed collection of processes connected by Unix network sockets. MPD is dynamic: processes and connections among them are created and destroyed as MPD is initialized, runs user processes, recovers from faults, and terminates. This dynamic nature is easily expressible in the SPIN/PROMELA framework but poses performance and scalability challenges. We present here the results of expressing some of the parallel algorithms of MPD and executing both simulation and verification runs with SPIN.
Three Optimisations for Sharing
Venue: arXiv cs.PL 2002
Year: 2002

In order to improve precision and efficiency sharing analysis should track both freeness and linearity. The abstract unification algorithms for these combined domains are suboptimal, hence there is scope for improving precision. This paper proposes three optimisations for tracing sharing in combination with freeness and linearity. A novel connection between equations and sharing abstractions is used to establish correctness of these optimisations even in the presence of rational trees. A method for pruning intermediate sharing abstractions to improve efficiency is also proposed. The optimisations are lightweight and therefore some, if not all, of these optimisations will be of interest to the implementor.
Models and Tools for Collaborative Annotation
Venue: arXiv cs.CL 2002
Year: 2002

The Annotation Graph Toolkit (AGTK) is a collection of software which facilitates development of linguistic annotation tools. AGTK provides a database interface which allows applications to use a database server for persistent storage. This paper discusses various modes of collaborative annotation and how they can be supported with tools built using AGTK and its database interface. We describe the relational database schema and API, and describe a version of the TableTrans tool which supports collaborative annotation. The remainder of the paper discusses a high-level query language for annotation graphs, along with optimizations, in support of expressive and efficient access to the annotations held on a large central server. The paper demonstrates that it is straightforward to support a variety of different levels of collaborative annotation with existing AGTK-based tools, with a minimum of additional programming effort.
TableTrans, MultiTrans, InterTrans and TreeTrans: Diverse Tools Built on the Annotation Graph Toolkit
Venue: arXiv cs.CL 2002
Year: 2002

Four diverse tools built on the Annotation Graph Toolkit are described. Each tool associates linguistic codes and structures with time-series data. All are based on the same software library and tool architecture. TableTrans is for observational coding, using a spreadsheet whose rows are aligned to a signal. MultiTrans is for transcribing multi-party communicative interactions recorded using multi-channel signals. InterTrans is for creating interlinear text aligned to audio. TreeTrans is for creating and manipulating syntactic trees. This work demonstrates that the development of diverse tools and re-use of software components is greatly facilitated by a common high-level application programming interface for representing the data and managing input/output, together with a common architecture for managing the interaction of multiple components.
Exploiting Synergy Between Ontologies and Recommender Systems
Venue: arXiv cs.LG 2002
Year: 2002

Recommender systems learn about user preferences over time, automatically finding things of similar interest. This reduces the burden of creating explicit queries. Recommender systems do, however, suffer from cold-start problems where no initial information is available early on upon which to base recommendations. Semantic knowledge structures, such as ontologies, can provide valuable domain knowledge and user information. However, acquiring such knowledge and keeping it up to date is not a trivial task and user interests are particularly difficult to acquire and maintain. This paper investigates the synergy between a web-based research paper recommender system and an ontology containing information automatically extracted from departmental databases available on the web. The ontology is used to address the recommender systems cold-start problem. The recommender system addresses the ontology's interest-acquisition problem. An empirical evaluation of this approach is conducted and the performance of the integrated systems measured.