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

Cited In (79)

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