Vector space representations of words capture many aspects of word similarity, but such methods tend to produce vector spaces in which antonyms (as well as synonyms) are close to each other.For spectral clustering using such word embeddings, words are points in a vector space where synonyms are linked with positive weights, while antonyms are linked with negative weights.We present a new signed spectral normalized graph cut algorithm, signed clustering, that overlays existing thesauri upon distributionally derived vector representations of words, so that antonym relationships between word pairs are represented by negative weights.Our signed clustering algorithm produces clusters of words that simultaneously capture distributional and synonym relations.By using randomized spectral decomposition (Halko et al., 2011) and sparse matrices, our method is both fast and scalable.We validate our clusters using datasets containing human judgments of word pair similarities and show the benefit of using our word clusters for sentiment prediction.

Algorithms for fixed-wing unmanned aerial systems (UAS) must integrate on-board sensor capabilities and vehicle maneuver constraints to reliably satisfy the objectives of persistent surveillance, path planning, and trajectory management. In many cases, the characteristic dimensions of sensor fields of view are comparable with the turning radius of the UAS platform. Consequently, when persistent, full area, time-critical coverage is required and the number of assets is limited, the complexity of path planning is increased, as the turn radius becomes comparable with or exceeds the sensor footprint. A technique is developed to integrate persistent surveillance mission requirements with sensor resolution and field-of-view to facilitate efficient path planning. Graph search techniques and spline-based methods are combined to develop computationally simple algorithms that converge to feasible paths with $G^{2}$ continuity. ( $G^{2}$ continuity in this context means the path, which is constructed from a concatenated series of $C^{2}$ curve segments, and its derivatives are continuous through two derivatives, but the magnitudes of second derivatives may differ at the boundaries, where these curve segments are joined to form the entire path. Curvature is continuous throughout.) Two example cases are provided. In the first, the turning radius is small in comparison with the sensor footprint, while in the second, the minimum turn radius is a critical parameter in the determination of a feasible path.

In this paper, we explore the exponential map and its inverse, the logarithm map, for the group SIM(n) of similarity transformations in ℝnwhich are the composition of a rotation, a translation and a uniform scaling. We give a formula for the exponential map and we prove that it is surjective. We give an explicit formula for the case of n = 3 and show how to efficiently compute the logarithmic map. As an application, we use these algorithms to perform motion interpolation. Given a sequence of similarity transformations, we compute a sequence of logarithms, then fit a cubic spline that interpolates the logarithms and finally, we compute the interpolating curve in SIM(3).

This paper presents two new, efficient solutions to the two-view, relative pose problem from three image point correspondences and one common reference direction. This three-plus-one problem can be used either as a substitute for the classic five-point algorithm, using a vanishing point for the reference direction, or to make use of an inertial measurement unit commonly available on robots and mobile devices where the gravity vector becomes the reference direction. We provide a simple, closed-form solution and a solution based on algebraic geometry which offers numerical advantages. In addition, we introduce a new method for computing visual odometry with RANSAC and four point correspondences per hypothesis. In a set of real experiments, we demonstrate the power of our approach by comparing it to the five-point method in a hypothesize-and-test visual odometry setting.

The problem of finding one-dimensional structures in images and videos can be formulated as a problem of searching for cycles in graphs. In, an untangling-cycle cost function was proposed for identifying persistent cycles in a weighted graph, corresponding to salient contours in an image. We have analyzed their method and give two significant improvements. First, we generalize their cost function to a contour cut criterion and give a computational solution by solving a family of Hermitian eigenvalue problems. Second, we use the idea of a graph circulation, which ensures that each node has a balanced in- and out-flow and permits a natural random-walk interpretation of our cost function. We show that our method finds far more accurate contours in images than. Furthermore, we show that our method is robust to graph compression which allows us to accelerate the computation without loss of accuracy.

It is well known that the resolution method (for propositional logic) is complete. However, completeness proofs found in the literature use an argument by contradiction showing that if a set of clauses is unsatisfiable, then it must have a resolution refutation. As a consequence, none of these proofs actually gives an algorithm for producing a resolution refutation from an unsatisfiable set of clauses. In this note, we give a simple and constructive proof of the completeness of propositional resolution which consists of an algorithm together with a proof of its correctness.

In this paper we give a simple method for drawing a closed rational curve specified in terms of control points as two Bézier segments. The main result is the following: For every affine frame (r,s) (where r ), for every rational curve F(t) specified over [ r,s ] by some control polygon (β 0 , …, β m ) (where the β zero are weighted control points or control vectors), the control points (θ 0 ,… ,θ m (w.r.t.[ r,s ]) of the rational curve G(t) = F(φ(t)) are given by θ i =(-1) i β i , where φ: RP 1 →RP 1 is the projectivity mapping [ r,s ] onto RP 1 -] r,s ]. Thus, in order to draw the entire trace of the curve F over [-∞,+∞], we simply draw the curve segments F [( r,s ]) and G ([ r,s ]). The correctness of the method is established using a simple geometric argument about ways of partitioning the real projective line into two disjoint segments. Other known methods for drawing rational curves can be justified using similar geometric arguments.

It was observed by Curry that when (untyped) λ-terms can be assigned types, for example, simple types, these terms have nice properties (for example, they are strongly normalizing). Coppo, Dezani, and Veneri, introduced type systems using conjunctive types, and showed that several important classes of (untyped) terms can be characterized according to the shape of the types that can be assigned to these terms. For example, the strongly normalizable terms, the normalizable terms, and the terms having head-normal forms, can be characterized in some systems D and DΩ. The proofs use variants of the method of reducibility. In this paper, we present a uniform approach for proving several meta-theorems relating properties of λ-terms and their typability in the systems D and DΩ. Our proofs use a new and more modular version of the reducibility method. As an application of our metatheorems, we show how the characterizations obtained by Coppo, Dezani, Veneri, and Pottinger, can be easily rederived. We also characterize the terms that have weak head-normal forms, which appears to be new. We conclude by stating a number of challenging open problems regarding possible generalizations of the realizability method.

Jean Gallier Department of Computer and Information Science University of Pennsylvania Philadelphia, PA 19104, USA [email protected] Abstract. In this short paper, we consider the practical problem of drawing a closed rational surface speci ed by a net of control points. The main result is that for any rational surface F , the entire surface F can be obtained as the union of the three square patches F (u; v), F v u ; 1 u , and F 1 v ; uv , over [ 1; 1] [ 1; 1]. Furthermore, if F is de ned by some triangular net N (consisting of weighted control points), the control nets of six triangular patches corresponding to the above three square patches can be computed very easily from the original control net. In the full paper [9], we illustrate our method on some classical examples (including the \Steiner roman surface), and we also discuss a method for resolving base points, using some simple \blowing-up technique involving the computation of new control nets.

We define a new class of Kripke structures for the second-order λ-calculus, and investigate the soundness and completeness of some proof systems for proving inequalities (rewrite rules) as well as equations. The Kripke structures under consideration are equipped with preorders that correspond to an abstract form of reduction, and they are not necessarily extensional. A novelty of our approach is that we define these structures directly as functors A: W → Preor equipped with certain natural transformations corresponding to application and abstraction (where W is a preorder, the set of worlds, and Preor is the category of preorders). We make use of an explicit construction of the exponential of functors in the Cartesian-closed category PreorW, and we also define a kind of exponential ΠΦ(As)s ϵ T to take care of type abstraction. However, we strive for simplicity, and we only use very elementary categorical concepts. Consequently, we believe that the models described in this paper are more palatable than abstract categorical models which require much more sophisticated machinery (and are not models of rewrite rules anyway). We obtain soundness and completeness theorems that generalize some results of Mitchell and Moggi to the second-order λ-calculus, and to sets of inequalities (rewrite rules).

The main purpose of this paper is to take apart the reducibility method in order to understand how its pieces fit together, and in particular, to recast the conditions on candidates of reducibility as sheaf conditions. There has been a feeling among experts on this subject that it should be possible to present the reducibility method using more semantic means, and that a deeper understanding would then be gained. This paper gives mathematical substance to this feeling, by presenting a generalization of the reducibility method based on a semantic notion of realizability which uses the notion of a cover algebra (as in abstract sheaf theory). A key technical ingredient is the introduction of a new class of semantic structures equipped with preorders, called pre-applicative structures. These structures need not be extensional. In this framework, a general realizability theorem can be shown. Kleene's recursive realizability and a variant of Kreisel's modified realizability both fit into this framework. We are then able to prove a metatheorem which shows that if a property of realizers satisfies some simple conditions, then it holds for the semantic interpretations of all terms. Applying this theorem to the special case of the term model, yields a general theorem for proving properties of typed λ-terms, in particular, strong normalization and confluence. This approach clarifies the reducibility method by showing that the closure conditions on candidates of reducibility can be viewed as sheaf conditions. The above approach is applied to the simply-typed λ-calculus (with types →, ×, +, and ⊥), and to the second-order (polymorphic) λ-calculus (with types → and ∀2), for which it yields a new theorem.

We study combinations of many-sorted algebraic term rewriting systems and polymorphic lambda term rewriting. Algebraic and lambda terms are mixed by adding the symbols of the algebraic signature to the polymorphic lambda calculus as higher-order constants. We show that if a many-sorted algebraic rewrite system R has the Church-Rosser property (is confluent), then R + β + type-β + type-η rewriting of mixed terms has the Church-Rosser property too. η reduction does not commute with algebraic reduction, in general. However, using long normal forms, we show that if R is canonical (confluent and strongly normalizing) then equational provability from R + β + η type-β + type-η is still decidable.

In this paper, it is shown that there is an algorithm that, given by finite set E of ground equations, produces a reduced canonical rewriting system R equivalent to E in polynomial time. This algorithm based on congruence closure performs simplification steps guided by a total simplification ordering on ground terms, and it runs in time O(n 3 ) .

The purpose of this paper is to give an exposition of material dealing with constructive logics, typed λ-calculi, and linear logic. The emergence in the past ten years of a coherent field of research often named “logic and computation” has had two major (and related) effects: firstly, it has rocked vigorously the world of mathematical logic; secondly, it has created a new computer science discipline, which spans a range of subjects from what is traditionally called the theory of computation, to programming language design. Remarkably, this new body of work relies heavily on some “old” concepts found in mathematical logic, like natural deduction, sequent calculus, and λ-calculus (but often viewed in a different light), and also on some newer concepts. Thus, it may be quite a challenge to become initiated to this new body of work (but the situation is improving, and there are now some excellent texts on this subject matter). This paper attempts to provide a coherent and hopefully “gentle” initiation to this new body of work. We have attempted to cover the basic material on natural deduction, sequent calculus, and typed λ-calculus, but also to provide an introduction to Girard's linear logic, one of the most exciting developments in logic these past six years. The first part of these notes gives an exposition of the background material (with some exceptions, such as “contraction-free” systems for intuitionistic propositional logic and the Girard translation of classical logic into intuitionistic logic, which is new). The second part is devoted to more current topics such as linear logic, proof nets, the geometry of interaction, and unified systems of logic (LU).

In this paper, it is shown that the method of matings due to Andrews and Bibel can be extended to (first-order) languages with equality. A decidable version of E -unification called rigid E-unification is introduced, and it is shown that the method of equational matings remains complete when used in conjunction with rigid E -unification. Checking that a family of mated sets is an equational mating is equivalent to the following restricted kind of E -unification. Problem Given E → ={E i | 1≤i≤n} a family of n finite sets of equations and S={〈u i ,v i 〉 |1≤i≤n} a set of n pairs of terms, is there a substitution θ such that, treating each set θ(E i ) as a set of ground equations (i.e., holding the variables in θ(E i ) “rigid”), θ(u i ), and θ(v i ) are provably equal from θ(E i ) for i=1,...,n? Equivalently, is there a substitution θ such that θ(u i ) and θ(v i ) can be shown congruent from θ(E i ) by the congruence closure method for i=1,...,n? A substitution θ solving the above problem is called a rigid E → -unifier of S , and a pair 〈E → ,S〉 such that S has some rigid E → -unifier is called an equational premating. It is shown that deciding whether a pair 〈 E → ,S〉is an equational premating is an NP-complete problem.

We study combinations of many-sorted algebraic term rewriting systems and polymorphic lambda term rewriting. Algebraic and lambda terms are mixed by adding the symbols of the algebraic signature to the polymorphic lambda calculus, as higher-order constants. We show that if a many-sorted algebraic rewrite system R is strongly normalizing (terminating, noetherian), then R + β + η + type-β + type-η rewriting of mixed terms is also strongly normalizing. The result is obtained using a technique which generalizes Girard's “candidats de reductibilité”, introduced in the original proof of strong normalization for the polymorphic lambda calculus.

Rigid E-unification is a restricted kind of unification modulo equational theories, or E-unification, that arises naturally in extending Andrew's theorem proving method of matings to first-order languages with equality. This extension was first presented by J. H. Gallier, S. Raatz, and W. Snyder, who conjectured that rigid E-unification is decidable. In this paper, it is shown that rigid E-unification is NP-complete and that finite complete sets of rigid E-unifiers always exist. As a consequence, deciding whether a family of mated sets is an equational mating is an NP-complete problem. Some implications of this result regarding the complexity of theorem proving in first-order logic with equality are also discussed.

In this paper, we reexamine the problem of general higher-order unification and develop an approach based on the method of transformations on systems of terms which has its roots in Herbrand's thesis, and which was developed by Martelli and Montanari in the context of first-order unification. This method provides an abstract and mathematically elegant means of analyzing the invariant properties of unification in various settings by providing a clean separation of the logical issues from the specification of procedural information. Our major contribution is three-fold. First, we have extended the Herbrand-Martelli-Montanari method of transformations on systems to higher-order unification and pre-unification; second, we have used this formalism to provide a more direct proof of the completeness of a method for higher-order unification than has previously been available; and, finally, we have shown the completeness of the strategy of eager variable elimination. In addition, this analysis provides another justification of the design of Huet's procedure, and shows how its basic principles work in a more general setting. Finally, it is hoped that this presentation might form a good introduction to higher-order unification for those readers unfamiliar with the field.

This paper is concerned with E-unification in arbitrary equational theories. We extend the method of transformations on systems of terms, developed by Martelli-Montanari for standard unification, to E-unification by giving two sets of transformation, BJ and J, which are proved to be sound and complete in the sense that a complete set of E-unifiers for any equational theory E can be enumerated by either of these sets. The set J is an inprovement of BJ, in that many E-unifiers produced by BJ will be weeded out by J. In addition, we show that a generalization of surreduction (also called narrowing) combined with the computation of critical pairs is complete. A new representation of equational proofs as certain kinds of trees is used to prove the completeness of the set BJ in a rather direct fashion that parallels the completeness of the transformations in the case of (standard) unification. The completeness of J and the generalization of surreduction is proved by a method inspired by the concept of unfailing completion, using an abstract (and simpler) notion of the completion of a set of equations.

Rigid E-unification is a restricted kind of unification modulo equational theories, or E-unification, that arises naturally in extending P. Andrews' (1981) theorem-proving method of mating to first-order languages with equality. It is shown that rigid E-unification is NP-complete and that finite complete sets of rigid E-unifiers always exist. As a consequence, deciding whether a family of mated sets is an equational mating is an NP-complete problem. Some implications of this result regarding the complexity of theorem proving in first-order logic with equality are discussed.>

This paper presents two fast algorithms for testing the unsatisfiability of a set of ground Horn clauses with or without equational atomic formulae. If the length of the set H of Horn clauses (viewed as the string obtained by concatenating the clauses in H) is n, it is possible to design an algorithm running in time O(n log(n)). These algorithms are obtained by generalising the concept of congruence closure to ground Horn clauses. The basic idea behind these algorithms is that the congruence closure induced by a set of ground Horn clauses can be obtained by interleaving steps in which an equational congruence closure is computed, and steps in which an implicational type of closure is computed.

A (strict) hierarchy of algebras in which only certain “constructive” chains have a least upper bound is studied. Such algebras, called n-rational, are “ideal” interpretations for finite recursion schemes of higher types. Indeed, the constructive chains that have least upper bounds in these algebras are obtained by unfolding rational recursion schemes of higher types. Part I of this paper deals with basic properties of these algebras, the existence of free algebras in particular. In Part II [SIAM J. Comput., 13 (1984), pp. 776–794.], varieties and a logic of inequalities are studied. A proof system with one infinitary inference rule is shown to be complete.

This work is a continuation of the study of n-rational algebras initiated in the first part of this paper [SIAM J. Comput.,13 (1984), pp.750–775.]. In this second part, varieties of n-rational algebras satisfying a set of inequalities and the corresponding logic are investigated. It is shown that there is a bijective Galois connection between such varieties, called semi-varieties, and “fully invariant” n-rational precongruences. A deductive system for proving inequalities in which a proof is represented as a well-founded tree is shown to be sound and complete. This proof system uses one infinitary inference rule, the “lub rule”. A “Birkhoff variety theorem” is also proved for semi-varieties. The relationship between this approach in which classes of interpretations are semi-varieties of n-rational algebras, and the approach in which $\omega $-continuous algebras are used (Courcelle, Nivat, Guessarian) is also briefly explored.

An essential part of any interactive programming development system is an incremental parser capable of error recovery. This paper presents a general incremental parser for LR(1) grammars allowing several/any form of modifications in the input program. The parser is suplemented with error recovery routines using an error automaton. Errors can be corrected automatically by recovery routines, or by the user at his request.