Primal grammars and unification modulo a binary clause

DOI10.1007/3-540-58156-1_20MaRDI QIDQ5210779zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Unification of infinite sets of terms schematized by primal grammars
• A complete superposition calculus for primal grammars
• On the semantics of unification grammars
• Implementation and Application of Automata
• Prime normal form and equivalence of simple grammars
• Unification grammars and off-line parsability
• Unambiguous Boolean grammars
• Polynomially parsable unification grammars
• The first order theory of primal grammars is decidable
• Indexed grammars and unification grammars

Cites work

• scientific article; zbMATH DE number 6084400 (Why is no real title available?)
• scientific article; zbMATH DE number 176722 (Why is no real title available?)
• scientific article; zbMATH DE number 1256672 (Why is no real title available?)
• scientific article; zbMATH DE number 1300970 (Why is no real title available?)
• scientific article; zbMATH DE number 1324446 (Why is no real title available?)
• scientific article; zbMATH DE number 1348461 (Why is no real title available?)
• scientific article; zbMATH DE number 512814 (Why is no real title available?)
• scientific article; zbMATH DE number 1414280 (Why is no real title available?)
• Automated deduction by theory resolution
• Efficient loop detection in prolog using the tortoise-and-hare technique
• Implication of clauses is undecidable
• On finite representations of infinite sequences of terms
• On the existence of nonterminating queries for a restricted class of PROLOG-clauses
• On unification of terms with integer exponents
• Satisfiability of the smallest binary program
• Unification of infinite sets of terms schematized by primal grammars
• Weighted graphs: A tool for studying the halting problem and time complexity in term rewriting systems and logic programming

Cited in

(3)

• Schematic saturation for decision and unification problems.
• Unification of infinite sets of terms schematized by primal grammars
• Implementation and Application of Automata

This page was built for publication: Primal grammars and unification modulo a binary clause

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