Complete Sets of Reductions for Some Equational Theories
From MaRDI portal
Publication:3938536
DOI10.1145/322248.322251zbMath0479.68092OpenAlexW2056016391MaRDI QIDQ3938536
Gerald E. Peterson, Mark E. Stickel
Publication date: 1981
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/322248.322251
Boolean algebradistributive latticesfinite termination propertywell-founded partial ordercommutative rings with unitcomplete unification algorithmsextension of the Knuth-Bendix algorithm for finding complete sets of reductionsfree commutative groupstheory of a finite number of associative and commutative functionsunique termination property
Related Items
Meta-rule synthesis from crossed rewrite systems, Completion procedures as semidecision procedures, Bi-rewriting, a term rewriting technique for monotonic order relations, A case study of completion modulo distributivity and Abelian groups, More problems in rewriting, AC-complete unification and its application to theorem proving, Typing Quantum Superpositions and Measurement, String Diagram Rewrite Theory I: Rewriting with Frobenius Structure, Buchberger's algorithm: The term rewriter's point of view, Unification properties of commutative theories: A categorical treatment, Set-theoretic graph rewriting, Buchberger's algorithm: A constraint-based completion procedure, Unification in varieties of completely regular semigroups, Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties, Towards automated deduction in cP systems, Unification theory, Operational Termination of Conditional Rewriting with Built-in Numbers and Semantic Data Structures, Variant Narrowing and Equational Unification, Combinable Extensions of Abelian Groups, Building Theorem Provers, AC Completion with Termination Tools, Associative-commutative deduction with constraints, AC-superposition with constraints: No AC-unifiers needed, On pot, pans and pudding or how to discover generalised critical Pairs, Extending Maximal Completion (Invited Talk), Confluence of algebraic rewriting systems, Reductions in tree replacement systems, On solving the equality problem in theories defined by Horn clauses, Unnamed Item, Semantically-guided goal-sensitive reasoning: model representation, Extending reduction orderings to ACU-compatible reduction orderings, Automated deduction with associative-commutative operators, Coherent confluence modulo relations and double groupoids, Unification in varieties of idempotent semigroups, A path ordering for proving termination of AC rewrite systems, Complete sets of reductions modulo associativity, commutativity and identity, An overview of LP, the Larch Prover, On how to move mountains ‘associatively and commutatively’, Linear Integer Arithmetic Revisited, Consider only general superpositions in completion procedures, Boolean algebra admits no convergent term rewriting system, Decidability of confluence and termination of monadic term rewriting systems, Proving equational and inductive theorems by completion and embedding techniques, Simulating Buchberger's algorithm by Knuth-Bendix completion, On ground AC-completion, Open problems in rewriting, Rewriting with a nondeterministic choice operator, Buchberger's algorithm: The term rewriter's point of view, Complexity of matching problems, Associative-commutative unification, Unification in combinations of collapse-free regular theories, A class of confluent term rewriting systems and unification, History and basic features of the critical-pair/completion procedure, Sufficient-completeness, ground-reducibility and their complexity, Structures for abstract rewriting, Modular and incremental proofs of AC-termination, Only prime superpositions need be considered in the Knuth-Bendix completion procedure, Critical pair criteria for completion, Computing a Gröbner basis of a polynomial ideal over a Euclidean domain, Orderings for term-rewriting systems, Efficient solution of linear diophantine equations, Combination problems for commutative/monoidal theories or how algebra can help in equational unification, Unnecessary inferences in associative-commutative completion procedures, On First-Order Model-Based Reasoning, Normal Higher-Order Termination, From diagrammatic confluence to modularity, Twenty years of rewriting logic, On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories, Strategy based semantics for mobility with time and access permissions, Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility, On using ground joinable equations in equational theorem proving, A complete proof of correctness of the Knuth-Bendix completion algorithm, Linear-algebraic λ-calculus: higher-order, encodings, and confluence., Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures, Equational completion in order-sorted algebras, Automated proofs of the Moufang identities in alternative rings, A rewriting strategy to verify observational congruence, Theorem proving modulo, Superposition with completely built-in abelian groups, On the unification problem for Cartesian closed categories, Conditional congruence closure over uninterpreted and interpreted symbols, Canonized Rewriting and Ground AC Completion Modulo Shostak Theories, A normal form for restricted exponential functions, Combining matching algorithms: The regular case, Confluence for graph transformations, Towards a foundation of completion procedures as semidecision procedures, Theorem proving in cancellative abelian monoids (extended abstract), Strict coherence of conditional rewriting modulo axioms, Termination and completion modulo associativity, commutativity and identity, Hilbert's tenth problem is of unification type zero, Complexity of unification problems with associative-commutative operators, Citius altius fortius, Unnamed Item, Regaining cut admissibility in deduction modulo using abstract completion, Using types as search keys in function libraries, Combining matching algorithms: The regular case, Abstract canonical presentations, Unification in commutative theories, Any ground associative-commutative theory has a finite canonical system, Generalized rewrite theories, coherence completion, and symbolic methods, Conditional narrowing modulo a set of equations, Completion for rewriting modulo a congruence, Invariants and closures in the theory of rewrite systems, On the descriptive power of term rewriting systems, Superposition theorem proving for abelian groups represented as integer modules, The algebraic lambda calculus, Complete sets of unifiers and matchers in equational theories, Tactics for Reasoning Modulo AC in Coq, Inductive proof search modulo, Termination Modulo Combinations of Equational Theories, Source-tracking unification, Confluence in probabilistic rewriting, A categorical critical-pair completion algorithm, Partial completion of equational theories, Set of support, demodulation, paramodulation: a historical perspective, Refutational theorem proving using term-rewriting systems, Axiomatisation des tests, Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description), Equational methods in first order predicate calculus, Cancellative Abelian monoids and related structures in refutational theorem proving. I, Towards a Sharing Strategy for the Graph Rewriting Calculus, Automated proofs of equality problems in Overbeek's competition, Termination orderings for associative-commutative rewriting systems, ELAN from a rewriting logic point of view, Equational rules for rewriting logic, Symbolic computation in Maude: some tapas
