Pages that link to "Item:Q1897557"
From MaRDI portal
The following pages link to Theorem proving with ordering and equality constrained clauses (Q1897557):
Displaying 14 items.
- Paramodulation with non-monotonic orderings and simplification (Q352977) (← links)
- Model evolution with equality -- revised and implemented (Q429586) (← links)
- A combined superposition and model evolution calculus (Q438531) (← links)
- Superposition-based equality handling for analytic tableaux (Q877891) (← links)
- Deciding expressive description logics in the framework of resolution (Q924723) (← links)
- A resolution-based decision procedure for \({\mathcal{SHOIQ}}\). (Q928657) (← links)
- Local simplification (Q1271570) (← links)
- Decidability and complexity analysis by basic paramodulation (Q1281494) (← links)
- Practical algorithms for deciding path ordering constraint satisfaction. (Q1400710) (← links)
- On using ground joinable equations in equational theorem proving (Q1404987) (← links)
- Induction = I-axiomatization + first-order consistency. (Q1854350) (← links)
- A comprehensive framework for saturation theorem proving (Q5918558) (← links)
- Formalizing Bachmair and Ganzinger's ordered resolution prover (Q5919011) (← links)
- A comprehensive framework for saturation theorem proving (Q5970776) (← links)
