scientific article; zbMATH DE number 3299786
From MaRDI portal
Publication:5581665
zbMath0188.04902MaRDI QIDQ5581665
Publication date: 1970
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items (only showing first 100 items - show all)
Proof normalization for resolution and paramodulation ⋮ Complete sets of reductions modulo associativity, commutativity and identity ⋮ Termination proofs and the length of derivations ⋮ On how to move mountains ‘associatively and commutatively’ ⋮ Generalized Gröbner bases: Theory and applications. A condensation ⋮ A local termination property for term rewriting systems ⋮ Optimization by non-deterministic, lazy rewriting ⋮ Restrictions of congruences generated by finite canonical string-rewriting systems ⋮ Conditional rewrite rule systems with built-in arithmetic and induction ⋮ Consider only general superpositions in completion procedures ⋮ Rewriting, and equational unification: the higher-order cases ⋮ Incremental termination proofs and the length of derivations ⋮ Program transformation and rewriting ⋮ An efficient representation of arithmetic for term rewriting ⋮ Boolean algebra admits no convergent term rewriting system ⋮ Decidability of confluence and termination of monadic term rewriting systems ⋮ Left-to-right tree pattern matching ⋮ Incremental techniques for efficient normalization of nonlinear rewrite systems ⋮ On fairness of completion-based theorem proving strategies ⋮ Proving equational and inductive theorems by completion and embedding techniques ⋮ Simulating Buchberger's algorithm by Knuth-Bendix completion ⋮ On proving properties of completion strategies ⋮ Bi-rewriting, a term rewriting technique for monotonic order relations ⋮ Distributing equational theorem proving ⋮ Topics in termination ⋮ Linear interpretations by counting patterns ⋮ Automatic termination proofs with transformation orderings ⋮ Substitution tree indexing ⋮ AC-complete unification and its application to theorem proving ⋮ Symideal Gröbner bases ⋮ Termination of constructor systems ⋮ The first-order theory of one-step rewriting is undecidable ⋮ FDT is undecidable for finitely presented monoids with solvable word problems ⋮ Unique normal forms for nonlinear term rewriting systems: Root overlaps ⋮ String Diagram Rewrite Theory I: Rewriting with Frobenius Structure ⋮ Polynomials over the reals in proofs of termination : from theory to practice ⋮ Algebraic data integration ⋮ On confluence versus strong confluence for one-rule trace-rewriting systems ⋮ Buchberger's algorithm: The term rewriter's point of view ⋮ It is undecidable whether the Knuth-Bendix completion procedure generates a crossed pair ⋮ Logic programs with equational type specifications ⋮ Applying term rewriting methods to finite groups ⋮ Optimization of rewriting and complexity of rewriting ⋮ AC-Termination of rewrite systems: A modified Knuth-Bendix ordering ⋮ An abstract formulation for rewrite systems ⋮ Set-theoretic graph rewriting ⋮ Non-size increasing graph rewriting for natural language processing ⋮ Unnamed Item ⋮ Critical pairs in term graph rewriting ⋮ Confluence up to Garbage ⋮ Initial Conflicts for Transformation Rules with Nested Application Conditions ⋮ Unnamed Item ⋮ AC-KBO revisited ⋮ Sémantique du parallélisme et du choix du langage Electre ⋮ How to prove decidability of equational theories with second-order computation analyser SOL ⋮ Symbolic manipulation for some non-algebraic objects and its application in computing the lce of van der pol equation* ⋮ Church-Rosser systems with respect to formal languages ⋮ Coherence of Gray Categories via Rewriting ⋮ Rewriting with generalized nominal unification ⋮ A partial solution for D-unification based on a reduction to AC 1-unification ⋮ Dynamically-typed computations for order-sorted equational presentations ⋮ Unnamed Item ⋮ Using the tree representation of terms to recognize matching with neural networks ⋮ Incremental theory reasoning methods for semantic tableaux ⋮ Learning domain knowledge to improve theorem proving ⋮ Theorem proving with group presentations: Examples and questions ⋮ Rewrite semantics for production rule systems: Theory and applications ⋮ Path indexing for AC-theories ⋮ Unnamed Item ⋮ Loops with Abelian Inner Mapping Groups: An Application of Automated Deduction ⋮ Harald Ganzinger’s Legacy: Contributions to Logics and Programming ⋮ Canonical Ground Horn Theories ⋮ From Search to Computation: Redundancy Criteria and Simplification at Work ⋮ Completion after Program Inversion of Injective Functions ⋮ Gröbner–Shirshov bases and their calculation ⋮ Essentials of Term Graph Rewriting ⋮ A list of applications of Stallings automata ⋮ Infinite trees in normal form and recursive equations having a unique solution ⋮ A PVS Theory for Term Rewriting Systems ⋮ Unnamed Item ⋮ Some relations on prefix reversal generators of the symmetric and hyperoctahedral group ⋮ Interpolation and Symbol Elimination ⋮ Any ground associative-commutative theory has a finite canonical system ⋮ CSI – A Confluence Tool ⋮ Unnamed Item ⋮ A pragmatic approach to resolution-based theorem proving ⋮ Completion for multiple reduction orderings ⋮ Solving the Conjugacy Decision Problem via Machine Learning ⋮ Induction using term orderings ⋮ On the connection between narrowing and proof by consistency ⋮ A completion-based method for mixed universal and rigid E-unification ⋮ On pot, pans and pudding or how to discover generalised critical Pairs ⋮ Unnamed Item ⋮ Extending Maximal Completion (Invited Talk) ⋮ On the Coalgebra of Partial Differential Equations ⋮ Transforming SAT into Termination of Rewriting ⋮ Unnamed Item ⋮ A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method ⋮ Automating Theories in Intuitionistic Logic ⋮ Comparing data type specifications via their normal forms
This page was built for publication:
