Paramodulation with built-in AC-theories and symbolic constraints

DOI10.1006/jsco.1996.0074zbMath0878.68074OpenAlexW2038734800MaRDI QIDQ1355755

Albert Rubio, Robert Nieuwenhuis

Publication date: 28 May 1997

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/b632bcad8bfc28618708459a111199ef51a925a3

zbMATH Keywords

clauses with symbolic constraintsparamodulation strategies

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items (3)

Superposition-based equality handling for analytic tableaux ⋮ Superposition with completely built-in abelian groups ⋮ Equational theorem proving modulo

This page was built for publication: Paramodulation with built-in AC-theories and symbolic constraints