OpenRaiser/Intern-Atlas huggingface dataset:
Semi-metric Behavior in Document Networks and its Application to Recommendation Systems
Venue: arXiv cs.IR 2003
Year: 2003

Recommendation systems for different Document Networks (DN) such as the World Wide Web (WWW) and Digital Libraries, often use distance functions extracted from relationships among documents and keywords. For instance, documents in the WWW are related via a hyperlink network, while documents in bibliographic databases are related by citation and collaboration networks. Furthermore, documents are related to keyterms. The distance functions computed from these relations establish associative networks among items of the DN, referred to as Distance Graphs, which allow recommendation systems to identify relevant associations for individual users. However, modern recommendation systems need to integrate associative data from multiple sources such as different databases, web sites, and even other users. Thus, we are presented with a problem of combining evidence (about associations between items) from different sources characterized by distance functions. In this paper we describe our work on (1) inferring relevant associations from, as well as characterizing, semi-metric distance graphs and (2) combining evidence from different distance graphs in a recommendation system. Regarding (1), we present the idea of semi-metric distance graphs, and introduce ratios to measure semi-metric behavior. We compute these ratios for several DN such as digital libraries and web sites and show that they are useful to identify implicit associations. Regarding (2), we describe an algorithm to combine evidence from distance graphs that uses Evidence Sets, a set structure based on Interval Valued Fuzzy Sets and Dempster-Shafer Theory of Evidence. This algorithm has been developed for a recommendation system named TalkMine.
cTI: A constraint-based termination inference tool for ISO-Prolog
Venue: arXiv cs.PL 2003
Year: 2003

We present cTI, the first system for universal left-termination inference of logic programs. Termination inference generalizes termination analysis and checking. Traditionally, a termination analyzer tries to prove that a given class of queries terminates. This class must be provided to the system, for instance by means of user annotations. Moreover, the analysis must be redone every time the class of queries of interest is updated. Termination inference, in contrast, requires neither user annotations nor recomputation. In this approach, terminating classes for all predicates are inferred at once. We describe the architecture of cTI and report an extensive experimental evaluation of the system covering many classical examples from the logic programming termination literature and several Prolog programs of respectable size and complexity.
Finding approximate palindromes in strings
Venue: arXiv cs.DS 2003
Year: 2003

We introduce a novel definition of approximate palindromes in strings, and provide an algorithm to find all maximal approximate palindromes in a string with up to $k$ errors. Our definition is based on the usual edit operations of approximate pattern matching, and the algorithm we give, for a string of size $n$ on a fixed alphabet, runs in $O(k^2 n)$ time. We also discuss two implementation-related improvements to the algorithm, and demonstrate their efficacy in practice by means of both experiments and an average-case analysis.
Computing Igusa's Local Zeta Functions of Univariate Polynomials, and Linear Feedback Shift Registers
Venue: arXiv cs.SC 2003
Year: 2003

We give a polynomial time algorithm for computing the Igusa local zeta function $Z(s,f)$ attached to a polynomial $f(x)\in \QTR{Bbb}{Z}[x]$, in one variable, with splitting field $\QTR{Bbb}{Q}$, and a prime number $p$. We also propose a new class of Linear Feedback Shift Registers based on the computation of Igusa's local zeta function.
A Performance Analysis Tool for Nokia Mobile Phone Software
Venue: arXiv cs.SE 2003
Year: 2003

Performance problems are often observed in embedded software systems. The reasons for poor performance are frequently not obvious. Bottlenecks can occur in any of the software components along the execution path. Therefore it is important to instrument and monitor the different components contributing to the runtime behavior of an embedded software system. Performance analysis tools can help locate performance bottlenecks in embedded software systems by monitoring the software's execution and producing easily understandable performance data. We maintain and further develop a tool for analyzing the performance of Nokia mobile phone software. The user can select among four performance analysis reports to be generated: average processor load, processor utilization, task execution time statistics, and task execution timeline. Each of these reports provides important information about where execution time is being spent. The demo will show how the tool helps to identify performance bottlenecks in Nokia mobile phone software and better understand areas of poor performance.
Determination of the Topology of a Directed Network
Venue: arXiv cs.DC 2003
Year: 2003

We consider strongly-connected directed networks of identical synchronous, finite-state processors with in- and out-degree uniformly bounded by a network constant. Via a straightforward extension of Ostrovsky and Wilkerson's Backwards Communication Algorithm in [OW], we exhibit a protocol which solves the Global Topology Determination Problem, the problem of having the root processor map the global topology of a network of unknown size and topology, with running time O(ND) where N represents the number of processors and D represents the diameter of the network. A simple counting argument suffices to show that the Global Topology Determination Problem has time-complexity Omega(N logN) which makes the protocol presented asymptotically time-optimal for many large networks.
Re-Finding Found Things: An Exploratory Study of How Users Re-Find Information
Venue: arXiv cs.HC 2003
Year: 2003

The problem of how people find information is studied extensively; however, the problem of how people organize, re-use, and re-find information that they have found is not as well understood. Recently, several projects have conducted in-situ studies to explore how people re-find and re-use information. Here, we present results and observations from a controlled, laboratory study of refinding information found on the web. Our study was conducted as a collaborative exercise with pairs of participants. One participant acted as a retriever, helping the other participant re-find information by telephone. This design allowed us to gain insight into the strategies that users employed to re-find information, and into how domain artifacts and contextual information were used to aid the re-finding process. We also introduced the ability for users to add their own explicitly artifacts in the form of making annotations on the web pages they viewed. We observe that re-finding often occurs as a two stage, iterative process in which users first attempt to locate an information source (search), and once found, begin a process to find the specific information being sought (browse). Our findings are consistent with research on waypoints; orienteering approaches to re-finding; and navigation of electronic spaces. Furthermore, we observed that annotations were utilized extensively, indicating that explicitly added context by the user can play an important role in re-finding.
A Monitoring Language for Run Time and Post-Mortem Behavior Analysis and Visualization
Venue: arXiv cs.SE 2003
Year: 2003

UFO is a new implementation of FORMAN, a declarative monitoring language, in which rules are compiled into execution monitors that run on a virtual machine supported by the Alamo monitor architecture.
A Particular Bug Trap: Execution Replay Using Virtual Machines
Venue: arXiv cs.DC 2003
Year: 2003

Execution-replay (ER) is well known in the literature but has been restricted to special system architectures for many years. Improved hardware resources and the maturity of virtual machine technology promise to make ER useful for a broader range of development projects. This paper describes an approach to create a practical, generic ER infrastructure for desktop PC systems using virtual machine technology. In the created VM environment arbitrary application programs will run and be replayed unmodified, neither instrumentation nor recompilation are required.
Secret Sharing for n-Colorable Graphs with Application to Public Key Cryptography
Venue: arXiv cs.CR 2003
Year: 2003

At the beginning some results from the field of graph theory are presented. Next we show how to share a secret that is proper n-coloring of the graph, with the known structure. The graph is described and converted to the form, where colors assigned to vertices form the number with entries from Zn. A secret sharing scheme (SSS) for the graph coloring is proposed. The proposed method is applied to the public-key cryptosystem called "Polly Cracker". In this case the graph structure is a public key, while proper 3-colouring of the graph is a private key. We show how to share the private key. Sharing particular n-coloring (color-to-vertex assignment) for the known-structure graph is presented next.
Mace4 Reference Manual and Guide
Venue: arXiv cs.SC 2003
Year: 2003

Mace4 is a program that searches for finite models of first-order formulas. For a given domain size, all instances of the formulas over the domain are constructed. The result is a set of ground clauses with equality. Then, a decision procedure based on ground equational rewriting is applied. If satisfiability is detected, one or more models are printed. Mace4 is a useful complement to first-order theorem provers, with the prover searching for proofs and Mace4 looking for countermodels, and it is useful for work on finite algebras. Mace4 performs better on equational problems than did our previous model-searching program Mace2.
An Introduction to Using Software Tools for Automatic Differentiation
Venue: arXiv cs.MS 2003
Year: 2003

We give a gentle introduction to using various software tools for automatic differentiation (AD). Ready-to-use examples are discussed, and links to further information are presented. Our target audience includes all those who are looking for a straightforward way to get started using the available AD technology. The document is dynamic in the sense that its content will be updated as the AD software evolves.
WSAT(cc) - a fast local-search ASP solver
Venue: arXiv cs.AI 2003
Year: 2003

We describe WSAT(cc), a local-search solver for computing models of theories in the language of propositional logic extended by cardinality atoms. WSAT(cc) is a processing back-end for the logic PS+, a recently proposed formalism for answer-set programming.
Maintaining Information in Fully-Dynamic Trees with Top Trees
Venue: arXiv cs.DS 2003
Year: 2003

We introduce top trees as a design of a new simpler interface for data structures maintaining information in a fully-dynamic forest. We demonstrate how easy and versatile they are to use on a host of different applications. For example, we show how to maintain the diameter, center, and median of each tree in the forest. The forest can be updated by insertion and deletion of edges and by changes to vertex and edge weights. Each update is supported in O(log n) time, where n is the size of the tree(s) involved in the update. Also, we show how to support nearest common ancestor queries and level ancestor queries with respect to arbitrary roots in O(log n) time. Finally, with marked and unmarked vertices, we show how to compute distances to a nearest marked vertex. The later has applications to approximate nearest marked vertex in general graphs, and thereby to static optimization problems over shortest path metrics. Technically speaking, top trees are easily implemented either with Frederickson's topology trees [Ambivalent Data Structures for Dynamic 2-Edge-Connectivity and k Smallest Spanning Trees, SIAM J. Comput. 26 (2) pp. 484-538, 1997] or with Sleator and Tarjan's dynamic trees [A Data Structure for Dynamic Trees. J. Comput. Syst. Sc. 26 (3) pp. 362-391, 1983]. However, we claim that the interface is simpler for many applications, and indeed our new bounds are quadratic improvements over previous bounds where they exist.
Enhancing a Search Algorithm to Perform Intelligent Backtracking
Venue: arXiv cs.AI 2003
Year: 2003

This paper illustrates how a Prolog program, using chronological backtracking to find a solution in some search space, can be enhanced to perform intelligent backtracking. The enhancement crucially relies on the impurity of Prolog that allows a program to store information when a dead end is reached. To illustrate the technique, a simple search program is enhanced. To appear in Theory and Practice of Logic Programming. Keywords: intelligent backtracking, dependency-directed backtracking, backjumping, conflict-directed backjumping, nogood sets, look-back.
A Parameterised Hierarchy of Argumentation Semantics for Extended Logic Programming and its Application to the Well-founded Semantics
Venue: arXiv cs.LO 2003
Year: 2003

Argumentation has proved a useful tool in defining formal semantics for assumption-based reasoning by viewing a proof as a process in which proponents and opponents attack each others arguments by undercuts (attack to an argument's premise) and rebuts (attack to an argument's conclusion). In this paper, we formulate a variety of notions of attack for extended logic programs from combinations of undercuts and rebuts and define a general hierarchy of argumentation semantics parameterised by the notions of attack chosen by proponent and opponent. We prove the equivalence and subset relationships between the semantics and examine some essential properties concerning consistency and the coherence principle, which relates default negation and explicit negation. Most significantly, we place existing semantics put forward in the literature in our hierarchy and identify a particular argumentation semantics for which we prove equivalence to the paraconsistent well-founded semantics with explicit negation, WFSX$_p$. Finally, we present a general proof theory, based on dialogue trees, and show that it is sound and complete with respect to the argumentation semantics.
OGSA/Globus Evaluation for Data Intensive Applications
Venue: arXiv cs.DC 2003
Year: 2003

We present an architecture of Globus Toolkit 3 based testbed intended for evaluation of applicability of the Open Grid Service Architecture (OGSA) for Data Intensive Applications.
The Chameleon Type Debugger (Tool Demonstration)
Venue: arXiv cs.PL 2003
Year: 2003

In this tool demonstration, we give an overview of the Chameleon type debugger. The type debugger's primary use is to identify locations within a source program which are involved in a type error. By further examining these (potentially) problematic program locations, users gain a better understanding of their program and are able to work towards the actual mistake which was the cause of the type error. The debugger is interactive, allowing the user to provide additional information to narrow down the search space. One of the novel aspects of the debugger is the ability to explain erroneous-looking types. In the event that an unexpected type is inferred, the debugger can highlight program locations which contributed to that result. Furthermore, due to the flexible constraint-based foundation that the debugger is built upon, it can naturally handle advanced type system features such as Haskell's type classes and functional dependencies.
Combining Logic Programs and Monadic Second Order Logics by Program Transformation
Venue: arXiv cs.PL 2003
Year: 2003

We present a program synthesis method based on unfold/fold transformation rules which can be used for deriving terminating definite logic programs from formulas of the Weak Monadic Second Order theory of one successor (WS1S). This synthesis method can also be used as a proof method which is a decision procedure for closed formulas of WS1S. We apply our synthesis method for translating CLP(WS1S) programs into logic programs and we use it also as a proof method for verifying safety properties of infinite state systems.
Algebras for Agent Norm-Regulation
Venue: arXiv cs.LO 2003
Year: 2003

An abstract architecture for idealized multi-agent systems whose behaviour is regulated by normative systems is developed and discussed. Agent choices are determined partially by the preference ordering of possible states and partially by normative considerations: The agent chooses that act which leads to the best outcome of all permissible actions. If an action is non-permissible depends on if the result of performing that action leads to a state satisfying a condition which is forbidden, according to the norms regulating the multi-agent system. This idea is formalized by defining set-theoretic predicates characterizing multi-agent systems. The definition of the predicate uses decision theory, the Kanger-Lindahl theory of normative positions, and an algebraic representation of normative systems.
Data mining and Privacy in Public Sector using Intelligent Agents (discussion paper)
Venue: arXiv cs.CY 2003
Year: 2003

The public sector comprises government agencies, ministries, education institutions, health providers and other types of government, commercial and not-for-profit organisations. Unlike commercial enterprises, this environment is highly heterogeneous in all aspects. This forms a complex network which is not always optimised. A lack of optimisation and communication hinders information sharing between the network nodes limiting the flow of information. Another limiting aspect is privacy of personal information and security of operations of some nodes or segments of the network. Attempts to reorganise the network or improve communications to make more information available for sharing and analysis may be hindered or completely halted by public concerns over privacy, political agendas, social and technological barriers. This paper discusses a technical solution for information sharing while addressing the privacy concerns with no need for reorganisation of the existing public sector infrastructure . The solution is based on imposing an additional layer of Intelligent Software Agents and Knowledge Bases for data mining and analysis.
Benchmarking and Implementation of Probability-Based Simulations on Programmable Graphics Cards
Venue: arXiv cs.GR 2003
Year: 2003

The latest Graphics Processing Units (GPUs) are reported to reach up to 200 billion floating point operations per second (200 Gflops) and to have price performance of 0.1 cents per M flop. These facts raise great interest in the plausibility of extending the GPUs' use to non-graphics applications, in particular numerical simulations on structured grids (lattice). We review previous work on using GPUs for non-graphics applications, implement probability-based simulations on the GPU, namely the Ising and percolation models, implement vector operation benchmarks for the GPU, and finally compare the CPU's and GPU's performance. A general conclusion from the results obtained is that moving computations from the CPU to the GPU is feasible, yielding good time and price performance, for certain lattice computations. Preliminary results also show that it is feasible to use them in parallel
Constraint Optimization and Statistical Mechanics
Venue: arXiv cs.CC 2003
Year: 2003

In these lectures I will present an introduction to the results that have been recently obtained in constraint optimization of random problems using statistical mechanics techniques. After presenting the general results, in order to simplify the presentation I will describe in details only the problems related to the coloring of a random graph.
Methods to Model-Check Parallel Systems Software
Venue: arXiv cs.LO 2003
Year: 2003

We report on an effort to develop methodologies for formal verification of parts of the Multi-Purpose Daemon (MPD) parallel process management system. MPD is a distributed collection of communicating processes. While the individual components of the collection execute simple algorithms, their interaction leads to unexpected errors that are difficult to uncover by conventional means. Two verification approaches are discussed here: the standard model checking approach using the software model checker SPIN and the nonstandard use of a general-purpose first-order resolution-style theorem prover OTTER to conduct the traditional state space exploration. We compare modeling methodology and analyze performance and scalability of the two methods with respect to verification of MPD.
Mapping Subsets of Scholarly Information
Venue: arXiv cs.IR 2003
Year: 2003

We illustrate the use of machine learning techniques to analyze, structure, maintain, and evolve a large online corpus of academic literature. An emerging field of research can be identified as part of an existing corpus, permitting the implementation of a more coherent community structure for its practitioners.
Strong Equivalence Made Easy: Nested Expressions and Weight Constraints
Venue: arXiv cs.LO 2003
Year: 2003

Logic programs P and Q are strongly equivalent if, given any program R, programs P union R and Q union R are equivalent (that is, have the same answer sets). Strong equivalence is convenient for the study of equivalent transformations of logic programs: one can prove that a local change is correct without considering the whole program. Lifschitz, Pearce and Valverde showed that Heyting's logic of here-and-there can be used to characterize strong equivalence for logic programs with nested expressions (which subsume the better-known extended disjunctive programs). This note considers a simpler, more direct characterization of strong equivalence for such programs, and shows that it can also be applied without modification to the weight constraint programs of Niemela and Simons. Thus, this characterization of strong equivalence is convenient for the study of equivalent transformations of logic programs written in the input languages of answer set programming systems dlv and smodels. The note concludes with a brief discussion of results that can be used to automate reasoning about strong equivalence, including a novel encoding that reduces the problem of deciding the strong equivalence of a pair of weight constraint programs to that of deciding the inconsistency of a weight constraint program.
CSIEC (Computer Simulator in Educational Communication): An Intelligent Web-Based Teaching System for Foreign Language Learning
Venue: arXiv cs.CY 2003
Year: 2003

In this paper we present an innovative intelligent web-based computer-aided instruction system for foreign language learning: CSIEC (Computer Simulator in Educational Communication). This system can not only grammatically understand the sentences in English given from the users via Internet, but also reasonably and individually speak with the users. At first the related works in this research field are analyzed. Then we introduce the system goals and the system framework, i.e., the natural language understanding mechanism (NLML, NLOMJ and NLDB) and the communicational response (CR). Finally we give the syntactic and semantic content of this instruction system, i.e. some important notations of English grammar used in it and their relations with the NLOMJ.