Completion of a Set of Rules Modulo a Set of Equations
From MaRDI portal
Recommendations
Cited in
(only showing first 100 items - show all)- Inductive proof search modulo
- On solving the equality problem in theories defined by Horn clauses
- Termination of rewriting
- Only prime superpositions need be considered in the Knuth-Bendix completion procedure
- Critical pair criteria for completion
- Preperfectness is undecidable for Thue systems containing only length- reducing rules and a single commutation rule
- Semantics of order-sorted specifications
- A criterion for proving noetherianity of a relation
- Combining matching algorithms: The regular case
- Conditional rewriting logic as a unified model of concurrency
- Termination and completion modulo associativity, commutativity and identity
- Conditional narrowing modulo a set of equations
- Completion for rewriting modulo a congruence
- Schematization of infinite sets of rewrite rules generated by divergent completion processes
- On deciding confluence of finite string-rewriting systems modulo partial commutativity
- Superposition theorem proving for abelian groups represented as integer modules
- Automated deduction with associative-commutative operators
- Buchberger's algorithm: The term rewriter's point of view
- Abstract data type systems
- Deciding the word problem in the union of equational theories.
- A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.
- Theorem proving modulo
- Swinging types=functions+relations+transition systems
- Partial completion of equational theories
- ELAN from a rewriting logic point of view
- Maude: specification and programming in rewriting logic
- Equational rules for rewriting logic
- Conditional congruence closure over uninterpreted and interpreted symbols
- Automatic proofs by induction in theories without constructors
- Unification in permutative equational theories is undecidable
- Unions of non-disjoint theories and combinations of satisfiability procedures
- Combination problems for commutative/monoidal theories or how algebra can help in equational unification
- From diagrammatic confluence to modularity
- Twenty years of rewriting logic
- On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
- Specification and proof in membership equational logic
- Process algebra with strategic interleaving
- Set of support, demodulation, paramodulation: a historical perspective
- Symbolic computation in Maude: some tapas
- Pattern eliminating transformations
- Terminating non-disjoint combined unification
- Generalized rewrite theories, coherence completion, and symbolic methods
- Reduction operators and completion of rewriting systems
- Metalevel algorithms for variant satisfiability
- Drags: a compositional algebraic framework for graph rewriting
- A semantic framework for open processes
- Abstract canonical presentations
- Structures for abstract rewriting
- Modular and incremental proofs of AC-termination
- Unification of drags and confluence of drag rewriting
- Metalevel algorithms for variant satisfiability
- Towards a sharing strategy for the graph rewriting calculus
- On First-Order Model-Based Reasoning
- Normal higher-order termination
- A Completion Method to Decide Reachability in Rewrite Systems
- scientific article; zbMATH DE number 6712184 (Why is no real title available?)
- Canonized Rewriting and Ground AC Completion Modulo Shostak Theories
- scientific article; zbMATH DE number 3870640 (Why is no real title available?)
- Linear-algebraic λ-calculus: higher-order, encodings, and confluence.
- Termination Modulo Combinations of Equational Theories
- scientific article; zbMATH DE number 3896290 (Why is no real title available?)
- scientific article; zbMATH DE number 3934390 (Why is no real title available?)
- Existence, Uniqueness, and Construction of Rewrite Systems
- scientific article; zbMATH DE number 4078851 (Why is no real title available?)
- On the unification problem for Cartesian closed categories
- scientific article; zbMATH DE number 2079033 (Why is no real title available?)
- Variant-Based Satisfiability in Initial Algebras
- On confluence versus strong confluence for one-rule trace-rewriting systems
- scientific article; zbMATH DE number 7453112 (Why is no real title available?)
- scientific article; zbMATH DE number 7455704 (Why is no real title available?)
- Complete sets of reductions modulo associativity, commutativity and identity
- Abstract rewriting with concrete operators
- On how to move mountains ‘associatively and commutatively’
- Combining matching algorithms: The regular case
- Undecidable properties of syntactic theories
- 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
- Any ground associative-commutative theory has a finite canonical system
- Open problems in rewriting
- 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
- Superposition theorem proving for abelian groups represented as integer modules
- Extending Maximal Completion (Invited Talk)
- Optimization of rewriting and complexity of rewriting
- AC-termination of rewrite systems: a modified Knuth-Bendix ordering
- Unification properties of commutative theories: a categorical treatment
- Buchberger's algorithm: a constraint-based completion procedure
- Higher-order narrowing with convergent systems
- One-rule trace-rewriting systems and confluence
- Computing knowledge in equational extensions of subterm convergent theories
- AC-superposition with constraints: no AC-unifiers needed
- On pot, pans and pudding or how to discover generalised critical pairs
- The vectorial \(\lambda\)-calculus
- Functional logic programming in Maude
- Unification in commutative theories
- Unification in a combination of arbitrary disjoint equational theories
This page was built for publication: Completion of a Set of Rules Modulo a Set of Equations
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3816048)
