Unification modulo -equivalence in a mathematical assistant system

MaRDI QIDQ5015098zbMATH OpenFDO

Authors Temur Kutsia

Publication date 8 December 2021

Full work available at URL http://www.viam.science.tsu.ge/Ami/2020_2/6_kutsia.pdf

zbMATH Keywords

\(\alpha\)-equivalencemathematical assistant systemspermissive nominal unificationsequence variablesTheorema

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Nominal C-unification
• Nominal unification
• Computer Science Logic
• A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols
• An efficient nominal unification algorithm

Cited in

(3)

• Unification modulo lists with reverse relation with certain word equations
• scientific article; zbMATH DE number 1231700 (Why is no real title available?)
• Unranked Nominal Unification

This page was built for publication: Unification modulo \(\alpha\)-equivalence in a mathematical assistant system

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5015098)