Primal grammars and unification modulo a binary clause

DOI10.1007/3-540-58156-1_20zbMath1433.68565OpenAlexW1533234552MaRDI QIDQ5210779

Gernot Salzer

Publication date: 21 January 2020

Published in: Automated Deduction — CADE-12 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-58156-1_20

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

Unification of infinite sets of terms schematized by primal grammars

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On the existence of nonterminating queries for a restricted class of PROLOG-clauses
• Weighted graphs: A tool for studying the halting problem and time complexity in term rewriting systems and logic programming
• Implication of clauses is undecidable
• Unification of infinite sets of terms schematized by primal grammars
• Automated deduction by theory resolution
• Satisfiability of the smallest binary program
• Efficient loop detection in prolog using the tortoise-and-hare technique
• On unification of terms with integer exponents
• On finite representations of infinite sequences of terms