Decision procedures for elementary sublanguages of set theory: XII. Multilevel syllogistic extended with singleton and choice operators |
| |
| Authors: | A Ferro |
| |
| Affiliation: | (1) Departimento di Matematica, Università di Catania, V.le Andrea Doria, 6, 95125 Catania, Italy |
| |
| Abstract: | Completeness results and decision algorithms for unquantified theory of sets involving the choice operator are presented. The interest for considering the choice operator is justified by the problem of formalizing transfinite induction in automated theorem proving. |
| |
| Keywords: | Set theory decidability choice operator theorem proving |
| 本文献已被 SpringerLink 等数据库收录！ |
