Unification with Simple Variable Restrictions and Admissibility of $Π_{2}$-rules
Fuente:
arXiv
Salvato in:
| Autori principali: | , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866916275709542400 |
|---|---|
| author | Almeida, Rodrigo Nicolau Ghilardi, Silvio |
| author_facet | Almeida, Rodrigo Nicolau Ghilardi, Silvio |
| contents | We develop a method to recognize admissibility of $Π_{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 $Π_{2}$-rules for many logical systems. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2406_03265 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Unification with Simple Variable Restrictions and Admissibility of $Π_{2}$-rules Almeida, Rodrigo Nicolau Ghilardi, Silvio Logic Logic in Computer Science We develop a method to recognize admissibility of $Π_{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 $Π_{2}$-rules for many logical systems. |
| title | Unification with Simple Variable Restrictions and Admissibility of $Π_{2}$-rules |
| topic | Logic Logic in Computer Science |
| url | https://arxiv.org/abs/2406.03265 |