Combinatorial analysis of proofs in projective and affine geometry

The axioms of projective and affine plane geometry are turned into rules of proof by which formal derivations are constructed. The rules act only on atomic formulas. It is shown that proof search for the derivability of atomic cases from atomic assumptions by these rules terminates (i.e., solves the word problem). This decision method is based on the central result of the combinatorial analysis of derivations by the geometric rules: The geometric objects that occur in derivations by the rules can be restricted to those known from the assumptions and cases. This “subterm property” is proved by permuting suitably the order of application of the geometric rules. As an example of the decision method, it is shown that there cannot exist a derivation of Euclid’s fifth postulate if the rule that corresponds to the uniqueness of the parallel line construction is taken away from the system of plane affine geometry.     

Combinatorial analysis of proofs in projective and affine geometry

The axioms of projective and affine plane geometry are turned into rules of proof by which formal derivations are constructed. The rules act only on atomic formulas. It is shown that proof search for the derivability of atomic cases from atomic assumptions by these rules terminates (i.e., solves the word problem). This decision method is based on the central result of the combinatorial analysis of derivations by the geometric rules: The geometric objects that occur in derivations by the rules can be restricted to those known from the assumptions and cases. This “subterm property” is proved by permuting suitably the order of application of the geometric rules. As an example of the decision method, it is shown that there cannot exist a derivation of Euclid’s fifth postulate if the rule that corresponds to the uniqueness of the parallel line construction is taken away from the system of plane affine geometry.     

Using Gale transforms in computational geometry

LetP denote a set ofn d+1 points ind-space ^d . A Gale transform ofP assigns to each point inP a vector in space ^n-d-1 such that the resultingn-tuple of vectors reflects all affinely invariant properties ofP. First utilized by Gale in the 1950s, Gale transforms have been recognized as a powerful tool in combinatorial geometry.This paper introduces Gale transforms to computational geometry. It offers a direct algorithm for their construction and addresses applications to convex hull and visibility problems. An application to scene analysis is worked out in detail.     

Structural stability and dynamic geometry: Some ideas on situated proofs

In this paper we survey the historical and contemporary connections in mathematics between classical “conceptual” tools versus modern computing tools. In this process we highlight the interplay between the inductive and deductive, experimental and theoretical, and propose the notion of Situated proofs as a didactic tool for the teaching of geometry in the 21^st century.     

New applications of random sampling in computational geometry

This paper gives several new demonstrations of the usefulness of random sampling techniques in computational geometry. One new algorithm creates a search structure for arrangements of hyperplanes by sampling the hyperplanes and using information from the resulting arrangement to divide and conquer. This algorithm requiresO(s ^d+ ) expected preprocessing time to build a search structure for an arrangement ofs hyperplanes ind dimensions. The expectation, as with all expected times reported here, is with respect to the random behavior of the algorithm, and holds for any input. Given the data structure, and a query pointp, the cell of the arrangement containingp can be found inO(logs) worst-case time. (The bound holds for any fixed >0, with the constant factors dependent ond and .) Using point-plane duality, the algorithm may be used for answering halfspace range queries. Another algorithm finds random samples of simplices to determine the separation distance of two polytopes. The algorithm uses expectedO(n ^[d/2]) time, wheren is the total number of vertices of the two polytopes. This matches previous results [10] for the cased = 3 and extends them. Another algorithm samples points in the plane to determine their orderk Voronoi diagram, and requires expectedO(s ¹⁺ k) time fors points. (It is assumed that no four of the points are cocircular.) This sharpens the boundO(sk ² logs) for Lee's algorithm [21], andO(s ² logs+k(s–k) log² s) for Chazelle and Edelsbrunner's algorithm [4]. Finally, random sampling is used to show that any set ofs points inE ³ hasO(sk ² log⁸ s/(log logs)⁶) distinctj-sets withjk. (ForS E ^d , a setS S with |S| =j is aj-set ofS if there is a half-spaceh ⁺ withS =S h ⁺.) This sharpens with respect tok the previous boundO(sk ⁵) [5]. The proof of the bound given here is an instance of a probabilistic method [15].A preliminary version of this paper appeared in theProceedings of the 18th Annual ACM Symposium on Theory of Computing, Berkeley, CA, 1986.     

On computational proofs of the existence of solutions to nonlinear parabolic problems

This paper is an extension of the preceding study (Nakao, this journal, 1991) in which we described a numerical verification method of the solution for one-space dimensional parabolic problems, to the several-space dimensional case. Here, numerical verification means the automatic proof of the existence of solutions to the problems by some numerical techniques on a computer. We reformulate the verification condition for nonlinear parabolic initial boundary value problems using the fixed-point problem of a compact operator on certain function spaces. As in the preceding study based upon a simple C⁰ finite-element approximation and its constructive a priori error estimates, a numerical verification procedure is presented with some numerical examples.     

Applications of random sampling in computational geometry,II

We use random sampling for several new geometric algorithms. The algorithms are Las Vegas, and their expected bounds are with respect to the random behavior of the algorithms. These algorithms follow from new general results giving sharp bounds for the use of random subsets in geometric algorithms. These bounds show that random subsets can be used optimally for divide-and-conquer, and also give bounds for a simple, general technique for building geometric structures incrementally. One new algorithm reports all the intersecting pairs of a set of line segments in the plane, and requiresO(A+n logn) expected time, whereA is the number of intersecting pairs reported. The algorithm requiresO(n) space in the worst case. Another algorithm computes the convex hull ofn points inE ^d inO(n logn) expected time ford=3, andO(n ^[d/2]) expected time ford>3. The algorithm also gives fast expected times for random input points. Another algorithm computes the diameter of a set ofn points inE ³ inO(n logn) expected time, and on the way computes the intersection ofn unit balls inE ³. We show thatO(n logA) expected time suffices to compute the convex hull ofn points inE ³, whereA is the number of input points on the surface of the hull. Algorithms for halfspace range reporting are also given. In addition, we give asymptotically tight bounds for (k)-sets, which are certain halfspace partitions of point sets, and give a simple proof of Lee's bounds for high-order Voronoi diagrams.     

On the role of kinesthetic thinking in computational geometry

Computational geometry is a new (about 30 years) and rapidly growing branch of knowledge in computer science that deals with the analysis and design of algorithms for solving geometric problems. These problems typically arise in computer graphics, image processing, computer vision, robotics, manufacturing, knot theory, polymer physics and molecular biology. Since its inception many of the algorithms proposed for solving geometric problems, published in the literature, have been found to be incorrect. These incorrect algorithms rather than being ‘purely mathematical’ often contain a strong kinesthetic component. This paper explores the relationship between computational geometric thinking and kinesthetic thinking, the effect of the latter on the correctness and efficiency of the resulting algorithms, and their implications for education.     

Applications of random sampling to on-line algorithms in computational geometry

This paper presents a general framework for the design and randomized analysis of geometric algorithms. These algorithms are on-line and the framework provides general bounds for their expected space and time complexities when averaging over all permutations of the input data. The method is general and can be applied to various geometric problems. The power of the technique is illustrated by new efficient on-line algorithms for constructing convex hulls and Voronoi diagrams in any dimension, Voronoi diagrams of line segments in the plane, arrangements of curves in the plane, and others. This work has been supported in part by the ESPRIT Basic Research Action Nr. 3075 (ALCOM).     

Charged ball method for solving some computational geometry problems

The concept of replacement of the initial stationary optimization problem with some nonstationary mechanical system tending with time to the position of equilibrium, which coincides with the solution of the initial problem, makes it possible to construct effective numerical algorithms. First, differential equations of the movement should be derived. Then we pass to the difference scheme and define the iteration algorithm. There is a wide class of optimization methods constructed in such a way. One of the most known representatives of this class is the heavy ball method. As a rule, such type of algorithms includes parameters that highly affect the convergence rate. In this paper, the charged ball method, belonging to this class, is proposed and investigated. It is a new effective optimization method that allows solving some computational geometry problems. A problem of orthogonal projection of a point onto a convex closed set with a smooth boundary and the problem of finding the minimum distance between two such sets are considered in detail. The convergence theorems are proved, and the estimates for the convergence rate are found. Numerical examples illustrating the work of the proposed algorithms are given.     

Randomized proofs in arithmetic

A randomized proof system for arithmetic is introduced. A proof of an arithmetical formula is defined as its derivation from the axioms of arithmetic by the standard rules of inference of arithmetic and also one more rule which we call the random substitution rule. Such proofs can be regarded as a special kind of interactive proof and, more exactly, as a special kind of the Arthur-Merlin proofs. The main result of the paper shows that a proof in arithmetic with the random substitution rule can be considerably shorter than an arithmetical proof of the same formula. Namely, there exists a set of formulas such that (i) these formulas are provable in arithmetic but, unless PSPACE=NP, do not have polynomially long proofs; (ii) these proofs have polynomially long proofs in arithmetic with random substitution (whatever random numbers appear) and the probability of error of these proofs is exponentially small. Bibliography: 10 titles. Translated fromZapiski Nauchnykh Seminarov POMI, Vol. 220, 1995, pp. 49–71. Translated by E. Ya. Dantsin.     

Students’ understanding of mathematical objects in the context of transformational geometry: Implications for constructing and understanding proofs

This research explored students’ views of geometric objects through the implementation of a curriculum module that allowed them to explore the relationships between transformational geometry and linear algebra. The majority of the students were middle and secondary mathematics education majors enrolled in a one-semester geometry course that is aimed at prospective teachers. A preponderance of the evidence suggests that the participating students, for the most part, viewed isometries operationally and viewed geometric objects (triangle, etc.) as “perceived.” Results also suggest that these two views influenced the students’ abilities to understand and to construct geometric proofs in transformational geometry.     

Cutting-plane proofs in polynomial space

Following Chvátal, cutting planes may be viewed as a proof system for establishing that a given system of linear inequalities has no integral solution. We show that such proofs may be carried out in polynomial workspace.Research supported by Sonderforschungsbereich 303 (DFG), Institut für Operations Research, Universität Bonn, FR Germany and by NSF grant ECS-8611841.