Towards automated proving in solid geometry

被引:0
|
作者
Simic, Danijela [1 ]
Stojanovic-Durdevic, Sana [1 ]
Tanasijevic, Ivana [1 ]
机构
[1] Univ Belgrade, Fac Math, Dept Comp Sci, Studentski Trg 16, Belgrade 11000, Serbia
关键词
Algebraic methods; Solid geometry; Automated theorem proving; READABLE PROOFS; GENERATION;
D O I
10.1007/s10472-025-09975-9
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
We present an approach for automated theorem proving in 3D solid geometry utilizing multiple algebraic prover engines. Our solution integrates dynamic geometry systems capable of generating solid geometry constructions. We have employed two different methods to transform geometric statements into algebraic representations, while implementing and evaluating these approaches with various theorem provers. Furthermore, we have explored non-degeneracy conditions (NDG) in the context of 3D solid geometry and provided insights into their role in ensuring the validity of geometric relations.
引用
收藏
页数:46
相关论文
共 50 条
  • [1] Towards a Geometry Automated Provers Competition*
    Baeta, Nuno
    Quaresma, Pedro
    Kovacs, Zoltan
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2020, (313): : 93 - 100
  • [2] Finding and Proving New Geometry Theorems in Regular Polygons with Dynamic Geometry and Automated Reasoning Tools
    Kovacs, Zoltan
    INTELLIGENT COMPUTER MATHEMATICS (CICM 2018), 2018, 11006 : 164 - 177
  • [3] AUTOMATED PRODUCTION OF TRADITIONAL PROOFS IN SOLID GEOMETRY
    CHOU, SC
    GAO, XS
    ZHANG, JZ
    JOURNAL OF AUTOMATED REASONING, 1995, 14 (02) : 257 - 291
  • [4] Automated Theorem Proving in GeoGebra: Current Achievements
    Botana, Francisco
    Hohenwarter, Markus
    Janicic, Predrag
    Kovacs, Zoltan
    Petrovic, Ivan
    Recio, Tomas
    Weitzhofer, Simon
    JOURNAL OF AUTOMATED REASONING, 2015, 55 (01) : 39 - 59
  • [5] Inconsistency and its automated proving
    Orzeszek, Piotr
    PHOTONICS APPLICATIONS IN ASTRONOMY, COMMUNICATIONS, INDUSTRY, AND HIGH-ENERGY PHYSICS EXPERIMENTS 2012, 2012, 8454
  • [6] Strategy parallelism in automated theorem proving
    Wolf, A
    Letz, R
    INTERNATIONAL JOURNAL OF PATTERN RECOGNITION AND ARTIFICIAL INTELLIGENCE, 1999, 13 (02) : 219 - 245
  • [7] Proof simplification and automated theorem proving
    Kinyon, Michael
    PHILOSOPHICAL TRANSACTIONS OF THE ROYAL SOCIETY A-MATHEMATICAL PHYSICAL AND ENGINEERING SCIENCES, 2019, 377 (2140):
  • [8] On the Unavoidable Uncertainty of Truth in Dynamic Geometry Proving
    Botana F.
    Recio T.
    Mathematics in Computer Science, 2016, 10 (1) : 5 - 25
  • [9] Automated Deduction and Knowledge Management in Geometry
    Quaresma, Pedro
    MATHEMATICS IN COMPUTER SCIENCE, 2020, 14 (04) : 673 - 692
  • [10] An Empirical Assessment of Progress in Automated Theorem Proving
    Sutcliffe, Geoff
    Suttner, Christian
    Kotthoff, Lars
    Perrault, C. Raymond
    Khalid, Zain
    AUTOMATED REASONING, IJCAR 2024, PT I, 2024, 14739 : 53 - 74