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
Eta-conversion for the languages of explicit substitutions, Extending Bachmair's method for proof by consistency to the final algebra, Some results on the confluence property of combined term rewriting systems, Automated deduction with associative-commutative operators, A complete equational axiomatization for prefix iteration, The shortest single axioms for groups of exponent 4, Single identities for ternary Boolean algebras, Weights for total division orderings on strings, Buchberger's algorithm: The term rewriter's point of view, Describing symmetrical structures in logic., The application of automated reasoning to questions in mathematics and logic, Mechanical translation of set theoretic problem specifications into efficient RAM code - a case study, The Church-Rosser property for ground term-rewriting systems is decidable, Simplifying conditional term rewriting systems: Unification, termination and confluence, Embedding Boolean expressions into logic programming, A class of confluent term rewriting systems and unification, On deciding the confluence of a finite string-rewriting system on a given congruence class, History and basic features of the critical-pair/completion procedure, Automatic inductive theorem proving using Prolog, Only prime superpositions need be considered in the Knuth-Bendix completion procedure, Critical pair criteria for completion, Parallel dynamic semantics of sequential programs with speculative and incremental computation, Computing a Gröbner basis of a polynomial ideal over a Euclidean domain, Implementing first-order rewriting with constructor systems, Pseudo-natural algorithms for finitely generated presentations of monoids and groups, A multi-level geometric reasoning system for vision, Finite generation of ambiguity in context-free languages, A geometrical approach to multiset orderings, Lifting canonical algorithms from a ring R to the ring R[x], Fast Knuth-Bendix completion with a term rewriting system compiler, Higher-order rewrite systems and their confluence, Parikh-reducing Church-Rosser representations for some classes of regular languages, A notation for lambda terms. A generalization of environments, Knuth's coherent presentations of plactic monoids of type A, Simple termination of rewrite systems, A note on simplification orderings, Undecidable properties of monoids with word problem solvable in linear time. II: Cross sections and homological and homotopical finiteness conditions., Undecidable properties of monoids with word problem solvable in linear time., A rewriting approach to satisfiability procedures., Orienting rewrite rules with the Knuth-Bendix order., An upper bound on the derivational complexity of Knuth-Bendix orderings., New decision algorithms for finitely presented commutative semigroups, On using ground joinable equations in equational theorem proving, Complete positive group presentations., A complete proof of correctness of the Knuth-Bendix completion algorithm, From hidden to visible: a unified framework for transforming behavioral theories into rewrite theories, Semantically-guided goal-sensitive reasoning: inference system and completeness, Testing for the Church-Rosser property, A Noetherian and confluent rewrite system for idempotent semigroups, Composition-diamond lemma for associative conformal algebras., Theorem proving modulo, Rewrite, rewrite, rewrite, rewrite, rewrite, \dots, Conditional congruence closure over uninterpreted and interpreted symbols, Completion for unification, Fuzzy term-rewriting system, What's so special about Kruskal's theorem and the ordinal \(\Gamma{}_ 0\)? A survey of some results in proof theory, Algebraic structures of \(F\)-manifolds via pre-Lie algebras, A new approach to recursion removal, Semantics of order-sorted specifications, A criterion for proving noetherianity of a relation, Some experiments with a completion theorem prover, Checking overlaps of nominal rewriting rules, The Knuth-Bendix procedure for strings as a substitute for coset enumeration, Operational semantics of a kernel of the language ELECTRE, New methods for using Cayley graphs in interconnection networks, Termination and completion modulo associativity, commutativity and identity, Confluent linear numeration systems, How to decide the lark, The diamond lemma for ring theory, Non-resolution theorem proving, Complete demodulation for automatic theorem proving, Decidability of elementary theories of certain finitely defined algebras, Free distributive groupoids, Completion for rewriting modulo a congruence, Complete sets of transformations for general E-unification, Schematization of infinite sets of rewrite rules generated by divergent completion processes, Confluence of some presentations associated with graphs, On graph invariants given by linear recurrence relations, On the descriptive power of term rewriting systems, Relating rewriting techniques on monoids and rings: congruences on monoids and ideals in monoid rings, The first-order theory of linear one-step rewriting is undecidable, The finiteness of finitely presented monoids, Complete sets of unifiers and matchers in equational theories, The problem of guaranteeing the existence of a complete set of reductions, On Gröbner bases of noncommutative power series, A strong restriction of the inductive completion procedure, Automatic proofs by induction in theories without constructors, Unification problem in equational theories, Rational languages defined with a non-associative concatenation, Deciding embeddability of partial groupoids into semigroups, Invariants, patterns and weights for ordering terms, Partial completion of equational theories, Simplification orderings: Putting them to the test, Single axioms for groups and abelian groups with various operations, On the duality of abduction and model generation in a framework for model generation with equality, Generating polynomial orderings, Automated proofs of equality problems in Overbeek's competition, Rewriting systems of Coxeter groups, Deductive and inductive synthesis of equational programs, Proving termination of (conditional) rewrite systems. A semantic approach, On sufficient-completeness and related properties of term rewriting systems, Effective codescent morphisms in the varieties determined by convergent term rewriting systems., On merging software extensions, On recursive path ordering, Reductions in tree replacement systems, n-level rewriting systems, On solving the equality problem in theories defined by Horn clauses, Adding decision procedures to SMT solvers using axioms with triggers, The problems of cyclic equality and conjugacy for finite complete rewriting systems, A refinement of strong sequentiality for term rewriting with constructors, Proof by consistency, Knuth-Bendix completion of theories of commuting group endomorphisms, Rewriting with a nondeterministic choice operator, KBO orientability, A catalogue of complete group presentations, Termination of rewriting, Rewrite method for theorem proving in first order theory with equality, Complexity of matching problems, Thue systems as rewriting systems, Unification in combinations of collapse-free regular theories, Analysis of Dehn's algorithm by critical pairs, Proving termination of context-sensitive rewriting by transformation, Representing and building models for decidable subclasses of equational clausal logic, Things to know when implementing KBO, Multi-completion with termination tools, Decidable sentences of Church-Rosser congruences, Orderings for term-rewriting systems, Mechanizing and improving dependency pairs, Superposition-based equality handling for analytic tableaux, A formalization of the Knuth-Bendix(-Huet) critical pair theorem, Meta-interpretive learning of higher-order dyadic datalog: predicate invention revisited, Weakly-non-overlapping non-collapsing shallow term rewriting systems are confluent, Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility, Categorification, term rewriting and the Knuth-Bendix procedure, Attributed graph transformation with inheritance: efficient conflict detection and local confluence analysis using abstract critical pairs, On deciding satisfiability by theorem proving with speculative inferences, Conjecture synthesis for inductive theories, Decreasing diagrams and relative termination, About the descriptive power of certain classes of finite string-rewriting systems, Equational completion in order-sorted algebras, Automated proofs of the Moufang identities in alternative rings, Decision problems for finite special string-rewriting systems that are confluent on some congruence class, On ground-confluence of term rewriting systems, Finite derivation type for semilattices of semigroups., An algorithm for the construction of matrix representations for finitely presented non-commutative algebras, A rationale for conditional equational programming, Best unifiers in transitive modal logics, Confluence results for the pure strong categorical logic CCL. \(\lambda\)- calculi as subsystems of CCL, Efficiency issues in the KBMAG procedure, Rigid E-unification: NP-completeness and applications to equational matings, Confluence for graph transformations, Towards a foundation of completion procedures as semidecision procedures, Natural termination, Relational graph rewritings, On proving confluence modulo equivalence for Constraint Handling Rules, Rewrite rules for \(\mathrm{CTL}^\ast\), Testing for the ground (co-)reducibility property in term-rewriting systems, More efficient bottom-up multi-pattern matching in trees, Using geometric rewrite rules for solving geometric problems symbolically, Solving divergence in Knuth--Bendix completion by enriching signatures, On weakly confluent monadic string-rewriting systems, Rippling: A heuristic for guiding inductive proofs, Complexity of unification problems with associative-commutative operators, The problem of demodulator adjunction, Reachability analysis over term rewriting systems, A compact fixpoint semantics for term rewriting systems, Building exact computation sequences, Verifying nilpotence, Order-sorted unification, Unification in a combination of arbitrary disjoint equational theories, Gröbner-Shirshov basis for the braid group in the Birman-Ko-Lee generators., Automating the Knuth Bendix ordering, Using forcing to prove completeness of resolution and paramodulation, Theorem-proving with resolution and superposition, On word problems in Horn theories, Automating inductionless induction using test sets, On the relation between resolution based and completion based theorem proving, Finite complete rewriting systems for the Jantzen monoid and the Greendlinger group, Gröbner-Shirshov bases for associative algebras with multiple operators and free Rota-Baxter algebras., Termination of narrowing revisited, Inductive proof search modulo, Proofs by induction in equational theories with constructors, Finite complete rewriting systems and the complexity of word problem, Remarks on an example of Jantzen, Some fundamental algebraic tools for the semantics of computation. I. Comma categories, colimits, signatures and theories, A superposition oriented theorem prover, On graph rewritings, A systematic study of models of abstract data types, On the data type extension problem for algebraic specifications, Refutational theorem proving using term-rewriting systems, Axiomatisation des tests, Rewrite systems on a lattice of types, Equational methods in first order predicate calculus, Conditional rewrite rules, Modular tree transducers, Semi-unification, Automated inferencing, Termination orderings for associative-commutative rewriting systems, A finite Thue system with decidable word problem and without equivalent finite canonical system, Pseudo-natural algorithms for the word problem for finitely presented monoids and groups, 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, Normalising Lustre preserves security, Automated generation of exam sheets for automated deduction, Unnamed Item, Deciding confluence of certain term rewriting systems in polynomial time, Coherent confluence modulo relations and double groupoids, A path ordering for proving termination of AC rewrite systems, History and Prospects for First-Order Automated Deduction, Non-E-Overlapping, Weakly Shallow, and Non-Collapsing TRSs are Confluent, An algebraic characterization of inductive soundness in proof by consistency, Finite generation and presentation problems for lambda calculus and combinatory logic, Sufficient-completeness, ground-reducibility and their complexity, Structures for abstract rewriting, Reduction relations for monoid semirings, A formal algorithmic language FALGOL. Thirty years after, Multiagent temporal logics, unification problems, and admissibilities, Unnamed Item, Reduction operators and completion of rewriting systems, Induction using term orders, Comprehensive Gröbner basis theory for a parametric polynomial ideal and the associated completion algorithm, Integration of parametric and ``ad hoc second order polymorphism in a calculus with subtyping, Algorithmic operator algebras via normal forms in tensor rings, Linear and unit-resulting refutations for Horn theories, Reasoning with conditional axioms, An improved general path order, Unnecessary inferences in associative-commutative completion procedures, Unification and combination of a class of traversal strategies made with pattern matching and fixed-points, The Word Problem for Finitely Presented Quandles is Undecidable, An Extension of the Knuth-Bendix Ordering with LPO-Like Properties, Computing all subtree repeats in ordered trees, Resolution with order and selection for hybrid logics, A Completion Method to Decide Reachability in Rewrite Systems, Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities, Efficiently solving quantified bit-vector formulas, Properties of graphs preserved by relational graph rewritings, Hereditarily finitely generated commutative monoids, Confluence of Graph Rewriting with Interfaces, Multi-completion with Termination Tools (System Description), Canonicity!, From Analytical Mechanics Problems to Rewriting Theory Through M. Janet’s Work, Noncommutative Gröbner Bases: Applications and Generalizations, String rewriting for double coset systems., Canonized Rewriting and Ground AC Completion Modulo Shostak Theories, Making theory reasoning simpler, Termination of term rewriting using dependency pairs, Gröbner-Shirshov bases, conformal algebras, and pseudo-algebras., Complete involutive rewriting systems, On the essence and initiality of conflicts in \(\mathcal{M} \)-adhesive transformation systems, Algebraic properties of some quadratic dynamical systems, Calcul de longueurs de chaînes de réécriture dans le monoïde libre, Regaining cut admissibility in deduction modulo using abstract completion, Convergent presentations and polygraphic resolutions of associative algebras, Abstract canonical presentations, Semantic foundations for generalized rewrite theories, Compilation of static and evolving conditional knowledge bases for computing induced nonmonotonic inference relations, Order-Sorted Rewriting and Congruence Closure, Confluence up to garbage in graph transformation, Transformation rules with nested application conditions: critical pairs, initial conflicts \& minimality, An application of matrix theory to a problem in universal algebra, Selecting the Selection, Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving, Normal Forms for Operators via Gröbner Bases in Tensor Algebras, A unifying splitting framework, Superposition with first-class booleans and inprocessing clausification, Neural precedence recommender, Confluence by critical pair analysis revisited, Certified equational reasoning via ordered completion, Automatic Termination, Proving Confluence of Term Rewriting Systems Automatically, Dependent choice as a termination principle, Deciding knowledge in security protocols under some e-voting theories, A generalization of the matrix equation \(A^ 2=J\), Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems, Derivational complexity and context-sensitive Rewriting, On equational theories, unification, and (un)decidability, Unification in permutative equational theories is undecidable, Chinese syzygies by insertions, Conditions for confluence of innermost terminating term rewriting systems, Pattern Unification with Sequence Variables and Flexible Arity Symbols, About the rewriting systems produced by the Knuth-Bendix completion algorithm, Some remarks on the Akivis algebras and the Pre-Lie algebras, More efficient left-to-right matching for overlapping pattern, On finitely presented and free algebras of Cantor varieties, The size-change principle and dependency pairs for termination of term rewriting, Polygraphs of finite derivation type, Automatic acquisition of search control knowledge from multiple proof attempts., Higher-order substitutions, The undecidability of the first-order theories of one step rewriting in linear canonical systems, Larry Wos: visions of automated reasoning, Set of support, demodulation, paramodulation: a historical perspective, A posthumous contribution by Larry Wos: excerpts from an unpublished column, Disjunctive bases of applied algebras of sets and their use in problems of combinatorial geometry, Iterating transducers, Ground joinability and connectedness in the superposition calculus, Term orderings for non-reachability of (conditional) rewriting, Algebraic Databases, Modular termination proofs for rewriting using dependency pairs, Undecidable Properties on Length-Two String Rewriting Systems, A complete superposition calculus for primal grammars, Labelings for decreasing diagrams, Confluence and commutation for nominal rewriting systems with atom-variables, Conditional term rewriting and first-order theorem proving, Proving group isomorphism theorems, A categorical formulation for critical-pair/completion procedures, Implementing contextual rewriting, Confluence of terminating membership conditional TRS, Completeness and confluence of order-sorted term rewriting, Completion for constrained term rewriting systems, A proof system for conditional algebraic specifications, Meta-rule synthesis from crossed rewrite systems, Completion of first-order clauses with equality by strict superposition, Completion procedures as semidecision procedures, Linear completion, Clausal rewriting, Design strategies for rewrite rules, Dynamic temporal logical operations in multi-agent logics, Unifying splitting, The Maude strategy language, Complete equational unification based on an extension of the Knuth-Bendix completion procedure, Network rewriting utility description, Shuffle polygraphic resolutions for operads, Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties, Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover, An explicit algorithm for normal forms in small overlap monoids, Positive Plücker tree certificates for non-realizability, Unnamed Item, Unification theory, Automata-driven efficient subterm unification, On interreduction of semi-complete term rewriting systems, Decreasing Diagrams and Relative Termination, Termination Tools in Ordered Completion, A general framework to build contextual cover set induction provers, Derivation lengths and order types of Knuth--Bendix orders, Superposition with lambdas, Making higher-order superposition work, Making higher-order superposition work, The HOM Problem is EXPTIME-Complete, High-Level Theories, Unification and Inference Rules in the Multi-modal Logic of Knowledge and Linear Time LTK, Rewriting in Gray categories with applications to coherence, String diagram rewrite theory III: Confluence with and without Frobenius, Confluence of algebraic rewriting systems, Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs
