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