On word problems in Horn theories

DOI10.1016/S0747-7171(08)80134-4zbMath0723.68100OpenAlexW2010001930MaRDI QIDQ757095

Emmanuel Kounalis, Michaël Rusinowitch

Publication date: 1991

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

Full work available at URL: https://doi.org/10.1016/s0747-7171(08)80134-4

zbMATH Keywords

Horn logicconditional rewrite rulesword roblem

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27) Grammars and rewriting systems (68Q42) Word problems, etc. in computability and recursion theory (03D40)

Related Items (10)

Implicit induction in conditional theories ⋮ Structures for abstract rewriting ⋮ A rewriting approach to satisfiability procedures. ⋮ Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ On deciding satisfiability by theorem proving with speculative inferences ⋮ Towards a foundation of completion procedures as semidecision procedures ⋮ Canonical Ground Horn Theories ⋮ Theorem-proving with resolution and superposition ⋮ SGGS decision procedures ⋮ Set of support, demodulation, paramodulation: a historical perspective

Cites Work

• Theorem-proving with resolution and superposition
• Simplifying conditional term rewriting systems: Unification, termination and confluence
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Equality, types, modules, and (why not?) generics for logic programming
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: On word problems in Horn theories