A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL

被引：2

作者：

Kosaian, Katherine ^{[1
]}

Tan, Yong Kiam ^{[1
]}

Platzer, Andre ^{[2
]}

机构：

[1] Carnegie Mellon Univ, Pittsburgh, PA 15213 USA

[2] Karlsruhe Inst Technol, Karlsruhe, Germany

来源：

PROCEEDINGS OF THE 12TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2023 | 2023年

基金：

美国国家科学基金会;

关键词：

quantifier elimination; theorem proving; real arithmetic; multivariate polynomials; CYLINDRICAL ALGEBRAIC DECOMPOSITION;

D O I：

10.1145/3573105.3575672

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We formalize a multivariate quantifier elimination (QE) algorithm in the theorem prover Isabelle/HOL. Our algorithm is complete, in that it is able to reduce any quantified formula in the first-order logic of real arithmetic to a logically equivalent quantifier-free formula. The algorithm we formalize is a hybrid mixture of Tarski's original QE algorithm and the Ben-Or, Kozen, and Reif algorithm, and it is the first complete multivariate QE algorithm formalized in Isabelle/HOL.

引用

页码：211 / 224

页数：14

共 42 条

[21]

Hong H., 1991, COMP SEVERAL DECISIO

[22]

Hupel Lars, 2018, Programming Languages and Systems. 27th European Symposium on Programming, ESOP 2018, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018. Proceedings: LNCS 10801, P999, DOI 10.1007/978-3-319-89884-1_35

[23]

Kosaian Katherine, 2022, Archive of Formal Proofs

[24] Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL [J].

Li, Wenda ;

Passmore, Grant Olney ;

Paulson, Lawrence C. .

JOURNAL OF AUTOMATED REASONING, 2019, 62 (01) :69-91

[25] A Modular, Efficient Formalisation of Real Algebraic Numbers [J].

Li, Wenda ;

Paulson, Lawrence C. .

PROCEEDINGS OF THE 5TH ACM SIGPLAN CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS (CPP'16), 2016, :66-75

[26]

Li Wenda, 2014, Archive of Formal Proofs

[27] Implementing the cylindrical algebraic decomposition within the Coq system [J].

Mahboubi, Assia .

MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2007, 17 (01) :99-127

[28]

McCallum S., 1985, EUROCAL '85. European Conference on Computer Algebra, P277

[29]

McLaughlin S, 2005, LECT NOTES ARTIF INT, V3632, P295

[30]

Narkawicz A, 2018, J FORMALIZ REASON, V11, P19, DOI 10.6092/issn.1972-5787/8212

← 1 2 3 4 5 →