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 条

[1]

Basu S, 2006, ALGORITHMS REAL ALGE, V10, DOI [DOI 10.1007/3-540-33099-2, 10.1007/3-540-33099-2]

[2] THE COMPLEXITY OF ELEMENTARY ALGEBRA AND GEOMETRY [J].

BENOR, M ;

KOZEN, D ;

REIF, J .

JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 1986, 32 (02) :251-264

[3]

Brown C. W., 2003, SIGSAM Bulletin, V37, P97, DOI 10.1145/968708.968710

[4] Improved projection for cylindrical algebraic decomposition [J].

Brown, CW .

JOURNAL OF SYMBOLIC COMPUTATION, 2001, 32 (05) :447-465

[5] IMPROVED ALGORITHMS FOR SIGN DETERMINATION AND EXISTENTIAL QUANTIFIER ELIMINATION [J].

CANNY, J .

COMPUTER JOURNAL, 1993, 36 (05) :409-418

[6]

Cohen C., 2021, PREPRINT, DOI 10.

[7]

Cohen C., 2012, THESIS ECOLE POLYTEC

[8] FORMAL PROOFS IN REAL ALGEBRAIC GEOMETRY: FROM ORDERED FIELDS TO QUANTIFIER ELIMINATION [J].

Cohen, Cyril ;

Mahboubi, Assia .

LOGICAL METHODS IN COMPUTER SCIENCE, 2012, 8 (01)

[9]

Collins G. E., 1975, Automata Theory and Formal Language 2nd GI Conference, P134

[10] PARTIAL CYLINDRICAL ALGEBRAIC DECOMPOSITION FOR QUANTIFIER ELIMINATION [J].

COLLINS, GE ;

HONG, H .

JOURNAL OF SYMBOLIC COMPUTATION, 1991, 12 (03) :299-328

← 1 2 3 4 5 →