Theorem proving using equational matings and rigid E -unification

DOI10.1145/128749.128754zbMath0799.68171OpenAlexW1999336350MaRDI QIDQ4302815

Stan Raatz, Jean H. Gallier, Paliath Narendran, Wayne Snyder

Publication date: 13 November 1994

Published in: Journal of the ACM (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/128749.128754

zbMATH Keywords

theorem provingNP- complete\(E\)-unificationmatingsequational premating

Mathematics Subject Classification ID

Related Items (16)

Theorem Proving with Bounded Rigid E-Unification ⋮ Efficient ground completion ⋮ Efficient Algorithms for Bounded Rigid E-unification ⋮ KoMeT ⋮ Superposition-based equality handling for analytic tableaux ⋮ TPS: A theorem-proving system for classical type theory ⋮ Free Variables and Theories: Revisiting Rigid E-unification ⋮ The undecidability of simultaneous rigid E-unification ⋮ Cyclic connections ⋮ Incremental theory reasoning methods for semantic tableaux ⋮ Proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-unification ⋮ <scp>OutsideIn(X)</scp>Modular type inference with local assumptions ⋮ A completion-based method for mixed universal and rigid E-unification ⋮ A practical integration of first-order reasoning and decision procedures ⋮ What you always wanted to know about rigid E-unification ⋮ Decidability and complexity of simultaneous rigid E-unification with one variable and related results

Uses Software

• ETPS

This page was built for publication: Theorem proving using equational matings and rigid E -unification