Theorem proving with ordering constrained clauses

DOI10.1007/3-540-55602-8_186MaRDI QIDQ4264721zbMATH OpenFDO

Authors Robert Nieuwenhuis, Albert Rubio

Publication date 10 October 1999

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-55602-8_186

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cited in

(23)

• Superposition theorem proving for abelian groups represented as integer modules
• The first-order theory of lexicographic path orderings is undecidable
• Practical algorithms for deciding path ordering constraint satisfaction.
• Linear and unit-resulting refutations for Horn theories
• Extensional higher-order paramodulation in Leo-III
• scientific article; zbMATH DE number 1231543 (Why is no real title available?)
• R n - and G n -logics
• Theorem proving in cancellative abelian monoids (extended abstract)
• Harald Ganzinger's legacy: contributions to logics and programming
• About the theory of tree embedding
• Redundancy criteria for constrained completion
• A precedence-based total AC-compatible ordering
• Polynomial time termination and constraint satisfaction tests
• On narrowing, refutation proofs and constraints
• Superposition theorem proving for abelian groups represented as integer modules
• Local simplification
• Solving simplification ordering constraints
• Associative-commutative deduction with constraints
• AC-superposition with constraints: no AC-unifiers needed
• Conditional term rewriting and first-order theorem proving
• Redundancy criteria for constrained completion
• A total AC-compatible ordering based on RPO
• Simple LPO constraint solving methods

This page was built for publication: Theorem proving with ordering constrained clauses

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4264721)