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

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

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

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

Research Centre for Computational Science and Mathematical Modelling

Research output: Contribution to conference › Paper › peer-review

37 Downloads (Pure)

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 language	English
Number of pages	5
Publication status	Published - 16 Jul 2021
Event	Third International Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements Workshop - Online Duration: 16 Jul 2021 → 16 Sept 2021 http://cl-informatik.uibk.ac.at/users/swinkler/arcade2021/

Workshop

Workshop	Third International Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements Workshop
Abbreviated title	ARCADE 2021
Period	16/07/21 → 16/09/21
Internet address	http://cl-informatik.uibk.ac.at/users/swinkler/arcade2021/

Access to Document

ADEK21bFinal published version, 288 KB

http://cl-informatik.uibk.ac.at/users/swinkler/arcade2021/pdfs/1.pdf

Cite this

@conference{1b947a868cf547f69f183c5293af0a2a,

title = "Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic",

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.",

author = "E. {\'A}brah{\'a}m and Davenport, {James H.} and Matthew England and Gereon Kremer",

year = "2021",

month = jul,

day = "16",

language = "English",

note = "Third International Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements Workshop , ARCADE 2021 ; Conference date: 16-07-2021 Through 16-09-2021",

url = "http://cl-informatik.uibk.ac.at/users/swinkler/arcade2021/",

}

TY - CONF

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

AU - Ábrahám, E.

AU - Davenport, James H.

AU - England, Matthew

AU - Kremer, Gereon

PY - 2021/7/16

Y1 - 2021/7/16

N2 - 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.

AB - 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.

M3 - Paper

T2 - Third International Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements Workshop

Y2 - 16 July 2021 through 16 September 2021

ER -

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

Abstract

Workshop

Access to Document

Fingerprint

Cite this