Nominal logic with equations only

Ranald Clouston*

*Corresponding author for this work

    Research output: Contribution to journalConference articlepeer-review

    2 Citations (Scopus)

    Abstract

    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.

    Original languageEnglish
    Pages (from-to)44-57
    Number of pages14
    JournalElectronic Proceedings in Theoretical Computer Science, EPTCS
    Volume71
    DOIs
    Publication statusPublished - 31 Oct 2011
    Event6th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2011 - Nijmegen, Netherlands
    Duration: 26 Aug 2011 → …

    Fingerprint

    Dive into the research topics of 'Nominal logic with equations only'. Together they form a unique fingerprint.

    Cite this