Theorem proving with ordering and equality constrained clauses
From MaRDI portal
Recommendations
Cited in
(36)- Rewrite method for theorem proving in first order theory with equality
- Local simplification
- Decidability and complexity analysis by basic paramodulation
- Practical algorithms for deciding path ordering constraint satisfaction.
- On using ground joinable equations in equational theorem proving
- Superposition with completely built-in abelian groups
- Cyclic proofs with ordering constraints
- Induction = I-axiomatization + first-order consistency.
- Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes)
- Pay-as-you-go consequence-based reasoning for the description logic \(\mathcal{SROIQ} \)
- 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
- Mechanising first-order temporal resolution
- scientific article; zbMATH DE number 1688812 (Why is no real title available?)
- Efficient description logic reasoning in Prolog: The DLog system
- Paramodulation with non-monotonic orderings and simplification
- scientific article; zbMATH DE number 3917747 (Why is no real title available?)
- scientific article; zbMATH DE number 67451 (Why is no real title available?)
- Model evolution with equality -- revised and implemented
- A combined superposition and model evolution calculus
- scientific article; zbMATH DE number 1980932 (Why is no real title available?)
- scientific article; zbMATH DE number 1761416 (Why is no real title available?)
- Reasoning with uncertain and inconsistent OWL ontologies
- Harald Ganzinger's legacy: contributions to logics and programming
- Superposition and Model Evolution Combined
- What you always wanted to know about rigid \(E\)-unification
- A comprehensive framework for saturation theorem proving
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- A comprehensive framework for saturation theorem proving
- Theorem proving modulo associativity
- Partial redundancy in saturation
- On the (in-)completeness of destructive equality resolution in the superposition calculus
- Superposition-based equality handling for analytic tableaux
- Deciding expressive description logics in the framework of resolution
- A resolution-based decision procedure for \({\mathcal{SHOIQ}}\).
This page was built for publication: Theorem proving with ordering and equality constrained clauses
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1897557)
