A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry

被引：0
|
作者：
Fuchs, Laurent [1 ]
Thery, Laurent [2 ]
机构：
[1] Univ Poitiers, XLIM SIC UMR CNRS 6172, Poitiers, France
[2] INRIA Sophia Antipolis, Mediterranee, France
来源：
AUTOMATED DEDUCTION IN GEOMETRY | 2011年 / 6877卷
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
This paper presents a formalization of Grassmann-Cayley algebra [6] that has been done in the COQ [2] proof assistant. The formalization is based on a data structure that represents elements of the algebra as complete binary trees. This allows to define the algebra products recursively. Using this formalization, published proofs of Pappus' and Desargues' theorem [7,1] are interactively derived. A method that automatically proves projective geometric theorems [11] is also translated successfully into the proposed formalization.
引用
收藏
页码：51 / +
页数：3
相关论文
共 50 条
  • [1] Projective geometric theorem proving with Grassmann-Cayley algebra
    Li, Hongbo
    [J]. HERMANN GRASSMANN: FROM PAST TO FUTURE: GRASSMANN'S WORK IN CONTEXT, 2011, : 275 - 285
  • [2] GRASSMANN-CAYLEY ALGEBRA AND ROBOTICS
    WHITE, NL
    [J]. JOURNAL OF INTELLIGENT & ROBOTIC SYSTEMS, 1994, 11 (1-2) : 91 - 107
  • [3] Quadric modeling in a Grassmann-Cayley algebra setting
    Jourdan, F
    [J]. NINTH INTERNATIONAL CONFERENCE ON INFORMATION VISUALISATION, PROCEEDINGS, 2005, : 860 - 865
  • [4] Application of Grassmann-Cayley Algebra to Geometrical Interpretation of Parallel Robot Singularities
    Ben-Horin, Patricia
    Shoham, Moshe
    [J]. INTERNATIONAL JOURNAL OF ROBOTICS RESEARCH, 2009, 28 (01): : 127 - 141
  • [5] AUTOMATIC TESSELLATION OF QUADRIC SURFACES USING GRASSMANN-CAYLEY ALGEBRA
    Jourdan, Frederic
    Hegron, Gerard
    Mace, Pierre
    [J]. COMPUTER VISION AND GRAPHICS (ICCVG 2004), 2006, 32 : 674 - 682
  • [6] Kinestatic analysis of robot manipulators using the Grassmann-Cayley algebra
    Staffetti, E
    [J]. IEEE TRANSACTIONS ON ROBOTICS AND AUTOMATION, 2004, 20 (02): : 200 - 210
  • [7] Singularity analysis of 3T2R parallel mechanisms using Grassmann-Cayley algebra and Grassmann geometry
    Amine, Semaan
    Masouleh, Mehdi Tale
    Caro, Stephane
    Wenger, Philippe
    Gosselin, Clement
    [J]. MECHANISM AND MACHINE THEORY, 2012, 52 : 326 - 340
  • [8] SINGULARITY ANALYSIS OF THE 4-(R)under-barUU PARALLEL MANIPULATOR BASED ON GRASSMANN-CAYLEY ALGEBRA AND GRASSMANN GEOMETRY
    Amine, Semaan
    Masouleh, Mehdi Tale
    Caro, Stephane
    Wenger, Philippe
    Gosselin, Clement
    [J]. PROCEEDINGS OF THE ASME INTERNATIONAL DESIGN ENGINEERING TECHNICAL CONFERENCES AND COMPUTERS AND INFORMATION IN ENGINEERING CONFERENCE - 2011, VOL 6, PTS A AND B, 2012, : 1017 - +
  • [9] Singularity analysis of a class of parallel robots based on Grassmann-Cayley algebra
    Ben-Horin, Patricia
    Shoham, Moshe
    [J]. MECHANISM AND MACHINE THEORY, 2006, 41 (08) : 958 - 970
  • [10] Mobility analysis of overconstrained parallel mechanism using Grassmann-Cayley algebra
    Chai, Xinxue
    Li, Qinchuan
    Ye, Wei
    [J]. APPLIED MATHEMATICAL MODELLING, 2017, 51 : 643 - 654
12345