What you always wanted to know about rigid E-unification

DOI10.1023/A:1005996623714MaRDI QIDQ1382154zbMATH OpenOpenAlexFDO

Authors Anatoli I. Degtyarev, Andrei Voronkov

Publication date 30 August 1998

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1023/a:1005996623714

zbMATH Keywords

rigid \(E\)-unificationtableau method

Mathematics Subject Classification ID

Recommendations

• What you always wanted to know about rigid \(E\)-unification
• scientific article; zbMATH DE number 1552529
• Special cases and substitutes for rigid \(E\)-unification
• scientific article; zbMATH DE number 1761415
• Theorem proving with bounded rigid E-unification

Cited in

(13)

• scientific article; zbMATH DE number 1614698 (Why is no real title available?)
• Free variables and theories: revisiting rigid E-unification
• Theorem proving with bounded rigid E-unification
• Efficient algorithms for bounded rigid E-unification
• scientific article; zbMATH DE number 517077 (Why is no real title available?)
• \(\lim +, \delta^+\), and non-permutability of \(\beta\)-steps
• scientific article; zbMATH DE number 1552529 (Why is no real title available?)
• scientific article; zbMATH DE number 1761415 (Why is no real title available?)
• Lean induction principles for tableaux
• A completion-based method for mixed universal and rigid \(E\)-unification
• What you always wanted to know about rigid \(E\)-unification
• Superposition-based equality handling for analytic tableaux
• Connection tableaux with lazy paramodulation

This page was built for publication: What you always wanted to know about rigid \(E\)-unification

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