scientific article; zbMATH DE number 3688778

MaRDI QIDQ3883563zbMATH OpenFDO

Authors Jörg H. Siekmann

Publication date 1979

zbMATH Keywords

matchingunification algorithm for terms involving a commutative functionunification problem

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Symbolic computation and algebraic computation (68W30)

Cited in

(6)

• Deciding the word problem for ground and strongly shallow identities w.r.t. extensional symbols
• A formalisation of nominal C-matching through unification with protected variables
• What is essential unification?
• Formalising nominal C-unification generalised with protected variables
• Decidability of confluence and termination of monadic term rewriting systems
• The unification type of an equational theory may depend on the instantiation preorder

This page was built for publication:

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