Basic paramodulation
From MaRDI portal
Recommendations
Cited in
(30)- AC simplifications and closure redundancies in the superposition calculus
- Positive deduction modulo regular theories
- On restrictions of ordered paramodulation with simplification
- Deciding expressive description logics in the framework of resolution
- Goal directed strategies for paramodulation
- Equational theorem proving modulo
- Harald Ganzinger's legacy: contributions to logics and programming
- Superposition theorem proving for abelian groups represented as integer modules
- What you always wanted to know about rigid \(E\)-unification
- Superposition with completely built-in abelian groups
- Superposition-based equality handling for analytic tableaux
- Simultaneous paramodulation
- \( \alpha \)-paramodulation method for a lattice-valued logic \(L_nF(X)\) with equality
- Induction = I-axiomatization + first-order consistency.
- Encoding monomorphic and polymorphic types
- 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)
- Tree automata with equality constraints modulo equational theories
- Decidability and complexity analysis by basic paramodulation
- ELAN from a rewriting logic point of view
- A resolution-based decision procedure for \({\mathcal{SHOIQ}}\).
- Paramodulation with non-monotonic orderings and simplification
- Model completeness, covers and superposition
- Reasoning in description logics by a reduction to disjunctive datalog
- Superposition with equivalence reasoning and delayed clause normal form transformation
- Ground joinability and connectedness in the superposition calculus
- scientific article; zbMATH DE number 4049136 (Why is no real title available?)
- Connection tableaux with lazy paramodulation
- Theorem proving modulo
- Lazy narrowing: strong completeness and eager variable elimination
This page was built for publication: Basic paramodulation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1899908)
