Automated theorem proving in first-order logic modulo: on the difference between type theory and set theory
Résumé
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.
Domaines
Logique en informatique [cs.LO]
Origine : Fichiers produits par l'(les) auteur(s)