scientific article; zbMATH DE number 1348468

zbMath0925.03076MaRDI QIDQ4264721

Robert Nieuwenhuis, Albert Rubio

Publication date: 10 October 1999

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

Conditional term rewriting and first-order theorem proving, About the theory of tree embedding, A precedence-based total AC-compatible ordering, Polynomial time termination and constraint satisfaction tests, On narrowing, refutation proofs and constraints, Linear and unit-resulting refutations for Horn theories, Extensional higher-order paramodulation in Leo-III, Solving simplification ordering constraints, The first-order theory of lexicographic path orderings is undecidable, Practical algorithms for deciding path ordering constraint satisfaction., Unnamed Item, Redundancy criteria for constrained completion, A total AC-compatible ordering based on RPO, R n - and G n -logics, Theorem proving in cancellative abelian monoids (extended abstract), Simple LPO constraint solving methods, Harald Ganzinger’s Legacy: Contributions to Logics and Programming, Redundancy criteria for constrained completion, Superposition theorem proving for abelian groups represented as integer modules, Associative-commutative deduction with constraints, AC-superposition with constraints: No AC-unifiers needed, Superposition theorem proving for abelian groups represented as integer modules, Local simplification