A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs

被引：0

作者：

Stojanovic, Sana ^{[1
]}

Pavlovic, Vesna ^{[1
]}

Janicic, Predrag ^{[1
]}

机构：

[1] Univ Belgrade, Fac Math, Belgrade 11000, Serbia

来源：

AUTOMATED DEDUCTION IN GEOMETRY | 2011年 / 6877卷

关键词：

D O I：

暂无

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We present a theorem prover ArgoCLP based on coherent logic that can be used for generating both readable and formal (machine verifiable) proofs in various theories, primarily geometry. We applied the prover to various axiomatic systems and proved tens of theorems from standard university textbooks on geometry. The generated proofs can be used in different educational purposes and can contribute to the growing body of formalized mathematics. The system can be used, for instance, in showing that modifications of some axioms do not change the power of an axiom system. The system can also be used as an assistant for proving appropriately chosen subgoals of complex conjectures.

引用

页码：201 / 220

页数：20

共 23 条

[21] A History-Based Theorem Prover for Intuitionistic Propositional Logic Using Global Caching: IntHistGC System Description
Gore, Rajeev
Thomson, Jimmy
Wu, Jesse
AUTOMATED REASONING, IJCAR 2014, 2014, 8562 : 262 - 268
[22] A general formal memory framework for smart contracts verification based on higher-order logic theorem proving
Yang Z.
Lei H.
International Journal of Performability Engineering, 2019, 15 (11) : 2998 - 3007
[23] Automated Theorem Finding by Forward Reasoning Based on Strong Relevant Logic: A Case Study in Tarski's Geometry
Gao, Hongbiao
Cheng, Jingde
ADVANCED MULTIMEDIA AND UBIQUITOUS ENGINEERING: FUTURETECH & MUE, 2016, 393 : 55 - 61

← 1 2 3 →