Generic Hermitian quantifier elimination

被引：0

作者：

Dolzmann, A ^{[1
]}

Gilch, LA

机构：

[1] Univ Passau, D-8390 Passau, Germany

[2] Graz Univ Technol, A-8010 Graz, Austria

来源：

ARTIFICIAL INTELLIGENCE AND SYMBOLIC COMPUTATION, PROCEEDINGS | 2004年 / 3249卷

关键词：

D O I：

暂无

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

We present a new method for generic quantifier elimination that uses an extension of Hermitian quantifier elimination. By means of sample computations we show that this generic Hermitian quantifier elimination is, for instance, an important method for automated theorem proving in geometry.

引用

页码：80 / 93

页数：14

共 20 条

[1]

[Anonymous], THESIS U PASSAU PASS

[2]

[Anonymous], 1998, QUANTIFIER ELIMINATI, DOI DOI 10.1007/978-3-7091-9459-1_20

[3]

BECKER E, 1994, CONT MATH, V155, P271

[4]

BROWN CW, 1998, P 1998 INT S SYMB AL, P295

[5]

Chou S.-C., 1988, MECH GEOMETRY THEORE

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

COLLINS, GE ;

HONG, H .

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

[7] Simplification of quantifier-free formulae over ordered fields [J].

Dolzmann, A ;

Sturm, T .

JOURNAL OF SYMBOLIC COMPUTATION, 1997, 24 (02) :209-231

[8] A new approach for automatic theorem proving in real geometry [J].

Dolzmann, A ;

Sturm, T ;

Weispfenning, V .

JOURNAL OF AUTOMATED REASONING, 1998, 21 (03) :357-380

[9]

Dolzmann A, 1999, LECT NOTES ARTIF INT, V1669, P14

[10]

DOLZMANN A, 1997, ACM SIGSAM B, V31, P2, DOI DOI 10.1145/261320.261324

← 1 2 →