On word problems in Horn theories

DOI10.1016/S0747-7171(08)80134-4zbMATH Open0723.68100OpenAlexW2010001930MaRDI QIDQ757095FDOQ757095

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

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

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)

Cites Work

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

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
• Title not available (Why is that?)
• Title not available (Why is that?)
• 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
• The problem of Horn and Tarski
• Problem corner: Non-Horn problems
• 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)