Automated theorem proving in first-order logic modulo: on the difference between type theory and set theory
Logic in Computer Science
2023-06-02 v1
Abstract
Resolution modulo is a first-order theorem proving method that can be applied both to first-order presentations of simple type theory (also called higher-order logic) and to set theory. When it is applied to some first-order presentations of type theory, it simulates exactly higherorder resolution. In this note, we compare how it behaves on type theory and on set theory.
Cite
@article{arxiv.2306.00498,
title = {Automated theorem proving in first-order logic modulo: on the difference between type theory and set theory},
author = {Gilles Dowek},
journal= {arXiv preprint arXiv:2306.00498},
year = {2023}
}