Special cases and substitutes for rigid E-unification

DOI10.1007/S002000050001MaRDI QIDQ1961709zbMATH OpenOpenAlexFDO

Authors David A. Plaisted

Publication date 5 March 2000

Published in Applicable Algebra in Engineering, Communication and Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s002000050001

zbMATH Keywords

decidabilityfirst-order logicundecidabilitytableauxHorn clausessimultaneous rigid \(E\)-unificationdecidable versiontheorem proving with equality

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Recommendations

• The undecidability of simultaneous rigid E-unification
• scientific article; zbMATH DE number 1552529
• Monadic simultaneous rigid E-unification
• Monadic simultaneous rigid \(E\)-unification and related problems
• scientific article; zbMATH DE number 1088208

Cited in

(11)

• Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem
• Simultaneous rigid E-unification is undecidable
• Decidability and complexity of simultaneous rigid E-unification with one variable and related results
• scientific article; zbMATH DE number 1189062 (Why is no real title available?)
• Theorem proving with bounded rigid \(E\)-unification
• Proof-search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification
• Monadic simultaneous rigid \(E\)-unification and related problems
• scientific article; zbMATH DE number 1552529 (Why is no real title available?)
• Free variables and theories: revisiting rigid \(E\)-unification
• What you always wanted to know about rigid \(E\)-unification
• Monadic simultaneous rigid E-unification

This page was built for publication: Special cases and substitutes for rigid \(E\)-unification

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