A completion-based method for mixed universal and rigid E-unification
From MaRDI portal
Publication:5210805
DOI10.1007/3-540-58156-1_49zbMath1433.68533OpenAlexW1606566547MaRDI QIDQ5210805
Publication date: 21 January 2020
Published in: Automated Deduction — CADE-12 (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/3-540-58156-1_49
Related Items
A framework for using knowledge in tableau proofs, The undecidability of simultaneous rigid E-unification, Incremental theory reasoning methods for semantic tableaux, The tableau-based theorem prover 3 T A P Version 4.0, What you always wanted to know about rigid E-unification
Uses Software
Cites Work