Theorem proving with ordering and equality constrained clauses
From MaRDI portal
Publication:1897557
DOI10.1006/jsco.1995.1020zbMath0844.68107OpenAlexW2082976889MaRDI QIDQ1897557
Robert Nieuwenhuis, Albert Rubio
Publication date: 4 September 1995
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Full work available at URL: https://semanticscholar.org/paper/06e483d04ec418ded7719bd9af4e42e07c325b53
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (26)
Paramodulation with non-monotonic orderings and simplification ⋮ Superposition-based equality handling for analytic tableaux ⋮ Practical algorithms for deciding path ordering constraint satisfaction. ⋮ On using ground joinable equations in equational theorem proving ⋮ Model evolution with equality -- revised and implemented ⋮ A combined superposition and model evolution calculus ⋮ Deciding expressive description logics in the framework of resolution ⋮ A resolution-based decision procedure for \({\mathcal{SHOIQ}}\). ⋮ Superposition with completely built-in abelian groups ⋮ Reasoning in description logics by a reduction to disjunctive datalog ⋮ Pay-as-you-go consequence-based reasoning for the description logic \(\mathcal{SROIQ} \) ⋮ Reasoning with Uncertain and Inconsistent OWL Ontologies ⋮ Harald Ganzinger’s Legacy: Contributions to Logics and Programming ⋮ Superposition with equivalence reasoning and delayed clause normal form transformation ⋮ Mechanising first-order temporal resolution ⋮ Superposition and Model Evolution Combined ⋮ Formalizing Bachmair and Ganzinger's ordered resolution prover ⋮ A comprehensive framework for saturation theorem proving ⋮ Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes) ⋮ Model completeness, covers and superposition ⋮ Local simplification ⋮ Efficient description logic reasoning in Prolog: The DLog system ⋮ Decidability and complexity analysis by basic paramodulation ⋮ What you always wanted to know about rigid E-unification ⋮ Induction = I-axiomatization + first-order consistency. ⋮ A comprehensive framework for saturation theorem proving
This page was built for publication: Theorem proving with ordering and equality constrained clauses
