OpenRaiser/Intern-Atlas huggingface dataset:
Rigorous design of tracers: an experiment for constraint logic programming
Venue: arXiv cs.SE 2003
Year: 2003

In order to design and implement tracers, one must decide what exactly to trace and how to produce this trace. On the one hand, trace designs are too often guided by implementation concerns and are not as useful as they should be. On the other hand, an interesting trace which cannot be produced efficiently, is not very useful either. In this article we propose a methodology which helps to efficiently produce accurate traces. Firstly, design a formal specification of the trace model. Secondly, derive a prototype tracer from this specification. Thirdly, analyze the produced traces. Fourthly, implement an efficient tracer. Lastly, compare the traces of the two tracers. At each step, problems can be found. In that case one has to iterate the process. We have successfully applied the proposed methodology to the design and implementation of a real tracer for constraint logic programming which is able to efficiently generate information required to build interesting graphical views of executions.
Abductive Logic Programs with Penalization: Semantics, Complexity and Implementation
Venue: arXiv cs.AI 2003
Year: 2003

Abduction, first proposed in the setting of classical logics, has been studied with growing interest in the logic programming area during the last years. In this paper we study abduction with penalization in the logic programming framework. This form of abductive reasoning, which has not been previously analyzed in logic programming, turns out to represent several relevant problems, including optimization problems, very naturally. We define a formal model for abduction with penalization over logic programs, which extends the abductive framework proposed by Kakas and Mancarella. We address knowledge representation issues, encoding a number of problems in our abductive framework. In particular, we consider some relevant problems, taken from different domains, ranging from optimization theory to diagnosis and planning; their encodings turn out to be simple and elegant in our formalism. We thoroughly analyze the computational complexity of the main problems arising in the context of abduction with penalization from logic programs. Finally, we implement a system supporting the proposed abductive framework on top of the DLV engine. To this end, we design a translation from abduction problems with penalties into logic programs with weak constraints. We prove that this approach is sound and complete.
OTTER 3.3 Reference Manual
Venue: arXiv cs.SC 2003
Year: 2003

OTTER is a resolution-style theorem-proving program for first-order logic with equality. OTTER includes the inference rules binary resolution, hyperresolution, UR-resolution, and binary paramodulation. Some of its other abilities and features are conversion from first-order formulas to clauses, forward and back subsumption, factoring, weighting, answer literals, term ordering, forward and back demodulation, evaluable functions and predicates, Knuth-Bendix completion, and the hints strategy. OTTER is coded in ANSI C, is free, and is portable to many different kinds of computer.
Application Architecture for Spoken Language Resources in Organisational Settings
Venue: arXiv cs.CL 2003
Year: 2003

Special technologies need to be used to take advantage of, and overcome, the challenges associated with acquiring, transforming, storing, processing, and distributing spoken language resources in organisations. This paper introduces an application architecture consisting of tools and supporting utilities for indexing and transcription, and describes how these tools, together with downstream processing and distribution systems, can be integrated into a workflow. Two sample applications for this architecture are outlined- the analysis of decision-making processes in organisations and the deployment of systems development methods by designers in the field.
Logic programs with monotone cardinality atoms
Venue: arXiv cs.LO 2003
Year: 2003

We investigate mca-programs, that is, logic programs with clauses built of monotone cardinality atoms of the form kX, where k is a non-negative integer and X is a finite set of propositional atoms. We develop a theory of mca-programs. We demonstrate that the operational concept of the one-step provability operator generalizes to mca-programs, but the generalization involves nondeterminism. Our main results show that the formalism of mca-programs is a common generalization of (1) normal logic programming with its semantics of models, supported models and stable models, (2) logic programming with cardinality atoms and with the semantics of stable models, as defined by Niemela, Simons and Soininen, and (3) of disjunctive logic programming with the possible-model semantics of Sakama and Inoue.
Computing Convex Hulls with a Linear Solver
Venue: arXiv cs.PL 2003
Year: 2003

A programming tactic involving polyhedra is reported that has been widely applied in the polyhedral analysis of (constraint) logic programs. The method enables the computations of convex hulls that are required for polyhedral analysis to be coded with linear constraint solving machinery that is available in many Prolog systems. To appear in Theory and Practice of Logic Programming (TPLP)
How Push-To-Talk Makes Talk Less Pushy
Venue: arXiv cs.HC 2003
Year: 2003

This paper presents an exploratory study of college-age students using two-way, push-to-talk cellular radios. We describe the observed and reported use of cellular radio by the participants. We discuss how the half-duplex, lightweight cellular radio communication was associated with reduced interactional commitment, which meant the cellular radios could be used for a wide range of conversation styles. One such style, intermittent conversation, is characterized by response delays. Intermittent conversation is surprising in an audio medium, since it is typically associated with textual media such as instant messaging. We present design implications of our findings.
Optimized Flooding Protocol for Ad hoc Networks
Venue: arXiv cs.NI 2003
Year: 2003

Flooding provides important control and route establishment functionality for a number of unicast and multicast protocols in Mobile Ad Hoc Networks. Considering its wide use as a building block for other network layer protocols, the flooding methodology should deliver a packet from one node to all other network nodes using as few messages as possible. In this paper, we propose the Optimized Flooding Protocol (OFP), based on a variation of The Covering Problem that is encountered in geometry, to minimize the unnecessary transmissions drastically and still be able to cover the whole region. OFP does not need hello messages and hence OFP saves a significant amount of wireless bandwidth and incurs lesser overhead. We present simulation results to show the efficiency of OFP in both ideal cases and randomly distributed networks. Moreover, OFP is scalable with respect to density; in fact OFP requires lesser number of transmissions at higher densities. OFP is also resilient to transmission errors.
LCG-1 Deployment and usage experience
Venue: arXiv cs.DC 2003
Year: 2003

LCG-1 is the second release of the software framework for the LHC Computing Grid project. In our work we describe the installation process, arising problems and their solutions, and configuration tuning details of the complete LCG-1 site, including all LCG elements required for the self-sufficient site.
Temporalized logics and automata for time granularity
Venue: arXiv cs.LO 2003
Year: 2003

Suitable extensions of the monadic second-order theory of k successors have been proposed in the literature to capture the notion of time granularity. In this paper, we provide the monadic second-order theories of downward unbounded layered structures, which are infinitely refinable structures consisting of a coarsest domain and an infinite number of finer and finer domains, and of upward unbounded layered structures, which consist of a finest domain and an infinite number of coarser and coarser domains, with expressively complete and elementarily decidable temporal logic counterparts. We obtain such a result in two steps. First, we define a new class of combined automata, called temporalized automata, which can be proved to be the automata-theoretic counterpart of temporalized logics, and show that relevant properties, such as closure under Boolean operations, decidability, and expressive equivalence with respect to temporal logics, transfer from component automata to temporalized ones. Then, we exploit the correspondence between temporalized logics and automata to reduce the task of finding the temporal logic counterparts of the given theories of time granularity to the easier one of finding temporalized automata counterparts of them.
Logic-Based Specification Languages for Intelligent Software Agents
Venue: arXiv cs.AI 2003
Year: 2003

The research field of Agent-Oriented Software Engineering (AOSE) aims to find abstractions, languages, methodologies and toolkits for modeling, verifying, validating and prototyping complex applications conceptualized as Multiagent Systems (MASs). A very lively research sub-field studies how formal methods can be used for AOSE. This paper presents a detailed survey of six logic-based executable agent specification languages that have been chosen for their potential to be integrated in our ARPEGGIO project, an open framework for specifying and prototyping a MAS. The six languages are ConGoLog, Agent-0, the IMPACT agent programming language, DyLog, Concurrent METATEM and Ehhf. For each executable language, the logic foundations are described and an example of use is shown. A comparison of the six languages and a survey of similar approaches complete the paper, together with considerations of the advantages of using logic-based languages in MAS modeling and prototyping.
XPath-Logic and XPathLog: A Logic-Programming Style XML Data Manipulation Language
Venue: arXiv cs.DB 2003
Year: 2003

We define XPathLog as a Datalog-style extension of XPath. XPathLog provides a clear, declarative language for querying and manipulating XML whose perspectives are especially in XML data integration. In our characterization, the formal semantics is defined wrt. an edge-labeled graph-based model which covers the XML data model. We give a complete, logic-based characterization of XML data and the main language concept for XML, XPath. XPath-Logic extends the XPath language with variable bindings and embeds it into first-order logic. XPathLog is then the Horn fragment of XPath-Logic, providing a Datalog-style, rule-based language for querying and manipulating XML data. The model-theoretic semantics of XPath-Logic serves as the base of XPathLog as a logic-programming language, whereas also an equivalent answer-set semantics for evaluating XPathLog queries is given. In contrast to other approaches, the XPath syntax and semantics is also used for a declarative specification how the database should be updated: when used in rule heads, XPath filters are interpreted as specifications of elements and properties which should be added to the database.
Idempotent I/O for safe time travel
Venue: arXiv cs.PL 2003
Year: 2003

Debuggers for logic programming languages have traditionally had a capability most other debuggers did not: the ability to jump back to a previous state of the program, effectively travelling back in time in the history of the computation. This ``retry'' capability is very useful, allowing programmers to examine in detail a part of the computation that they previously stepped over. Unfortunately, it also creates a problem: while the debugger may be able to restore the previous values of variables, it cannot restore the part of the program's state that is affected by I/O operations. If the part of the computation being jumped back over performs I/O, then the program will perform these I/O operations twice, which will result in unwanted effects ranging from the benign (e.g. output appearing twice) to the fatal (e.g. trying to close an already closed file). We present a simple mechanism for ensuring that every I/O action called for by the program is executed at most once, even if the programmer asks the debugger to travel back in time from after the action to before the action. The overhead of this mechanism is low enough and can be controlled well enough to make it practical to use it to debug computations that do significant amounts of I/O.
Derivation of Efficient Logic Programs by Specialization and Reduction of Nondeterminism
Venue: arXiv cs.PL 2003
Year: 2003

Program specialization is a program transformation methodology which improves program efficiency by exploiting the information about the input data which are available at compile time. We show that current techniques for program specialization based on partial evaluation do not perform well on nondeterministic logic programs. We then consider a set of transformation rules which extend the ones used for partial evaluation, and we propose a strategy for guiding the application of these extended rules so to derive very efficient specialized programs. The efficiency improvements which sometimes are exponential, are due to the reduction of nondeterminism and to the fact that the computations which are performed by the initial programs in different branches of the computation trees, are performed by the specialized programs within single branches. In order to reduce nondeterminism we also make use of mode information for guiding the unfolding process. To exemplify our technique, we show that we can automatically derive very efficient matching programs and parsers for regular languages. The derivations we have performed could not have been done by previously known partial evaluation techniques.
Integrating existing cone-shaped and projection-based cardinal direction relations and a TCSP-like decidable generalisation
Venue: arXiv cs.AI 2003
Year: 2003

We consider the integration of existing cone-shaped and projection-based calculi of cardinal direction relations, well-known in QSR. The more general, integrating language we consider is based on convex constraints of the qualitative form $r(x,y)$, $r$ being a cone-shaped or projection-based cardinal direction atomic relation, or of the quantitative form $(α,β)(x,y)$, with $α,β\in [0,2π)$ and $(β-α)\in [0,π]$: the meaning of the quantitative constraint, in particular, is that point $x$ belongs to the (convex) cone-shaped area rooted at $y$, and bounded by angles $α$ and $β$. The general form of a constraint is a disjunction of the form $[r_1\vee...\vee r_{n_1}\vee (α_1,β_1)\vee...\vee (α_{n_2},β_{n_2})](x,y)$, with $r_i(x,y)$, $i=1... n_1$, and $(α_i,β_i)(x,y)$, $i=1... n_2$, being convex constraints as described above: the meaning of such a general constraint is that, for some $i=1... n_1$, $r_i(x,y)$ holds, or, for some $i=1... n_2$, $(α_i,β_i)(x,y)$ holds. A conjunction of such general constraints is a $\tcsp$-like CSP, which we will refer to as an $\scsp$ (Spatial Constraint Satisfaction Problem). An effective solution search algorithm for an $\scsp$ will be described, which uses (1) constraint propagation, based on a composition operation to be defined, as the filtering method during the search, and (2) the Simplex algorithm, guaranteeing completeness, at the leaves of the search tree. The approach is particularly suited for large-scale high-level vision, such as, e.g., satellite-like surveillance of a geographic area.
Hybrid LQG-Neural Controller for Inverted Pendulum System
Venue: arXiv cs.NE 2003
Year: 2003

The paper presents a hybrid system controller, incorporating a neural and an LQG controller. The neural controller has been optimized by genetic algorithms directly on the inverted pendulum system. The failure free optimization process stipulated a relatively small region of the asymptotic stability of the neural controller, which is concentrated around the regulation point. The presented hybrid controller combines benefits of a genetically optimized neural controller and an LQG controller in a single system controller. High quality of the regulation process is achieved through utilization of the neural controller, while stability of the system during transient processes and a wide range of operation are assured through application of the LQG controller. The hybrid controller has been validated by applying it to a simulation model of an inherently unstable system of inverted pendulum.
Improving spam filtering by combining Naive Bayes with simple k-nearest neighbor searches
Venue: arXiv cs.LG 2003
Year: 2003

Using naive Bayes for email classification has become very popular within the last few months. They are quite easy to implement and very efficient. In this paper we want to present empirical results of email classification using a combination of naive Bayes and k-nearest neighbor searches. Using this technique we show that the accuracy of a Bayes filter can be improved slightly for a high number of features and significantly for a small number of features.
Counting complexity classes for numeric computations II: algebraic and semialgebraic sets
Venue: arXiv cs.CC 2003
Year: 2003

We define counting classes #P_R and #P_C in the Blum-Shub-Smale setting of computations over the real or complex numbers, respectively. The problems of counting the number of solutions of systems of polynomial inequalities over R, or of systems of polynomial equalities over C, respectively, turn out to be natural complete problems in these classes. We investigate to what extent the new counting classes capture the complexity of computing basic topological invariants of semialgebraic sets (over R) and algebraic sets (over C). We prove that the problem of computing the (modified) Euler characteristic of semialgebraic sets is FP_R^{#P_R}-complete, and that the problem of computing the geometric degree of complex algebraic sets is FP_C^{#P_C}-complete. We also define new counting complexity classes in the classical Turing model via taking Boolean parts of the classes above, and show that the problems to compute the Euler characteristic and the geometric degree of (semi)algebraic sets given by integer polynomials are complete in these classes. We complement the results in the Turing model by proving, for all k in N, the FPSPACE-hardness of the problem of computing the k-th Betti number of the zet of real zeros of a given integer polynomial. This holds with respect to the singular homology as well as for the Borel-Moore homology.
Soft lambda-calculus: a language for polynomial time computation
Venue: arXiv cs.LO 2003
Year: 2003

Soft linear logic ([Lafont02]) is a subsystem of linear logic characterizing the class PTIME. We introduce Soft lambda-calculus as a calculus typable in the intuitionistic and affine variant of this logic. We prove that the (untyped) terms of this calculus are reducible in polynomial time. We then extend the type system of Soft logic with recursive types. This allows us to consider non-standard types for representing lists. Using these datatypes we examine the concrete expressivity of Soft lambda-calculus with the example of the insertion sort algorithm.
An Exploratory Study of Mobile Computing Use by Knowledge Workers
Venue: arXiv cs.HC 2003
Year: 2003

This paper describes some preliminary results from a 20-week study on the use of Compaq iPAQ Personal Digital Assistants (PDAs) by 10 senior developers, analysts, technical managers, and senior organisational managers. The goal of the study was to identify what applications were used, how and where they were used, the problems and issues that arose, and how use of the iPAQs changed over the study period. The paper highlights some interesting uses of the iPAQs, and identifies some of the characteristics of successful mobile applications.
Modeling Object Oriented Constraint Programs in Z
Venue: arXiv cs.AI 2003
Year: 2003

Object oriented constraint programs (OOCPs) emerge as a leading evolution of constraint programming and artificial intelligence, first applied to a range of industrial applications called configuration problems. The rich variety of technical approaches to solving configuration problems (CLP(FD), CC(FD), DCSP, Terminological systems, constraint programs with set variables ...) is a source of difficulty. No universally accepted formal language exists for communicating about OOCPs, which makes the comparison of systems difficult. We present here a Z based specification of OOCPs which avoids the falltrap of hidden object semantics. The object system is part of the specification, and captures all of the most advanced notions from the object oriented modeling standard UML. The paper illustrates these issues and the conciseness and precision of Z by the specification of a working OOCP that solves an historical AI problem : parsing a context free grammar. Being written in Z, an OOCP specification also supports formal proofs. The whole builds the foundation of an adaptative and evolving framework for communicating about constrained object models and programs.
Sharing secret color images using cellular automata with memory
Venue: arXiv cs.CR 2003
Year: 2003

A {k,n}-threshold scheme based on two-dimensional memory cellular automata is proposed to share images in a secret way. This method allows to encode an image into n shared images so that only qualified subsets of k or more shares can recover the secret image, but any k-1 or fewer of them gain no information about the original image. The main characteristics of this new scheme are: each shared image has the same size that the original one, and the recovered image is exactly the same than the secret image; i.e., there is no loss of resolution.
On A Theory of Probabilistic Deductive Databases
Venue: arXiv cs.DB 2003
Year: 2003

We propose a framework for modeling uncertainty where both belief and doubt can be given independent, first-class status. We adopt probability theory as the mathematical formalism for manipulating uncertainty. An agent can express the uncertainty in her knowledge about a piece of information in the form of a confidence level, consisting of a pair of intervals of probability, one for each of her belief and doubt. The space of confidence levels naturally leads to the notion of a trilattice, similar in spirit to Fitting's bilattices. Intuitively, thep oints in such a trilattice can be ordered according to truth, information, or precision. We develop a framework for probabilistic deductive databases by associating confidence levels with the facts and rules of a classical deductive database. While the trilattice structure offers a variety of choices for defining the semantics of probabilistic deductive databases, our choice of semantics is based on the truth-ordering, which we find to be closest to the classical framework for deductive databases. In addition to proposing a declarative semantics based on valuations and an equivalent semantics based on fixpoint theory, we also propose a proof procedure and prove it sound and complete. We show that while classical Datalog query programs have a polynomial time data complexity, certain query programs in the probabilistic deductive database framework do not even terminate on some input databases. We identify a large natural class of query programs of practical interest in our framework, and show that programs in this class possess polynomial time data complexity, i.e., not only do they terminate on every input database, they are guaranteed to do so in a number of steps polynomial in the input database size.