
TL;DR
This paper introduces Nominal Equation-only Logic (NEoL), a simplified logic with only equations that is as expressive as Nominal Equational Logic (NEL), facilitating easier translation of results.
Contribution
It presents proof rules for NEoL, an equation-only logic, and proves its expressiveness matches NEL, simplifying reasoning about freshness and equality.
Findings
NEoL is as expressive as NEL
Provides a simple description of equality in empty NEoL-theory
Extends results to describe freshness in empty NEL-theory
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
