2026-07-26T02:45:50Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:9853 2024-03-06T10:42:24Z ddc:004 open_access

A Shallow Embedding of Pure Type Systems into First-Order Logic Czajka, Lukasz pure type systems first-order logic hammers proof automation dependent type theory We define a shallow embedding of logical proof-irrelevant Pure Type Systems (piPTSs) into minimal first-order logic. In logical piPTSs a distinguished sort *^p of propositions is assumed. Given a context Gamma and a Gamma-proposition tau, i.e., a term tau such that Gamma |- tau : *^p, the embedding translates tau and Gamma into a first-order formula F_Gamma(tau) and a set of first-order axioms Delta_Gamma. The embedding is not complete in general, but it is strong enough to correctly translate most of piPTS propositions (by completeness we mean that if Gamma |- M : tau is derivable in the piPTS then F_Gamma(tau) is provable in minimal first-order logic from the axioms Delta_Gamma). We show the embedding to be sound, i.e., if F_Gamma(tau) is provable in minimal first-order logic from the axioms Delta_Gamma, then Gamma |- M : tau is derivable in the original system for some term M. The interest in the proposed embedding stems from the fact that it forms a basis of the translations used in the recently developed CoqHammer automation tool for dependent type theory. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Lukasz Czajka 2018 Is Part Of LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2016.9 urn:nbn:de:0030-drops-98533 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.9 eng https://creativecommons.org/licenses/by/3.0/legalcode