6 Citations (SciVal)


The purpose of this paper is to explore the question "to what extent could we produce formal, machineverifiable, proofs in real algebraic geometry?" The question has been asked before but as yet the leading algorithms for answering such questions have not been formalised. We present the thesis that a new algorithm for ascertaining satisfiability of formulae over the reals via Cylindrical Algebraic Coverings [Ábrahám, Davenport, England, Kremer, Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driver Search Using Cylindrical Algebraic Coverings, 2020] might provide a trace and outputs that allowthe results to be more susceptible to machine verification than those of competing algorithms.

Original languageEnglish
Pages (from-to)178-188
Number of pages11
JournalCEUR Workshop Proceedings
Publication statusPublished - 31 Dec 2020
EventJoint of the 7th Workshop on Practical Aspects of Automated Reasoning and the 5th Satisfiability Checking and Symbolic Computation Workshop, PAAR+SC-Square 2020 - Virtual, Paris, France
Duration: 5 Jul 2020 → …

Bibliographical note

Publisher Copyright:
© 2020 CEUR-WS. All rights reserved.

Copyright 2020 Elsevier B.V., All rights reserved.

ASJC Scopus subject areas

  • Computer Science(all)


Dive into the research topics of 'New opportunities for the formal proof of computational real geometry? (Extended Abstract)'. Together they form a unique fingerprint.

Cite this