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 (only showing first 100 items - show all)
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
This page was built for publication: Complete Sets of Reductions for Some Equational Theories
