Basic paramodulation
From MaRDI portal
Publication:1899908
DOI10.1006/inco.1995.1131zbMath0833.68115OpenAlexW2914834504MaRDI QIDQ1899908
Publication date: 10 October 1995
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://semanticscholar.org/paper/5fb89d6ac8174c2b10292d280cb9f0ccf7b36439
Related Items
AC simplifications and closure redundancies in the superposition calculus, \( \alpha \)-paramodulation method for a lattice-valued logic \(L_nF(X)\) with equality, Paramodulation with non-monotonic orderings and simplification, Superposition-based equality handling for analytic tableaux, Tree automata with equality constraints modulo equational theories, Encoding Monomorphic and Polymorphic Types, Deciding expressive description logics in the framework of resolution, Connection tableaux with lazy paramodulation, A resolution-based decision procedure for \({\mathcal{SHOIQ}}\)., Theorem proving modulo, Superposition with completely built-in abelian groups, Reasoning in description logics by a reduction to disjunctive datalog, Lazy narrowing: strong completeness and eager variable elimination, Harald Ganzinger’s Legacy: Contributions to Logics and Programming, Superposition with equivalence reasoning and delayed clause normal form transformation, Translation of resolution proofs into short first-order proofs without choice axioms, Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes), Equational theorem proving modulo, Model completeness, covers and superposition, Superposition theorem proving for abelian groups represented as integer modules, Decidability and complexity analysis by basic paramodulation, What you always wanted to know about rigid E-unification, Induction = I-axiomatization + first-order consistency., Ground joinability and connectedness in the superposition calculus, ELAN from a rewriting logic point of view
