Name
Abstract | ||
|---|---|---|
In this paper we present a set of clauses for set theory, thus developing a foundation for the expression of most theorems
of mathematics in a form acceptable to a resolution-based automated theoren prover. Because Gdel's formulation of set theory
permits presentation in a finite number of first-orde formulas, we employ it rather than that of Zermelo-Fraenkel. We illustrate
the expressive power of thi formulation by providing statements of some well-known open questions in number theory, and give
some intuition about how the axioms are used by including some sample proofs. A small set of challeng problems is also given. |
Year | DOI | Venue |
|---|---|---|
1986 | 10.1007/BF02328452 | Journal of Automated Reasoning |
Keywords | Field | DocType |
set theory,automated theorem proving,logic | Set theory,Discrete mathematics,Class (set theory),Finite set,Zermelo–Fraenkel set theory,Axiom,Algorithm,Infinite set,General set theory,Mathematics,Universal set | Journal |
Volume | Issue | ISSN |
2 | 3 | 1573-0670 |
Citations | PageRank | References |
50 | 8.20 | 1 |
Authors | ||
6 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Robert S Boyer | 1 | 1553 | 529.82 |
| Ewing L. Lusk | 2 | 54 | 9.07 |
| William Mccune | 3 | 50 | 8.20 |
| Ross A. Overbeek | 4 | 760 | 234.40 |
| Mark E. Stickel | 5 | 1619 | 292.88 |
| Lawrence Wos | 6 | 301 | 212.69 |