Name
Abstract | ||
|---|---|---|
We present a fully proof-producing implementation of a quantifier elimination procedure for real closed fields. To our knowledge, this is the first generally useful proof-producing implementation of such an algorithm. While many problems within the domain are intractable, we demonstrate convincing examples of its value in interactive theorem proving. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1007/11532231_22 | CADE |
Keywords | Field | DocType |
proof-producing implementation,useful proof-producing implementation,real closed field,proof-producing decision procedure,real arithmetic,quantifier elimination procedure,interactive theorem,interactive theorem proving,quantifier elimination | Quantifier elimination,Discrete mathematics,Real arithmetic,Computer science,Automated theorem proving,Algorithm,Proof theory,Linear arithmetic,Proof assistant | Conference |
Volume | ISSN | ISBN |
3632 | 0302-9743 | 3-540-28005-7 |
Citations | PageRank | References |
36 | 2.86 | 8 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Sean McLaughlin | 1 | 140 | 9.39 |
| John Harrison | 2 | 319 | 24.19 |