Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity

Cited in

(79)

Associative-commutative deduction with constraints
Termination of Narrowing in Left-Linear Constructor Systems
A Transformational Approach to Polyvariant BTA of Higher-Order Functional Programs
Term rewriting induction
Rewrite method for theorem proving in first order theory with equality
Towards Erlang verification by term rewriting
A superposition oriented theorem prover
Symbolic computation in Maude: some tapas
Cancellative Abelian monoids and related structures in refutational theorem proving. I
Enumerating outer narrowing derivations for constructor-based term rewriting systems
The narrowing-driven approach to functional logic program specialization
Chain properties of rule closures
Completion for rewriting modulo a congruence
Complete sets of transformations for general E-unification
Negation with logical variables in conditional rewriting
A partial evaluation framework for order-sorted equational programs modulo axioms
Characterizing Compatible View Updates in Syntactic Bidirectionalization
From outermost reduction semantics to abstract machine
Unification theory
An introduction to category-based equational logic
Ensuring the quasi-termination of needed narrowing computations
Towards Modelling Actor-Based Concurrency in Term Rewriting
Complexity of matching problems
Orderings for term-rewriting systems
Termination of narrowing via termination of rewriting
Operational semantics for declarative multi-paradigm languages
Refutational theorem proving using term-rewriting systems
On pot, pans and pudding or how to discover generalised critical pairs
Lazy narrowing: strong completeness and eager variable elimination (extended abstract)
Transforming Boolean equalities into constraints
Unification in commutative theories
Relative termination via dependency pairs
Superposition with completely built-in abelian groups
A pragmatic approach to resolution-based theorem proving
Complexity of unification problems with associative-commutative operators
Applications and extensions of context-sensitive rewriting
Proving convergence of self-stabilizing systems using first-order rewriting and regular languages
A new generic scheme for functional logic programming with constraints
Proof normalization for resolution and paramodulation
Optimizing Maude programs via program specialization
An integrated framework for the diagnosis and correction of rule-based programs
From Logic to Functional Logic Programs
Termination of rewriting
Non-resolution theorem proving
Symbolic Specialization of Rewriting Logic Theories with Presto
Narrowing trees for syntactically deterministic conditional term rewriting systems
Complete sets of unifiers and matchers in equational theories
Basic narrowing revisited
Unnecessary inferences in associative-commutative completion procedures
Combination problems for commutative/monoidal theories or how algebra can help in equational unification
Optimization of rewrite theories by equational partial evaluation
Efficient solution of linear diophantine equations
Functional logic programming in Maude
Using resolution for deciding solvable classes and building finite models
Higher-order narrowing with definitional trees
Exploring conditional rewriting logic computations
On completeness of narrowing strategies
Unification properties of commutative theories: a categorical treatment
A Finite Representation of the Narrowing Space
Static slicing of rewrite systems
History and basic features of the critical-pair/completion procedure
Conditional equational theories and complete sets of transformations
Axiomatization of a functional logic language
A rationale for conditional equational programming
Equational methods in first order predicate calculus
Variant-Based Satisfiability in Initial Algebras
Critical pair criteria for completion
Only prime superpositions need be considered in the Knuth-Bendix completion procedure
Consider only general superpositions in completion procedures
Decidability of confluence and termination of monadic term rewriting systems
Context-sensitive rewriting strategies
Functional Logic Programming: From Theory to Curry
Modeling pointer redirection as cyclic term-graph rewriting
A strong restriction of the inductive completion procedure
Unification in varieties of completely regular semigroups
From Boolean equalities to constraints
On solving the equality problem in theories defined by Horn clauses
Lazy narrowing: strong completeness and eager variable elimination
Default rules for Curry

This page was built for publication: Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4050191)