Paper Info
Title
The undecidability of proof search when equality is a logical connective
Abstract
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.
Year
DOI
Venue
2022
10.1007/s10472-021-09764-0
Annals of Mathematics and Artificial Intelligence
Keywords
DocType
Volume
Equality, Unification, Undecidability, Sequent calculus, 03F03
Journal
90
Issue
ISSN
Citations 
5
1012-2443
0
PageRank 
References 
Authors
0.34
17
2
Name
Order
Citations
PageRank
Dale Miller12485232.26
A Viel200.34