Automated development of Tarski's geometry
type: Item
instance of: scholarly article
title: Automated development of Tarski's geometry
zbMATH Open document ID: 0683.68082
DOI: 10.1007/BF00245024
author: Art Quaife
published in: Journal of Automated Reasoning
publication date: 1989-01-01T00:00:00Z
review text: The author uses McCune's automated reasoning system to prove theorems in Euclidean plane geometry within the framework of Tarski's axiomatization (this is a first-order axiomatization which was shown by Tarski to be complete and decidable). McCune's automated reasoning system OTTER is a resolution based theorem prover (hyperresolution was used in most cases) but it is not interactive. The author carefully comments about his choice of weight for retained clauses. He proved various ``challenge problems'' on a VAX 8800 and gives performance statistics for the challenge problems. In addition, he comments briefly upon the performance of a CRAY X-MP/14 and poses further challenge problems.
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03B35
zbMATH DE Number: 4119667
zbMATH Keywords: Tarski's geometry
zbMATH Keywords: mechanical theorem proving
zbMATH Keywords: automated reasoning
zbMATH Keywords: resolution
reviewed by: Christian Fenske
describes a project that uses: OTTER
MaRDI profile type: Publication
full work available at URL: https://doi.org/10.1007/bf00245024
OpenAlex ID: W2011928646
description: scientific article; zbMATH DE number 4119667