Clausal Logic and Logic Programming in Algebraic Domains

We introduce a domain-theoretic foundation for disjunctive logic programming. This foundation is built on clausal logic, a representation of the Smyth powerdomain of any coherent algebraic dcpo. We establish the completeness of a resolution rule for inference in such a clausal logic; we introduce a natural declarative semantics and a fixed-point semantics for disjunctive logic programs, and prove their equivalence; finally, we apply our results to give both a syntax and semantics for default logic in any coherent algebraic dcpo.     

The Undecidability of the First-Order Theories of One Step Rewriting in Linear Canonical Systems

By reduction from the halting problem for Minsky's two-register machines we prove that there is no algorithm capable of deciding the -theory of one step rewriting of an arbitrary finite linear confluent finitely terminating term rewriting system (weak undecidability). We also present a fixed such system with undecidable *-theory of one step rewriting (strong undecidability). This improves over all previously known results of the same kind.     

Assigning Types to Processes

In wide area distributed systems it is now common for higher-order code to be transferred from one domain to another; the receiving host may initialise parameters and then execute the code in its local environment. In this paper we propose a fine-grained typing system for a higher-order π-calculus which can be used to control the effect of such migrating code on local environments. Processes may be assigned different types depending on their intended use. This is in contrast to most of the previous work on typing processes where all processes are typed by a unique constant type, indicating essentially that they are well typed relative to a particular environment. Our fine-grained typing facilitates the management of access rights and provides host protection from potentially malicious behaviour. Our process type takes the form of an interface limiting the resources to which it has access and the types at which they may be used. Allowing resource names to appear both in process types and process terms, as interaction ports, complicates the typing system considerably. For the development of a coherent typing system, we use a kinding technique, similar to that used by the subtyping of the system F, and order-theoretic properties of our subtyping relation. Various examples of this paper illustrate the usage of our fine-grained process types in distributed systems.     

Optimal Series-Parallel Trade-offs for Reducing a Function to Its Own Graph

Consider the problem of computing a function given only an oracle for its graph. For this problem, we present optimal trade-offs between serial and parallel queries. In particular, we give a function for which parallel access to its own graph is exponentially more expensive than sequential access.     

Encoding Linear Logic with Interaction Combinators

The purpose of this paper is to demonstrate how Lafont's interaction combinators, a system of three symbols and six interaction rules, can be used to encode linear logic. Specifically, we give a translation of the multiplicative, exponential, and additive fragments of linear logic together with a strategy for cut-elimination which can be faithfully simulated. Finally, we show briefly how this encoding can be used for evaluating λ-terms. In addition to offering a very simple, perhaps the simplest, system of rewriting for linear logic and the λ-calculus, the interaction net implementation that we present has been shown by experimental testing to offer a good level of sharing in terms of the number of cut-elimination steps (resp. β-reduction steps). In particular it performs better than all extant finite systems of interaction nets.     

Formative Processes with Applications to the Decision Problem in Set Theory: I. Powerset and Singleton Operators

This paper introduces formative processes, composed by transitive partitions. Given a family of sets, a formative process ending in the Venn partition Σ of is shown to exist. Sufficient criteria are also singled out for a transitive partition to model (via a function from set variables to unions of sets in the partition) all set-literals modeled by Σ. On the basis of such criteria a procedure is designed that mimics a given formative process by another where sets have finite rank bounded by C(|Σ|), with C a specific computable function. As a by-product, one of the core results on decidability in computable set theory is rediscovered, namely the one that regards the satisfiability of unquantified set-theoretic formulae involving Boolean operators, the singleton-former, and the powerset operator. The method described (which is able to exhibit a set-solution when the answer is affirmative) can be extended to solve the satisfiability problem for broader fragments of set theory.     

Test Sets for the Universal and Existential Closure of Regular Tree Languages

Finite test sets are a useful tool for deciding the membership problem for the universal closure of a given tree language, that is, for deciding whether a term has all its ground instances in the given language. A uniform test set for the universal closure must serve the following purpose: In order to decide membership of a term, it is sufficient to check whether all its test set instances belong to the underlying language. A possible application, and our main motivation, is ground reducibility, an essential concept for many approaches to inductive reasoning. Ground reducibility modulo some rewrite system is membership in the universal closure of the set of reducible ground terms. Here, test sets always exist, and several algorithmic approaches are known. The resulting sets, however, are often unnecessarily large. In this paper we consider regular languages and linear closure operators. We prove that universal as well as existential closure, defined analogously, preserve regularity. By relating test sets to tree automata and to appropriate congruence relations, we show how to characterize, how to compute, and how to minimize ground and non-ground test sets. In particular, optimal solutions now replace previous ad hoc approximations for the ground reducibility problem.     

Reduction of Permutation-Invariant Polynomials: A Noncommutative Case Study

Let R be a commutative ring with 1, let RX₁,…,X_n/I be the polynomial algebra in the n≥4 noncommuting variables X₁,…,X_n over R modulo the set of commutator relations I={(X₁+···+X_n)*X_i=X_i*(X₁+···+X_n)|1≤i≤n}. Furthermore, let G be an arbitrary group of permutations operating on the indeterminates X₁,…,X_n, and let RX₁,…,X_n/I^G be the R-algebra of G-invariant polynomials in RX₁,…,X_n/I. The first part of this paper is about an algorithm, which computes a representation for any fRX₁,…,X_n/I^G as a polynomial in multilinear G-invariant polynomials, i.e., the maximal variable degree of the generators of RX₁,…,X_n/I^G is at most 1. The algorithm works for any ring R and for any permutation group G. In addition, we present a bound for the number of necessary generators for the representation of all G-invariant polynomials in RX₁,…,X_n/I^G with a total degree of at most d. The second part contains a first but promising analysis of G-invariant polynomials of solvable polynomial rings.     

An Algebraic Approach to Camera Self-Calibration

This paper describes a new self-calibration method for a single camera undergoing general motions. It has the following main contributions. First, we establish new constraints which relate the intrinsic parameters of the camera to the rotational part of the motions. This derivation is purely algebraic. We propose an algorithm which simultaneously solves for camera calibration and the rotational part of motions. Second, we provide a comparison between the developed method and a Kruppa equation-based method. Extensive experiments on both synthetic and real image data show the reliability and outperformance of the proposed method. The practical contribution of the method is its interesting convergence property compared with that of the Kruppa equations method.     

Communication Complexity Method for Measuring Nondeterminism in Finite Automata

While deterministic finite automata seem to be well understood, surprisingly many important problems concerning nondeterministic finite automata (nfa's) remain open. One such problem area is the study of different measures of nondeterminism in finite automata and the estimation of the sizes of minimal nondeterministic finite automata. In this paper the concept of communication complexity is applied in order to achieve progress in this problem area. The main results are as follows:1. Deterministic communication complexity provides lower bounds on the size of nfa's with bounded unambiguity. Applying this fact, the proofs of several results about nfa's with limited ambiguity can be simplified and presented in a uniform way.2. There is a family of languages KON_k² with an exponential size gap between nfa's with polynomial leaf number/ambiguity and nfa's with ambiguity k. This partially provides an answer to the open problem posed by B. Ravikumar and O. Ibarra (1989, SIAM J. Comput.18, 1263–1282) and H. Leung (1998, SIAM J. Comput.27, 1073–1082).     

An Exhaustive Study of Particular Cases Leading to Robust and Accurate Motion Estimation

For decades, there has been an intensive research effort in the Computer Vision community to deal with video sequences. In this paper, we present a new method for recovering a maximum of information on displacement and projection parameters in monocular video sequences without calibration. This work follows previous studies on particular cases of displacement, scene geometry, and camera analysis and focuses on the particular forms of homographic matrices. It is already known that the number of particular cases involved in a complete study precludes an exhaustive test. To lower the algorithmic complexity, some authors propose to decompose all possible cases in a hierarchical tree data structure but these works are still in development (T. Viéville and D. Lingrand, Internat. J. Comput. Vision31, 1999, 5–L29). In this paper, we propose a new way to deal with the huge number of particular cases: (i) we use simple rules in order to eliminate some redundant cases and some physically impossible cases, and (ii) we divide the cases into subsets corresponding to particular forms determined by simple rules leading to a computationally efficient discrimination method. Finally, some experiments were performed on image sequences acquired either using a robotic system or manually in order to demonstrate that when several models are valid, the model with the fewer parameters gives the best estimation, regarding the free parameters of the problem. The experiments presented in this paper show that even if the selected case is an approximation of reality, the method is still robust.     

On the Power of Las Vegas for One-Way Communication Complexity, OBDDs, and Finite Automata

The study of the computational power of randomized computations is one of the central tasks of complexity theory. The main goal of this paper is the comparison of the power of Las Vegas computation and deterministic respectively nondeterministic computation. We investigate the power of Las Vegas computation for the complexity measures of one-way communication, ordered binary decision diagrams, and finite automata.(i) For the one-way communication complexity of two-party protocols we show that Las Vegas communication can save at most one half of the deterministic one-way communication complexity. We also present a language for which this gap is tight.(ii) The result (i) is applied to show an at most polynomial gap between determinism and Las Vegas for ordered binary decision diagrams.(iii) For the size (i.e., the number of states) of finite automata we show that the size of Las Vegas finite automata recognizing a language L is at least the square root of the size of the minimal deterministic finite automaton recognizing L. Using a specific language we verify the optimality of this lower bound.     

Working with ARMs: Complexity Results on Atomic Representations of Herbrand Models

An atomic representation of a Herbrand model (ARM) is a finite set of (not necessarily ground) atoms over a given Herbrand universe. Each ARM represents a possibly infinite Herbrand interpretation. This concept has emerged independently in different branches of computer science as a natural and useful generalization of the concept of finite Herbrand interpretation. It was shown that several recursively decidable problems on finite Herbrand models (or interpretations) remain decidable on ARMs.The following problems are essential when working with ARMs: Deciding the equivalence of two ARMs, deciding subsumption between ARMs, and evaluating clauses over ARMs. These problems were shown to be decidable, but their computational complexity has remained obscure so far. The previously published decision algorithms require exponential space. In this paper, we prove that all mentioned problems are coNP-complete.     

An Algebra of Discrete Channels That Involve Combinations of Three Basic Error Types

Recently, the author introduced a nonprobabilistic mathematical model of discrete channels, the BEE channels, that involve the error-types substitution, insertion, and deletion. This paper defines an important class of BEE channels, the SID channels, which include channels that permit a bounded number of scattered errors and, possibly at the same time, a bounded burst of errors in any segment of predefined length of a message. A formal syntax is defined for generating channel expressions, and appropriate semantics is provided for interpreting a given channel expression as a communication channel (SID channel) that permits combinations of substitutions, insertions, and deletions of symbols. Our framework permits one to generalize notions such as error correction and unique decodability, and express statements of the form “The code K can correct all errors of type ξ” and “it is decidable whether the code K is uniquely decodable for the channel described by ξ”, where ξ is any SID channel expression.     

A Real-Time Approach to the Spotting, Representation, and Recognition of Hand Gestures for Human–Computer Interaction

Aiming at the use of hand gestures for human–computer interaction, this paper presents a real-time approach to the spotting, representation, and recognition of hand gestures from a video stream. The approach exploits multiple cues including skin color, hand motion, and shape. Skin color analysis and coarse image motion detection are joined to perform reliable hand gesture spotting. At a higher level, a compact spatiotemporal representation is proposed for modeling appearance changes in image sequences containing hand gestures. The representation is extracted by combining robust parameterized image motion regression and shape features of a segmented hand. For efficient recognition of gestures made at varying rates, a linear resampling technique for eliminating the temporal variation (time normalization) while maintaining the essential information of the original gesture representations is developed. The gesture is then classified according to a training set of gestures. In experiments with a library of 12 gestures, the recognition rate was over 90%. Through the development of a prototype gesture-controlled panoramic map browser, we demonstrate that a vocabulary of predefined hand gestures can be used to interact successfully with applications running on an off-the-shelf personal computer equipped with a home video camera.     

Fuzzy Distance Transform: Theory, Algorithms, and Applications

This paper describes the theory and algorithms of distance transform for fuzzy subsets, called fuzzy distance transform (FDT). The notion of fuzzy distance is formulated by first defining the length of a path on a fuzzy subset and then finding the infimum of the lengths of all paths between two points. The length of a path π in a fuzzy subset of the n-dimensional continuous space ⁿ is defined as the integral of fuzzy membership values along π. Generally, there are infinitely many paths between any two points in a fuzzy subset and it is shown that the shortest one may not exist. The fuzzy distance between two points is defined as the infimum of the lengths of all paths between them. It is demonstrated that, unlike in hard convex sets, the shortest path (when it exists) between two points in a fuzzy convex subset is not necessarily a straight line segment. For any positive number θ≤1, the θ-support of a fuzzy subset is the set of all points in ⁿ with membership values greater than or equal to θ. It is shown that, for any fuzzy subset, for any nonzero θ≤1, fuzzy distance is a metric for the interior of its θ-support. It is also shown that, for any smooth fuzzy subset, fuzzy distance is a metric for the interior of its 0-support (referred to as support). FDT is defined as a process on a fuzzy subset that assigns to a point its fuzzy distance from the complement of the support. The theoretical framework of FDT in continuous space is extended to digital cubic spaces and it is shown that for any fuzzy digital object, fuzzy distance is a metric for the support of the object. A dynamic programming-based algorithm is presented for computing FDT of a fuzzy digital object. It is shown that the algorithm terminates in a finite number of steps and when it does so, it correctly computes FDT. Several potential applications of fuzzy distance transform in medical imaging are presented. Among these are the quantification of blood vessels and trabecular bone thickness in the regime of limited special resolution where these objects become fuzzy.     

Learning Variable-Length Markov Models of Behavior

In recent years there has been an increased interest in the modeling and recognition of human activities involving highly structured and semantically rich behavior such as dance, aerobics, and sign language. A novel approach for automatically acquiring stochastic models of the high-level structure of an activity without the assumption of any prior knowledge is presented. The process involves temporal segmentation into plausible atomic behavior components and the use of variable-length Markov models for the efficient representation of behaviors. Experimental results that demonstrate the synthesis of realistic sample behaviors and the performance of models for long-term temporal prediction are presented.     

Specularities on Surfaces with Tangential Hairs or Grooves

Specularities on surfaces with tangential hairs or grooves are readily observable in nature. Examples of such phenomena are the arched or looped highlights observed on horses and human heads and the linear or curved specularities observed on parts of industrial machinery that have tangential grooves. We investigate the geometry of curvilinear specularities on surfaces of different curvature with tangential hairs or grooves of different orientations under controlled lighting and viewing conditions. First the nature of these specularities is investigated qualitatively. Then specularities on parametric surfaces and hair or groove orientations are calculated for some specific cases. Explicit calculations of specularities on some special surfaces, cylinders, cones, and spheres, are verified by photographs of the reflections. Aspects of the work are applicable to computer graphics and can be utilized for the image interpretation of surface specularities.     

Attentional Scene Segmentation: Integrating Depth and Motion

We present an approach to attention in active computer vision. The notion of attention plays an important role in biological vision. In recent years, and especially with the emerging interest in active vision, computer vision researchers have been increasingly concerned with attentional mechanisms as well. The basic principles behind these efforts are greatly influenced by psychophysical research. That is the case also in the work presented here, which adapts to the model of Treisman (1985, Comput. Vision Graphics Image Process. Image Understanding31, 156–177), with an early parallel stage with preattentive cues followed by a later serial stage where the cues are integrated. The contributions in our approach are (i) the incorporation of depth information from stereopsis, (ii) the simple implementation of low level modules such as disparity and flow by local phase, and (iii) the cue integration along pursuit and saccade mode that allows us a proper target selection based on nearness and motion. We demonstrate the technique by experiments in which a moving observer selectively masks out different moving objects in real scenes.     

Three-Class Markovian Segmentation of High-Resolution Sonar Images

This paper presents an original method for analyzing, in an unsupervised way, images supplied by high resolution sonar. We aim at segmenting the sonar image into three kinds of regions: echo areas (due to the reflection of the acoustic wave on the object), shadow areas (corresponding to a lack of acoustic reverberation behind an object lying on the sea-bed), and sea-bottom reverberation areas. This unsupervised method estimates the parameters of noise distributions, modeled by a Weibull probability density function (PDF), and the label field parameters, modeled by a Markov random field (MRF). For the estimation step, we adopt a maximum likelihood technique for the noise model parameters and a least-squares method to estimate the MRF prior model. Then, in order to obtain an accurate segmentation map, we have designed a two-step process that finds the shadow and the echo regions separately, using the previously estimated parameters. First, we introduce a scale-causal and spatial model called SCM (scale causal multigrid), based on a multigrid energy minimization strategy, to find the shadow class. Second, we propose a MRF monoscale model using a priori information (at different level of knowledge) based on physical properties of each region, which allows us to distinguish echo areas from sea-bottom reverberation. This technique has been successfully applied to real sonar images and is compatible with automatic processing of massive amounts of data.