On the algebraic formulation of certain geometry statements and mechanical geometry theorem proving

In this paper we analyze the algebraic formulations of certain geometry statements appearing in recent literature related to mechanical geometry theorem proving and give several examples to show that one of these formulations can cause serious problems. We clarify a formulation which is essentially due to W. T. Wu and, in our opinion, is the most satisfactory.     

Automated production of traditional proofs in solid geometry

This paper presents a method of producing readable proofs for theorems in solid geometry. The method is for a class of constructive geometry statements about straight lines, planes, circles, and spheres. The key idea of the method is to eliminate points from the conclusion of a geometric statement using several (fixed) high-level basic propositions about the signed volumes of tetrahedrons and Pythagorean differences of triangles. We have implemented the algorithm, and more than 80 examples from solid geometry have been used to test the program. Our program is efficient and the proofs produced by it are generally short and readable.The work reported here was supported in part by the NSF Grant CCR-9117870 and Chinese National Science Foundation.On leave from Institute of Systems Sciences, Academia Sinica, Beijing 100080, P.R. China.     

基于消点法的几何自动推理系统实现

为了实现几何自动推理的可读性证明,并提高推理效率,介绍了一个基于消点法的可构造性几何命题自动推理系统的设计与实现。该系统提供作图的方式接受用户的几何命题前提条件的输入,可以对初等几何中的大部分可构造性几何问题进行自动证明和求解,并生成可读的证明步骤,大大方便了初高等几何教育和相关研究者的需要。     

Automated development of Tarski's geometry

Tarski's geometry, a complete first-order axiomatization of Euclidean plane geometry, is developed within the automated reasoning system OTTER. Proofs are obtained and performance statistics supplied for most of the challenge problems appearing in the literature. Few of these problems have been previously solved by any clause-based reasoning system. Further challenges are offered.     

On simultaneous optimization of truss geometry and topology

The paper addresses the classical problem of optimal truss design where cross-sectional areas and the positions of joints are simultaneously optimized. Se-veral approaches are discussed from a general point of view. In particular, we focus on the difference between simultaneous and alternating optimization of geometry and topology. We recall a rigorously mathematical approach based on the implicit programming technique which considers the classical single load minimum compliance problem subject to a volume constraint. This approach is refined leading to three new problem formulations which can be treated by methods of Mathematical Programming. In particular, these formulations cover the effect of melting end nodes, i.e., vanishing potential bars due to changes in the geometry. In one of these new problem formulations, the objective function is a polynomial of degree three and the constraints are bilinear or just sign constraints. Because heuristics is avoided, certain optimality properties can be proven for resulting structures. The paper closes with two numerical test examples.     

An algorithm for constructing gr?bner bases from characteristic sets and its application to geometry

In Ritt's method, a prime ideal is given by a characteristic set. A characteristic set of a prime ideal is generally not a set of generators of this ideal. In this paper we present a simple algorithm for constructing Gröbner bases of a prime ideal from its characteristic set. We give a method for finding new theorems in geometry as an application of this algorithm.The first author was supported by NSF Grants Nos. DCR-8503498 and CCR-8702108. The computer facility was supported by the NSF/CER Grant at the University of Texas.     

Optimization methods for truss geometry and topology design

Truss topology design for minimum external work (compliance) can be expressed in a number of equivalent potential or complementary energy problem formulations in terms of member forces, displacements and bar areas. Using duality principles and non-smooth analysis we show how displacements only as well as stresses only formulations can be obtained and discuss the implications these formulations have for the construction and implementation of efficient algorithms for large-scale truss topology design. The analysis covers min-max and weighted average multiple load designs with external as well as self-weight loads and extends to the topology design of reinforcement and the topology design of variable thickness sheets and sandwich plates. On the basis of topology design as an inner problem in a hierarchical procedure, the combined geometry and topology design of truss structures is also considered. Numerical results and illustrative examples are presented.     

Proving geometry theorems with rewrite rules

We investigate the application of rewrite rules to proving theorems from elementary geometry. We have proven 80 theorems, some of them quite difficult. There is a discussion of the formulation of the problem and degenerate conditions. The authors thank the National Science Foundation for its support of the work described in this article.     

Mechanical Geometry Theorem Proving Based on Groebner Bases

A new method for the mechanical elementary geometry theorem proving is presented by using Groebner bases of polynomial ideals.It has two main advantages over the approach proposed in literature:(i)It is complete and not a refutational procdure;(ii) The subcases of the geometry statements which are not generally true can be differentiated clearly.     

A method for the mechanical derivation of formulas in elementary geometry

A method for mechanical derivation of formulas and calculation of quantities in geometry is given with several examples to illustrate its applications.The work described in this article was supported by NSF grant DRC-8503498.     

可由用户持续发展的几何自动推理平台的推理算法

目前的几何定理证明器都不具有可持续性。提出一种结构具有一般性的知识表示和能够统一处理所有规则的推理算法，初步实现了可由用户持续发展的几何自动推理平台。该推理平台允许用户添加几何知识，如几何对象、谓词和规则，并可以综合使用多种推理算法，如前推搜索法和一部分面积法，它将更适合用于几何教学。     

Automated reasoning in geometry theorem proving with Prolog

This paper describes automated reasoning in a PROLOG Euclidean geometry theorem-prover. It brings into focus general topics in automated reasoning and the ability of Prolog in coping with them.     

An introduction to Wu's method for mechanical theorem proving in geometry

Wu's algebraic method for mechanically proving geometry theorems is presented at a level as elementary as possible with sufficient examples for further understanding the complete method.The work reported here was supported by NSF Grant DCR-8503498.     

基于Web的动态几何软件领域模型及其应用

动态几何软件以其动态、直观的特点广泛应用于几何约束作图。针对数据结构缺乏对动态几何领域内可复用的抽象描述的问题,提出一种动态几何软件领域模型的设计方法。首先经过领域分析来识别并划分出最基本的上下文边界,然后通过领域模型设计得到动态几何软件核心领域模型,最后在体系结构建模过程中,在纵向与横向两个维度对动态几何软件进行解耦。实验结果表明,利用该领域模型设计方法研发的动态几何软件能正确地处理图形在临界位置退化的情形。该模型表达的领域知识同时适用于二维及三维的动态几何软件,并支持对不同设备分别设计布局与交互,实现了领域知识的高层次复用。     

Detail-generating geometry completion for point-sampled geometry

In this paper, we present a novel method for detail-generating geometry completion over point-sampled geometry. The main idea consists of converting the context-based geometry completion into the detail-based texture completion on the surface. According to the influence region of boundary points surrounding a hole, a smooth patch covering the hole is first constructed using radial base functions. By applying region-growing clustering to the patch, the patching units for further completion with geometry details is then produced, and using the trilateral filtering operator formulated by us, the geometry-detail texture of each sample point on the input geometry is determined. The geometry details on the smooth completed patch are finally generated by optimizing a constrained global texture energy function on the point-sampled surfaces. Experimental results demonstrate that the method can achieve efficient completed patches that not only conform with their boundaries, but also contain the plausible 3D surface details.     

基于动态几何技术的平面几何资源库检索

在几何资源库中使用传统的方法检索相似的几何题,效果并不理想。对于基于动态几何技术的平面几何资源库,提出使用几何特征量进行相似性检索的方法。几何特征量量化了几何命题中的各几何元素,可以由动态几何作图指令序列提取,该方法能较好地检索相似的几何命题。     

Analyzing group coordination when solving geometry problems with dynamic geometry software

In CSCL research, collaborative activity is conceptualized along various yet intertwined dimensions. When functioning within these multiple dimensions, participants make use of several resources, which can be social or content-related (and sometimes temporal) in nature. It is the effective coordination of these resources that appears to characterize successful collaborative activity. This study proposes a methodological approach for studying coordination of resources when solving geometry problems with dynamic geometry software. The aim is to suggest a methodological lens to capture both the content-related and social discourse within the context of geometry problem solving using dynamic geometry software. As an example, the paper also provides an analysis of a dyad’s face-to-face interaction using the suggested framework.     

Interactive deformable geometry maps

Haptics on 3D deformable models is a challenge because of the inevitable and expensive 3D deformation computation. In this paper, we propose a new technique that extends the conventional rigid geometry images approach proposed by Gu et al. [9]. Our approach not only flattens the geometry, but also helps to accomplish deformation in an effective and efficient manner. Our approach is suitable for haptics computing, as it performs the deformation on the geometry map itself thereby avoiding the expensive 3D deformation computation. We demonstrate construction of the deformable geometry map representation and its application utilizing practical methods for interactive surgery simulation and interactive textile simulation.     

结合仿射几何和正交分解的类中心分类法研究

类中心分类法是非常有效的分类算法。但由于向量空间产生空间扭曲,导致类中心分类法处理某些界限不明显的类别精确度不高。对此引入仿射几何和力的正交分解的方法,提出基于仿射几何和力的正交分解模型的类中心分类法的改进算法。在降低了计算维度的同时解决了由于向量空间特征项维被认为是正交带来的空间扭曲引起的误差。     

A constraint-based dynamic geometry system

Dynamic geometry systems are tools for geometric visualization. They allow the user to define geometric elements, establish relationships between them and explore the dynamic behavior of the remaining geometric elements when one of them is moved. The main problem in dynamic geometry systems is the ambiguity that arises from operations that lead to more than one possible solution. Most dynamic geometry systems deal with this problem in such a way that the solution selection method leads to a fixed dynamic behavior of the system. This is specially annoying when the behavior observed is not the one the user intended.In this work we propose a modular architecture for dynamic geometry systems built upon a set of functional units which will allow us to apply some well-known results from the Geometric Constraint Solving field. A functional unit called filter will provide the user with tools to unambiguously capture the expected dynamic behavior of a given geometric problem.