What you always wanted to know about rigid E-unification

DOI10.1007/3-540-61630-6_4MaRDI QIDQ5235253zbMATH OpenOpenAlexFDO

Authors Anatoli I. Degtyarev, Andrei Voronkov

Publication date 8 October 2019

Published in Logics in Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-61630-6_4

zbMATH Keywords

automated deductionconnection methodintuitionistic logicnegation normal formtableau method

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• What you always wanted to know about rigid \(E\)-unification
• scientific article; zbMATH DE number 1552529
• scientific article; zbMATH DE number 1761415
• Special cases and substitutes for rigid \(E\)-unification
• A completion-based method for mixed universal and rigid \(E\)-unification

Cites work

• A completion-based method for mixed universal and rigid \(E\)-unification
• An algorithm for reasoning about equality
• An improved proof procedure1
• Basic paramodulation
• Consolution as a framework for comparing calculi
• Gentzen-type systems, resolution and tableaux
• scientific article; zbMATH DE number 3837990 (Why is no real title available?)
• scientific article; zbMATH DE number 4209640 (Why is no real title available?)
• scientific article; zbMATH DE number 15881 (Why is no real title available?)
• scientific article; zbMATH DE number 46359 (Why is no real title available?)
• scientific article; zbMATH DE number 67453 (Why is no real title available?)
• scientific article; zbMATH DE number 3568056 (Why is no real title available?)
• scientific article; zbMATH DE number 1324435 (Why is no real title available?)
• scientific article; zbMATH DE number 1348470 (Why is no real title available?)
• scientific article; zbMATH DE number 517077 (Why is no real title available?)
• scientific article; zbMATH DE number 1761415 (Why is no real title available?)
• scientific article; zbMATH DE number 3236051 (Why is no real title available?)
• scientific article; zbMATH DE number 3266571 (Why is no real title available?)
• scientific article; zbMATH DE number 3274715 (Why is no real title available?)
• scientific article; zbMATH DE number 3299689 (Why is no real title available?)
• scientific article; zbMATH DE number 3344563 (Why is no real title available?)
• scientific article; zbMATH DE number 3349331 (Why is no real title available?)
• scientific article; zbMATH DE number 3415409 (Why is no real title available?)
• Mechanical Theorem-Proving by Model Elimination
• On Matrices with Connections
• Proof-search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification
• Proving Theorems with the Modification Method
• Rigid E-unification: NP-completeness and applications to equational matings
• Simple LPO constraint solving methods
• Special cases and substitutes for rigid \(E\)-unification
• The undecidability of simultaneous rigid E-unification
• Theorem proving using equational matings and rigid E -unification
• Theorem Proving via General Matings
• Theorem proving with ordering and equality constrained clauses
• Theorem proving with variable-constrained resolution
• Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi's Conjecture
• What you always wanted to know about rigid \(E\)-unification

Cited in

(5)

• What you always wanted to know about rigid \(E\)-unification
• scientific article; zbMATH DE number 517077 (Why is no real title available?)
• scientific article; zbMATH DE number 1552529 (Why is no real title available?)
• scientific article; zbMATH DE number 1761415 (Why is no real title available?)
• A completion-based method for mixed universal and rigid \(E\)-unification

Describes a project that uses

Uses Software

• PROTEIN
• 3TAP

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