On word problems in Horn theories

DOI10.1016/S0747-7171(08)80134-4MaRDI QIDQ757095zbMATH OpenOpenAlexFDO

Authors 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

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

Recommendations

• scientific article; zbMATH DE number 4064978
• scientific article; zbMATH DE number 4089521
• On solving the equality problem in theories defined by Horn clauses
• scientific article; zbMATH DE number 3924139
• Conditional rewrite rules

Cites work

• scientific article; zbMATH DE number 4016226 (Why is no real title available?)
• scientific article; zbMATH DE number 3928346 (Why is no real title available?)
• scientific article; zbMATH DE number 3930339 (Why is no real title available?)
• scientific article; zbMATH DE number 3990847 (Why is no real title available?)
• scientific article; zbMATH DE number 4089521 (Why is no real title available?)
• scientific article; zbMATH DE number 4776 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• scientific article; zbMATH DE number 3349331 (Why is no real title available?)
• scientific article; zbMATH DE number 3413831 (Why is no real title available?)
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Equality, types, modules, and (why not?) generics for logic programming
• Simplifying conditional term rewriting systems: Unification, termination and confluence
• Theorem-proving with resolution and superposition

Cited in

(16)

• Set of support, demodulation, paramodulation: a historical perspective
• Canonical ground Horn theories
• On deciding satisfiability by theorem proving with speculative inferences
• Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover
• Towards a foundation of completion procedures as semidecision procedures
• Theorem-proving with resolution and superposition
• scientific article; zbMATH DE number 4064978 (Why is no real title available?)
• scientific article; zbMATH DE number 4089521 (Why is no real title available?)
• Implicit induction in conditional theories
• Structures for abstract rewriting
• A rewriting approach to satisfiability procedures.
• Normalization of linear Horn clauses
• Combinatorial Problems for Horn Clauses
• Problem corner: Non-Horn problems
• The problem of Horn and Tarski
• SGGS decision procedures

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

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