scientific article; zbMATH DE number 475429

MaRDI QIDQ4273676zbMATH OpenFDO

Authors Jean Gallier

Publication date 31 October 1994

zbMATH Keywords

automated deductionautomated theorem provingdecidabilityNP-completenessSkolem formSkolem- Herbrand-Gödel theoremunification

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 65745
• Unification: a multidisciplinary survey
• scientific article; zbMATH DE number 8800
• A proof theory for general unification
• Theorem proving using equational matings and rigid E -unification

Cited in

(6)

• What is essential unification?
• Formal synthesis of a unification algorithm by the deductive-tableau method
• scientific article; zbMATH DE number 8800 (Why is no real title available?)
• Theorem proving using equational matings and rigid E -unification
• Cyclic connections
• E-unification based on generalized embedding

Describes a project that uses

Uses Software

• ETPS

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 Q4273676)