Unification of infinite sets of terms schematized by primal grammars
From MaRDI portal
Publication:1392278
DOI10.1016/S0304-3975(96)00052-7zbMath0903.68117MaRDI QIDQ1392278
Publication date: 23 July 1998
Published in: Theoretical Computer Science (Search for Journal in Brave)
Related Items
The first order theory of primal grammars is decidable, Linear pattern matching of compressed terms and polynomial rewriting, Simplified handling of iterated term schemata, Deciding Innermost Loops, Tree automata for rewrite strategies, Perfect Discrimination Graphs: Indexing Terms with Integer Exponents, Primal grammars and unification modulo a binary clause, A complete superposition calculus for primal grammars
Cites Work
- A total AC-compatible ordering based on RPO
- Fundamental properties of infinite trees
- Termination of rewriting
- The realm of primitive recursion
- Equational problems and disunification
- Classical recursion theory. The theory of functions and sets of natural numbers.
- Infinitary logics and 0-1 laws
- A field guide to equational logic
- A unification algorithm for typed \(\overline\lambda\)-calculus
- Schematization of infinite sets of rewrite rules generated by divergent completion processes
- Solving \(*\)-problems modulo distributivity by a reduction to \(AC1\)- unification
- Equational formulae with membership constraints
- An efficient incremental algorithm for solving systems of linear diophantine equations
- Reasoning about infinite computations
- Recurrence domains: Their unification and application to logic programming
- Satisfiability of the smallest binary program
- On unification of terms with integer exponents
- Completion of rewrite systems with membership constraints
- Infinitary logic for computer science
- Primal grammars and unification modulo a binary clause
- SOLVING SYMBOLIC ORDERING CONSTRAINTS
- On interreduction of semi-complete term rewriting systems
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
