Decidability and complexity analysis by basic paramodulation

DOI10.1006/inco.1998.2730zbMath0927.68042OpenAlexW1966042322MaRDI QIDQ1281494

Robert Nieuwenhuis

Publication date: 29 November 1999

Published in: Information and Computation (Search for Journal in Brave)

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

zbMATH Keywords

Horn clausesbasic paramodulation

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items

Permutative rewriting and unification ⋮ A polynomial algorithm for uniqueness of normal forms of linear shallow term rewrite systems ⋮ Unification and Matching in Hierarchical Combinations of Syntactic Theories ⋮ Superposition with completely built-in abelian groups

Cites Work

• Termination of rewriting
• Syntacticness, cycle-syntacticness and shallow theories
• Theorem proving with ordering and equality constrained clauses
• Basic paramodulation
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• On ground AC-completion
• Any ground associative-commutative theory has a finite canonical system
• On narrowing, refutation proofs and constraints
• Unnamed Item
• Unnamed Item
• Unnamed Item