Automated theorem proving in first-order logic module: On the difference between type theory and set theory

Authors
Dowek, G
Citation
G. Dowek, Automated theorem proving in first-order logic module: On the difference between type theory and set theory, LECT N A I, 1761, 2000, pp. 1-22
Citations number
30
Categorie Soggetti
Current Book Contents
Journal title
AUTOMATED DEDUCTION IN CLASSICAL AND NON-CLASSICAL LOGICS → ACNP
ISSN journal
03029743
Volume
1761
Year of publication
2000
Pages
1 - 22
Database
ISI
SICI code
0302-9743(2000)1761:<1:ATPIFL>2.0.ZU;2-L
Abstract
Resolution modulo is a first-order theorem proving method that can be appli ed both to first-order presentations of simple type theory (also called hig her-order logic) and to set theory. When it is applied to some first-order presentations of type theory, it simulates exactly higher-order resolution. In this note, we compare how it behaves on type theory and on set theory.