首页> 外文期刊>urnal of Symbolic Computation >Automated short proof generation for projective geometric theorems with Cayley and bracket algebras Ⅱ. Conic geometry
【24h】

Automated short proof generation for projective geometric theorems with Cayley and bracket algebras Ⅱ. Conic geometry

机译:Cayley和方括号Ⅱ的射影几何定理的自动短证明生成。圆锥几何

获取原文
获取原文并翻译 | 示例
           

摘要

In this paper we study plane conic geometry, particularly different representations of geometric constructions and relations in plane conic geometry, with Cayley and bracket algebras. We propose three powerful simplification techniques for bracket computation involving conic points, and an algorithm for rational Cayley factorization in conic geometry. The factorization algorithm is not a general one, but works for all the examples tried so far. We establish a series of elimination rules for various geometric constructions based on the idea of bracket-oriented representation and elimination, and an algorithm for optimal representation of the conclusion in theorem proving. These techniques can be used in any applications involving brackets and conies. In theorem proving, our algorithm based on these techniques can produce extremely short proofs for difficult theorems in conic geometry.
机译:在本文中,我们使用Cayley和方括号代数研究平面圆锥几何,特别是平面圆锥几何中几何构造和关系的不同表示形式。我们为涉及圆锥点的括号计算提出了三种强大的简化技术,以及一种用于圆锥几何中有理Cayley因式分解的算法。分解算法不是通用算法,但适用于到目前为止尝试的所有示例。我们基于面向括号的表示和消除的思想建立了一系列针对各种几何构造的消除规则,并建立了定理证明中结论的最佳表示的算法。这些技术可用于涉及括号和圆锥形的任何应用程序。在定理证明中,我们基于这些技术的算法可以为圆锥几何中的困难定理提供极短的证明。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号