Nominal unification with atom-variables
From MaRDI portal
Publication:1640638
DOI10.1016/j.jsc.2018.04.003zbMath1395.68096MaRDI QIDQ1640638
Yunus D. K. Kutz, David Sabel, Manfred Schmidt-Schauss
Publication date: 14 June 2018
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jsc.2018.04.003
68Q25: Analysis of algorithms and problem complexity
68Q42: Grammars and rewriting systems
68Q17: Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Related Items
Unnamed Item, Nominal Unification and Matching of Higher Order Expressions with Recursive Let, Rewriting with generalized nominal unification, Ground confluence and strong commutation modulo alpha-equivalence in nominal rewriting, Confluence and commutation for nominal rewriting systems with atom-variables, Nominal unification with letrec and environment-variables
Uses Software
Cites Work
- Equivariant unification
- A polynomial nominal unification algorithm
- Isabelle/HOL. A proof assistant for higher-order logic
- Checking overlaps of nominal rewriting rules
- Nominal unification of higher order expressions with recursive let
- Nominal Sets
- Unifying Nominal Unification
- Constraint solving in non-permutative nominal abstract syntax
- Safety of Nöcker's strictness analysis
- An Efficient Unification Algorithm
- Computer Science Logic
- An Efficient Nominal Unification Algorithm
- The complexity of satisfiability problems
- Automata, Languages and Programming
- General Bindings and Alpha-Equivalence in Nominal Isabelle
- Nominal Unification from a Higher-Order Perspective