Theorem proving using equational matings and rigid E -unification
From MaRDI portal
Publication:4302815
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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
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
This page was built for publication: Theorem proving using equational matings and rigid E -unification
