Nominal Logic with Equations Only
| Autor: | Clouston, Ranald |
|---|---|
| Rok vydání: | 2011 |
| Předmět: | |
| Zdroj: | EPTCS 71, 2011, pp. 44-57 |
| Druh dokumentu: | Working Paper |
| DOI: | 10.4204/EPTCS.71.4 |
| Popis: | Many formal systems, particularly in computer science, may be captured by equations modulated by side conditions asserting the "freshness of names"; these can be reasoned about with Nominal Equational Logic (NEL). Like most logics of this sort NEL employs this notion of freshness as a first class logical connective. However, this can become inconvenient when attempting to translate results from standard equational logic to the nominal setting. This paper presents proof rules for a logic whose only connectives are equations, which we call Nominal Equation-only Logic (NEoL). We prove that NEoL is just as expressive as NEL. We then give a simple description of equality in the empty NEoL-theory, then extend that result to describe freshness in the empty NEL-theory. Comment: In Proceedings LFMTP 2011, arXiv:1110.6685 |
| Databáze: | arXiv |
| Externí odkaz: |
|