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

DOI10.1145/321850.321859zbMath0296.68092OpenAlexW2048748607MaRDI QIDQ4050191

James R. Slagle

Publication date: 1974

Published in: Journal of the ACM (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/321850.321859

Mathematics Subject Classification ID

Related Items (78)

Relative termination via dependency pairs ⋮ From Logic to Functional Logic Programs ⋮ On solving the equality problem in theories defined by Horn clauses ⋮ Transforming Boolean equalities into constraints ⋮ A Finite Representation of the Narrowing Space ⋮ From Outermost Reduction Semantics to Abstract Machine ⋮ Towards Erlang Verification by Term Rewriting ⋮ 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 ⋮ Ensuring the quasi-termination of needed narrowing computations ⋮ 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 ⋮ Using resolution for deciding solvable classes and building finite models ⋮ 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 ⋮ Enumerating outer narrowing derivations for constructor-based term rewriting systems ⋮ An integrated framework for the diagnosis and correction of rule-based programs ⋮ A new generic scheme for functional logic programming with constraints ⋮ Optimization of rewrite theories by equational partial evaluation ⋮ Unnecessary inferences in associative-commutative completion procedures ⋮ 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) ⋮ Symbolic Specialization of Rewriting Logic Theories with Presto ⋮ Default rules for Curry ⋮ Unification in varieties of completely regular semigroups ⋮ Optimizing Maude programs via program specialization ⋮ On completeness of narrowing strategies ⋮ A rationale for conditional equational programming ⋮ Chain properties of rule closures ⋮ Conditional equational theories and complete sets of transformations ⋮ Towards Modelling Actor-Based Concurrency in Term Rewriting ⋮ Proving convergence of self-stabilizing systems using first-order rewriting and regular languages ⋮ Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems ⋮ Superposition with completely built-in abelian groups ⋮ Operational semantics for declarative multi-paradigm languages ⋮ Exploring conditional rewriting logic computations ⋮ Lazy narrowing: strong completeness and eager variable elimination ⋮ Functional Logic Programming in Maude ⋮ Unification theory ⋮ Complexity of unification problems with associative-commutative operators ⋮ Functional Logic Programming: From Theory to Curry ⋮ Termination of narrowing via termination of rewriting ⋮ From Boolean Equalities to Constraints ⋮ Unification in commutative theories ⋮ Non-resolution theorem proving ⋮ Variant-Based Satisfiability in Initial Algebras ⋮ The narrowing-driven approach to functional logic program specialization ⋮ A pragmatic approach to resolution-based theorem proving ⋮ A Transformational Approach to Polyvariant BTA of Higher-Order Functional Programs ⋮ Termination of Narrowing in Left-Linear Constructor Systems ⋮ A partial evaluation framework for order-sorted equational programs modulo axioms ⋮ Associative-commutative deduction with constraints ⋮ On pot, pans and pudding or how to discover generalised critical Pairs ⋮ Applications and extensions of context-sensitive rewriting ⋮ Completion for rewriting modulo a congruence ⋮ Complete sets of transformations for general E-unification ⋮ Complete sets of unifiers and matchers in equational theories ⋮ A strong restriction of the inductive completion procedure ⋮ Basic narrowing revisited ⋮ Characterizing Compatible View Updates in Syntactic Bidirectionalization ⋮ Context-sensitive rewriting strategies ⋮ A superposition oriented theorem prover ⋮ Refutational theorem proving using term-rewriting systems ⋮ Modeling Pointer Redirection as Cyclic Term-graph Rewriting ⋮ Equational methods in first order predicate calculus ⋮ Cancellative Abelian monoids and related structures in refutational theorem proving. I ⋮ Static Slicing of Rewrite Systems ⋮ Higher-order narrowing with definitional trees ⋮ Symbolic computation in Maude: some tapas

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