OpenRaiser/Intern-Atlas huggingface dataset:
A Logic for SDSI's Linked Local Name Spaces
Venue: arXiv cs.CR 2000
Year: 2000

Abadi has introduced a logic to explicate the meaning of local names in SDSI, the Simple Distributed Security Infrastructure proposed by Rivest and Lampson. Abadi's logic does not correspond precisely to SDSI, however; it draws conclusions about local names that do not follow from SDSI's name resolution algorithm. Moreover, its semantics is somewhat unintuitive. This paper presents the Logic of Local Name Containment, which does not suffer from these deficiencies. It has a clear semantics and provides a tight characterization of SDSI name resolution. The semantics is shown to be closely related to that of logic programs, leading to an approach to the efficient implementation of queries concerning local names. A complete axiomatization of the logic is also provided.
Multiplicative Nonholonomic/Newton -like Algorithm
Venue: arXiv cs.LG 2000
Year: 2000

We construct new algorithms from scratch, which use the fourth order cumulant of stochastic variables for the cost function. The multiplicative updating rule here constructed is natural from the homogeneous nature of the Lie group and has numerous merits for the rigorous treatment of the dynamics. As one consequence, the second order convergence is shown. For the cost function, functions invariant under the componentwise scaling are choosen. By identifying points which can be transformed to each other by the scaling, we assume that the dynamics is in a coset space. In our method, a point can move toward any direction in this coset. Thus, no prewhitening is required.
An Internet Multicast System for the Stock Market
Venue: arXiv cs.NI 2000
Year: 2000

We are moving toward a distributed, international, twenty-four hour, electronic stock exchange. The exchange will use the global Internet, or internet technology. This system is a natural application of multicast because there are a large number of receivers that should receive the same information simultaneously. The data requirements for the stock exchange are discussed. The current multicast protocols lack the reliability, fairness, and scalability needed in this application. We describe a distributed architecture together with a reliable multicast protocol, a modification of the RMP protocol, that has characteristics appropriate for this application. The architecture is used in three applications: In the first, we construct a unified stock ticker of the transactions that are being conducted on the various physical and electronic exchanges. Our objective is to deliver the the same combined ticker reliably and simultaneously to all receivers, anywhere in the world. In the second, we construct a unified sequence of buy and sell offers that are delivered to a single exchange or a collection of exchanges. Our objective is to give all traders the same fair access to an exchange independent of their relative distances to the exchange or the loss characteristics of the international network. In the third, we construct a distributed, electronic trading floor that can replace the current exchanges. This application uses the innovations from the first two applications to combine their fairness attributes.
Computing Circumscriptive Databases by Integer Programming: Revisited (Extended Abstract)
Venue: arXiv cs.AI 2000
Year: 2000

In this paper, we consider a method of computing minimal models in circumscription using integer programming in propositional logic and first-order logic with domain closure axioms and unique name axioms. This kind of treatment is very important since this enable to apply various technique developed in operations research to nonmonotonic reasoning. Nerode et al. (1995) are the first to propose a method of computing circumscription using integer programming. They claimed their method was correct for circumscription with fixed predicate, but we show that their method does not correctly reflect their claim. We show a correct method of computing all the minimal models not only with fixed predicates but also with varied predicates and we extend our method to compute prioritized circumscription as well.
Conditional indifference and conditional preservation
Venue: arXiv cs.AI 2000
Year: 2000

The idea of preserving conditional beliefs emerged recently as a new paradigm apt to guide the revision of epistemic states. Conditionals are substantially different from propositional beliefs and need specific treatment. In this paper, we present a new approach to conditionals, capturing particularly well their dynamic part as revision policies. We thoroughly axiomatize a principle of conditional preservation as an indifference property with respect to conditional structures of worlds. This principle is developed in a semi-quantitative setting, so as to reveal its fundamental meaning for belief revision in quantitative as well as in qualitative frameworks. In fact, it is shown to cover other proposed approaches to conditional preservation.
Hypothetical revision and matter-of-fact supposition
Venue: arXiv cs.AI 2000
Year: 2000

The paper studies the notion of supposition encoded in non-Archimedean conditional probability (and revealed in the acceptance of the so-called indicative conditionals). The notion of qualitative change of view that thus arises is axiomatized and compared with standard notions like AGM and UPDATE. Applications in the following fields are discussed: (1) theory of games and decisions, (2) causal models, (3) non-monotonic logic.
A Compiler for Ordered Logic Programs
Venue: arXiv cs.AI 2000
Year: 2000

This paper describes a system, called PLP, for compiling ordered logic programs into standard logic programs under the answer set semantics. In an ordered logic program, rules are named by unique terms, and preferences among rules are given by a set of dedicated atoms. 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 theory correspond with the preferred answer sets of the original theory. Since the result of the translation is an extended logic program, existing logic programming systems can be used as underlying reasoning engine. In particular, PLP is conceived as a front-end to the logic programming systems dlv and smodels.
Logic Programs with Compiled Preferences
Venue: arXiv cs.AI 2000
Year: 2000

We describe an approach for compiling preferences into logic programs 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 dedicated atoms. 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 theory correspond with the preferred answer sets of the original theory. Our approach allows both the specification of static orderings (as found in most previous work), in which preferences are external to a logic program, as well as orderings on sets of rules. In large part then, we are interested in describing a general methodology for uniformly incorporating preference information in a logic program. Since the result of our translation is an extended logic program, we can make use of existing implementations, such as dlv and smodels. To this end, we have developed a compiler, available on the web, as a front-end for these programming systems.
DLV - A System for Declarative Problem Solving
Venue: arXiv cs.AI 2000
Year: 2000

DLV is an efficient logic programming and non-monotonic reasoning (LPNMR) system with advanced knowledge representation mechanisms and interfaces to classic relational database systems. Its core language is disjunctive datalog (function-free disjunctive logic programming) under the Answer Set Semantics with integrity constraints, both default and strong (or explicit) negation, and queries. Integer arithmetics and various built-in predicates are also supported. In addition DLV has several frontends, namely brave and cautious reasoning, abductive diagnosis, consistency-based diagnosis, a subset of SQL3, planning with action languages, and logic programming with inheritance.
Implementing Integrity Constraints in an Existing Belief Revision System
Venue: arXiv cs.AI 2000
Year: 2000

SNePS is a mature knowledge representation, reasoning, and acting system that has long contained a belief revision subsystem, called SNeBR. SNeBR is triggered when an explicit contradiction is introduced into the SNePS belief space, either because of a user's new assertion, or because of a user's query. SNeBR then makes the user decide what belief to remove from the belief space in order to restore consistency, although it provides information to help the user in making that decision. We have recently added automatic belief revision to SNeBR, by which, under certain circumstances, SNeBR decides by itself which belief to remove, and then informs the user of the decision and its consequences. We have used the well-known belief revision integrity constraints as a guide in designing automatic belief revision, taking into account, however, that SNePS's belief space is not deductively closed, and that it would be infeasible to form the deductive closure in order to decide what belief to remove. This paper briefly describes SNeBR both before and after this revision, discusses how we adapted the integrity constraints for this purpose, and gives an example of the new SNeBR in action.
Planning with Incomplete Information
Venue: arXiv cs.AI 2000
Year: 2000

Planning is a natural domain of application for frameworks of reasoning about actions and change. In this paper we study how one such framework, the Language E, can form the basis for planning under (possibly) incomplete information. We define two types of plans: weak and safe plans, and propose a planner, called the E-Planner, which is often able to extend an initial weak plan into a safe plan even though the (explicit) information available is incomplete, e.g. for cases where the initial state is not completely known. The E-Planner is based upon a reformulation of the Language E in argumentation terms and a natural proof theory resulting from the reformulation. It uses an extension of this proof theory by means of abduction for the generation of plans and adopts argumentation-based techniques for extending weak plans into safe plans. We provide representative examples illustrating the behaviour of the E-Planner, in particular for cases where the status of fluents is incompletely known.
Security of the Cao-Li Public Key Cryptosystem
Venue: arXiv cs.CR 2000
Year: 2000

We show that the Cao-Li cryptosystem proposed in \cite{CL1} is not secure. Its private key can be reconstructed from its public key using elementary means such as LU-decomposition and Euclidean algorithm.
Specifying and Implementing Security Policies Using LaSCO, the Language for Security Constraints on Objects
Venue: arXiv cs.CR 2000
Year: 2000

In this dissertation, we present LaSCO, the Language for Security Constraints on Objects, a new approach to expressing security policies using policy graphs and present a method for enforcing policies so expressed. Other approaches for stating security policies fall short of what is desirable with respect to either policy clarity, executability, or the precision with which a policy may be expressed. However, LaSCO is designed to have those three desirable properties of a security policy language as well as: relevance for many different systems, statement of policies at an appropriate level of detail, user friendliness for both casual and expert users, and amenability to formal reasoning. In LaSCO, the constraints of a policy are stated as directed graphs annotated with expressions describing the situation under which the policy applies and what the requirement is. LaSCO may be used for such diverse applications as executing programs, file systems, operating systems, distributed systems, and networks. Formal operational semantics have been defined for LaSCO. An architecture for implementing LaSCO on any system, is presented along with an implementation of the system-independent portion in Perl. Using this, we have implemented LaSCO for Java programs, preventing Java programs from violating policy. A GUI to facilitate writing policies is provided. We have studied applying LaSCO to a network as viewed by GrIDS, a distributed intrusion detection system for large networks, and propose a design. We conclude that LaSCO has characteristics that enable its use on different types of systems throughout the process of precisely expressing a policy, understanding the implications of a policy, and implementing it on a system.
Detecting Unsolvable Queries for Definite Logic Programs
Venue: arXiv cs.LO 2000
Year: 2000

In solving a query, the SLD proof procedure for definite programs sometimes searches an infinite space for a non existing solution. For example, querying a planner for an unreachable goal state. Such programs motivate the development of methods to prove the absence of a solution. Considering the definite program and the query ``<- Q'' as clauses of a first order theory, one can apply model generators which search for a finite interpretation in which the program clauses as well as the clause ``false <- Q'' are true. This paper develops a new approach which exploits the fact that all clauses are definite. It is based on a goal directed abductive search in the space of finite pre-interpretations for a pre-interpretation such that ``Q'' is false in the least model of the program based on it. Several methods for efficiently searching the space of pre-interpretations are presented. Experimental results confirm that our approach find solutions with less search than with the use of a first order model generator.
On the theory of system administration
Venue: arXiv cs.OH 2000
Year: 2000

This paper describes necessary elements for constructing theoretical models of network and system administration. Armed with a theoretical model it becomes possible to determine best practices and optimal strategies in a way which objectively relates policies and assumptions to results obtained. It is concluded that a mixture of automation and human, or other intelligent incursion is required to fully implement system policy with current technology. Some aspects of the author's immunity model for automated system administration are explained, as an example. A theoretical framework makes the prediction that the optimal balance between resource availability and garbage collection strategies is encompassed by the immunity model.
Searching for Spaceships
Venue: arXiv cs.AI 2000
Year: 2000

We describe software that searches for spaceships in Conway's Game of Life and related two-dimensional cellular automata. Our program searches through a state space related to the de Bruijn graph of the automaton, using a method that combines features of breadth first and iterative deepening search, and includes fast bit-parallel graph reachability and path enumeration algorithms for finding the successors of each state. Successful results include a new 2c/7 spaceship in Life, found by searching a space with 2^126 states.
How to Evaluate your Question Answering System Every Day and Still Get Real Work Done
Venue: arXiv cs.CL 2000
Year: 2000

In this paper, we report on Qaviar, an experimental automated evaluation system for question answering applications. The goal of our research was to find an automatically calculated measure that correlates well with human judges' assessment of answer correctness in the context of question answering tasks. Qaviar judges the response by computing recall against the stemmed content words in the human-generated answer key. It counts the answer correct if it exceeds agiven recall threshold. We determined that the answer correctness predicted by Qaviar agreed with the human 93% to 95% of the time. 41 question-answering systems were ranked by both Qaviar and human assessors, and these rankings correlated with a Kendall's Tau measure of 0.920, compared to a correlation of 0.956 between human assessors on the same data.
Design and Evaluation of Mechanisms for a Multicomputer Object Store
Venue: arXiv cs.DC 2000
Year: 2000

Multicomputers have traditionally been viewed as powerful compute engines. It is from this perspective that they have been applied to various problems in order to achieve significant performance gains. There are many applications for which this compute intensive approach is only a partial solution. CAD, virtual reality, simulation, document management and analysis all require timely access to large amounts of data. This thesis investigates the use of the object store paradigm to harness the large distributed memories found on multicomputers. The design, implementation, and evaluation of a distributed object server on the Fujitsu AP1000 is described. The performance of the distributed object server under example applications, mainly physical simulation problems, is used to evaluate solutions to the problems of client space recovery, object migration, and coherence maintenance. The distributed object server follows the client-server model, allows object replication, and uses binary semaphores as a concurrency control measure. Instrumentation of the server under these applications supports several conclusions: client space recovery should be dynamically controlled by the application, predictively prefetching object replicas yields benefits in restricted circumstances, object migration by storage unit (segment) is not generally suitable where there are many objects per storage unit, and binary semaphores are an expensive concurrency control measure in this environment.
Application Software, Domain-Specific Languages, and Language Design Assistants
Venue: arXiv cs.PL 2000
Year: 2000

While application software does the real work, domain-specific languages (DSLs) are tools to help produce it efficiently, and language design assistants in turn are meta-tools to help produce DSLs quickly. DSLs are already in wide use (HTML for web pages, Excel macros for spreadsheet applications, VHDL for hardware design, ...), but many more will be needed for both new as well as existing application domains. Language design assistants to help develop them currently exist only in the basic form of language development systems. After a quick look at domain-specific languages, and especially their relationship to application libraries, we survey existing language development systems and give an outline of future language design assistants.
Connectivity Compression for Irregular Quadrilateral Meshes
Venue: arXiv cs.GR 2000
Year: 2000

Applications that require Internet access to remote 3D datasets are often limited by the storage costs of 3D models. Several compression methods are available to address these limits for objects represented by triangle meshes. Many CAD and VRML models, however, are represented as quadrilateral meshes or mixed triangle/quadrilateral meshes, and these models may also require compression. We present an algorithm for encoding the connectivity of such quadrilateral meshes, and we demonstrate that by preserving and exploiting the original quad structure, our approach achieves encodings 30 - 80% smaller than an approach based on randomly splitting quads into triangles. We present both a code with a proven worst-case cost of 3 bits per vertex (or 2.75 bits per vertex for meshes without valence-two vertices) and entropy-coding results for typical meshes ranging from 0.3 to 0.9 bits per vertex, depending on the regularity of the mesh. Our method may be implemented by a rule for a particular splitting of quads into triangles and by using the compression and decompression algorithms introduced in [Rossignac99] and [Rossignac&Szymczak99]. We also present extensions to the algorithm to compress meshes with holes and handles and meshes containing triangles and other polygons as well as quads.
A Denotational Semantics for First-Order Logic
Venue: arXiv cs.PL 2000
Year: 2000

In Apt and Bezem [AB99] (see cs.LO/9811017) we provided a computational interpretation of first-order formulas over arbitrary interpretations. Here we complement this work by introducing a denotational semantics for first-order logic. Additionally, by allowing an assignment of a non-ground term to a variable we introduce in this framework logical variables. The semantics combines a number of well-known ideas from the areas of semantics of imperative programming languages and logic programming. In the resulting computational view conjunction corresponds to sequential composition, disjunction to ``don't know'' nondeterminism, existential quantification to declaration of a local variable, and negation to the ``negation as finite failure'' rule. The soundness result shows correctness of the semantics with respect to the notion of truth. The proof resembles in some aspects the proof of the soundness of the SLDNF-resolution.
Practical Reasoning for Expressive Description Logics
Venue: arXiv cs.LO 2000
Year: 2000

Description Logics (DLs) are a family of knowledge representation formalisms mainly characterised by constructors to build complex concepts and roles from atomic ones. Expressive role constructors are important in many applications, but can be computationally problematical. We present an algorithm that decides satisfiability of the DL ALC extended with transitive and inverse roles, role hierarchies, and qualifying number restrictions. Early experiments indicate that this algorithm is well-suited for implementation. Additionally, we show that ALC extended with just transitive and inverse roles is still in PSPACE. Finally, we investigate the limits of decidability for this family of DLs.
Centroid-based summarization of multiple documents: sentence extraction, utility-based evaluation, and user studies
Venue: arXiv cs.CL 2000
Year: 2000

We present a multi-document summarizer, called MEAD, which generates summaries using cluster centroids produced by a topic detection and tracking system. We also describe two new techniques, based on sentence utility and subsumption, which we have applied to the evaluation of both single and multiple document summaries. Finally, we describe two user studies that test our models of multi-document summarization.
C++ programming language for an abstract massively parallel SIMD architecture
Venue: arXiv cs.PL 2000
Year: 2000

The aim of this work is to define and implement an extended C++ language to support the SIMD programming paradigm. The C++ programming language has been extended to express all the potentiality of an abstract SIMD machine consisting of a central Control Processor and a N-dimensional toroidal array of Numeric Processors. Very few extensions have been added to the standard C++ with the goal of minimising the effort for the programmer in learning a new language and to keep very high the performance of the compiled code. The proposed language has been implemented as a porting of the GNU C++ Compiler on a SIMD supercomputer.
A One-Time Pad based Cipher for Data Protection in Distributed Environments
Venue: arXiv cs.CR 2000
Year: 2000

A one-time pad (OTP) based cipher to insure both data protection and integrity when mobile code arrives to a remote host is presented. Data protection is required when a mobile agent could retrieve confidential information that would be encrypted in untrusted nodes of the network; in this case, information management could not rely on carrying an encryption key. Data integrity is a prerequisite because mobile code must be protected against malicious hosts that, by counterfeiting or removing collected data, could cover information to the server that has sent the agent. The algorithm described in this article seems to be simple enough, so as to be easily implemented. This scheme is based on a non-interactive protocol and allows a remote host to change its own data on-the-fly and, at the same time, protecting information against handling by other hosts.