The undecidability of proof search when equality is a logical connective

被引：0
|
作者：
Dale Miller
Alexandre Viel
机构：
[1] Inria Saclay & LIX/Ecole Polytechnique,
来源：
Annals of Mathematics and Artificial Intelligence | 2022年 / 90卷
关键词：
Equality; Unification; Undecidability; Sequent calculus; 03F03;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
One proof-theoretic approach to equality in quantificational logic treats equality as a logical connective: in particular, term equality can be given both left and right introduction rules in a sequent calculus proof system. We present a particular example of this approach to equality in a first-order logic setting in which there are no predicate symbols (apart from equality). After we illustrate some interesting applications of this logic, we show that provability in this logic is undecidable.
引用
收藏
页码：523 / 535
页数：12
相关论文
共 50 条
  • [1] The undecidability of proof search when equality is a logical connective
    Miller, Dale
    Viel, Alexandre
    ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE, 2022, 90 (05) : 523 - 535
  • [2] PROOF SEARCH ALGORITHM IN PURE LOGICAL FRAMEWORK
    Vlasov, D. Yu
    SIBERIAN ELECTRONIC MATHEMATICAL REPORTS-SIBIRSKIE ELEKTRONNYE MATEMATICHESKIE IZVESTIYA, 2020, 17 : 988 - 998
  • [3] A purely logical account of sequentiality in proof search
    Bruscoli, P
    LOGICS PROGRAMMING, PROCEEDINGS, 2002, 2401 : 302 - 316
  • [4] Undecidability of Equality for Codata Types
    Berger, Ulrich
    Setzer, Anton
    COALGEBRAIC METHODS IN COMPUTER SCIENCE (CMCS 2018), 2018, 11202 : 34 - 55
  • [5] ON A LOGICAL CHARACTERIZATION OF AXIOMS AND OF UNDECIDABILITY
    HONIG, WM
    SPECULATIONS IN SCIENCE AND TECHNOLOGY, 1990, 13 (01) : 63 - 69
  • [6] A simple proof of the undecidability of inhabitation in λP
    Bezem, Marc
    Springintveld, Jan
    Journal of Functional Programming, 1996, 6 (05): : 757 - 761
  • [7] New proof for the undecidability of the circular PCP
    Halava, Vesa
    Harju, Tero
    ACTA INFORMATICA, 2013, 50 (5-6) : 331 - 341
  • [8] New proof for the undecidability of the circular PCP
    Vesa Halava
    Tero Harju
    Acta Informatica, 2013, 50 : 331 - 341
  • [9] Truth as a Logical Connective
    Yatabe, Shunsuke
    NEW FRONTIERS IN ARTIFICIAL INTELLIGENCE, 2017, 10091 : 166 - 182
  • [10] Logic-Independent Proof Search in Logical Frameworks (Short Paper)
    Kohlhase, Michael
    Rabe, Florian
    Coen, Claudio Sacerdoti
    Schaefer, Jan Frederik
    AUTOMATED REASONING, PT I, 2020, 12166 : 395 - 401
12345