首页    期刊浏览 2024年11月29日 星期五
登录注册

文章基本信息

  • 标题:A Shallow Embedding of Pure Type Systems into First-Order Logic
  • 本地全文:下载
  • 作者:Lukasz Czajka
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2018
  • 卷号:97
  • 页码:1-39
  • DOI:10.4230/LIPIcs.TYPES.2016.9
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要: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.
  • 关键词:pure type systems; first-order logic; hammers; proof automation; dependent type theory
国家哲学社会科学文献中心版权所有