Nominal Logic with Equations Only
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 firs...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2011-10-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1111.0088v1 |
| id |
doaj-70f95486ea7841eaa56cc7125c027ab6 |
|---|---|
| record_format |
Article |
| spelling |
doaj-70f95486ea7841eaa56cc7125c027ab62020-11-25T01:59:29ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802011-10-0171Proc. LFMTP 2011445710.4204/EPTCS.71.4Nominal Logic with Equations OnlyRanald CloustonMany 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.http://arxiv.org/pdf/1111.0088v1 |
| collection |
DOAJ |
| language |
English |
| format |
Article |
| sources |
DOAJ |
| author |
Ranald Clouston |
| spellingShingle |
Ranald Clouston Nominal Logic with Equations Only Electronic Proceedings in Theoretical Computer Science |
| author_facet |
Ranald Clouston |
| author_sort |
Ranald Clouston |
| title |
Nominal Logic with Equations Only |
| title_short |
Nominal Logic with Equations Only |
| title_full |
Nominal Logic with Equations Only |
| title_fullStr |
Nominal Logic with Equations Only |
| title_full_unstemmed |
Nominal Logic with Equations Only |
| title_sort |
nominal logic with equations only |
| publisher |
Open Publishing Association |
| series |
Electronic Proceedings in Theoretical Computer Science |
| issn |
2075-2180 |
| publishDate |
2011-10-01 |
| description |
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. |
| url |
http://arxiv.org/pdf/1111.0088v1 |
| work_keys_str_mv |
AT ranaldclouston nominallogicwithequationsonly |
| _version_ |
1724964316460875776 |