# Automated theorem proving in first-order logic modulo: on the difference between type theory and set theory

Preprint · Gilles Dowek

- Archive id: arxiv:2306.00498
- Published: 2023-06-01
- arXiv: https://arxiv.org/abs/2306.00498
- Source URL: https://arxiv.org/abs/2306.00498
- PDF: https://arxiv.org/pdf/2306.00498
- Provenance: arxiv

## 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.

_Abstract reproduced under CC0-1.0 (arXiv descriptive metadata)._

---
Space Kitty Archive · https://space-kitty.com · API: https://space-kitty.com/api/v1 · MCP: https://space-kitty.com/mcp · Premium: $0.20/request via x402 (Base Sepolia (testnet)). Metadata: arXiv (CC0), OpenAlex (CC0), Europe PMC (CC BY/CC0 works), ClinicalTrials.gov.