Nominal Logic Programming

TL;DR

This paper explores logic programming based on nominal logic, providing formal semantics and demonstrating its application for reasoning about syntax with bound names, ensuring correct implementation behavior.

Contribution

It develops the model-theoretic, proof-theoretic, and operational semantics for nominal logic programs, establishing a rigorous foundation for their analysis and reasoning.

Findings

Formal semantics for nominal logic programming are established.

Examples demonstrate reasoning about syntax with bound names.

Framework ensures correct implementation behavior.

Abstract

Nominal logic is an extension of first-order logic which provides a simple foundation for formalizing and reasoning about abstract syntax modulo consistent renaming of bound names (that is, alpha-equivalence). This article investigates logic programming based on nominal logic. We describe some typical nominal logic programs, and develop the model-theoretic, proof-theoretic, and operational semantics of such programs. Besides being of interest for ensuring the correct behavior of implementations, these results provide a rigorous foundation for techniques for analysis and reasoning about nominal logic programs, as we illustrate via examples.