A complete connection calculus with rigid E-unification

DOI10.1007/BFB0021970MaRDI QIDQ4537435zbMATH OpenFDO

Authors Uwe Petermann

Publication date 30 June 2002

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• What you always wanted to know about rigid \(E\)-unification
• What you always wanted to know about rigid \(E\)-unification
• scientific article; zbMATH DE number 1552529
• scientific article; zbMATH DE number 64168
• Theorem proving with bounded rigid E-unification

Cited in

(10)

• What you always wanted to know about rigid \(E\)-unification
• scientific article; zbMATH DE number 64168 (Why is no real title available?)
• scientific article; zbMATH DE number 517084 (Why is no real title available?)
• scientific article; zbMATH DE number 1950264 (Why is no real title available?)
• Cyclic connections
• What you always wanted to know about rigid \(E\)-unification
• Connection calculus theorem proving with multiple built-in theories
• Simultaneous rigid E-unification is undecidable
• The undecidability of simultaneous rigid E-unification
• Superposition-based equality handling for analytic tableaux

Describes a project that uses

Uses Software

• SETHEO

This page was built for publication: A complete connection calculus with rigid E-unification

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