arXiv · 2406.03265
Unification with Simple Variable Restrictions and Admissibility of $\Pi_{2}$-rules
Abstract
We develop a method to recognize admissibility of $\Pi_{2}$-rules, relating this problem to a specific instance of the unification problem with linear constants restriction, called here "unification with simple variable restriction". It is shown that for logical systems enjoying an appropriate algebraic semantics and a finite approximation of left uniform interpolation, this unification with simple variable restriction can be reduced to standard unification. As a corollary, we obtain the decidability of admissibility of $\Pi_{2}$-rules for many logical systems.
Explore related subjects
Keep this discovery
Explore connections, maps & timelines
Rodrigo Nicolau Almeida, Silvio Ghilardi. 2024-06-05. Unification with Simple Variable Restrictions and Admissibility of $\Pi_{2}$-rules. https://arxiv.org/abs/2406.03265
Cite the original work for its findings. Save a collection to share your selection of sources.