Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic

E. Ábrahám, James H. Davenport, Matthew England, Gereon Kremer

Research output: Contribution to conferencePaperpeer-review

Abstract

We discuss the topic of unsatisfiability proofs in SMT, particularly with reference to quantifier free non-linear real arithmetic. We outline how the methods here do not admit trivial proofs and how past formalisation attempts are not sufficient. We note that the new breed of local search based algorithms for this domain may offer an easier path forward.
Original languageEnglish
Number of pages5
Publication statusPublished - 16 Jul 2021
EventThird International Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements Workshop - Online
Duration: 16 Jul 202116 Sep 2021
http://cl-informatik.uibk.ac.at/users/swinkler/arcade2021/

Workshop

WorkshopThird International Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements Workshop
Abbreviated titleARCADE 2021
Period16/07/2116/09/21
Internet address

Fingerprint

Dive into the research topics of 'Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic'. Together they form a unique fingerprint.

Cite this