scientific article

zbMath0659.68114MaRDI QIDQ3809306

Nachum Dershowitz, Leo Bachmair

Publication date: 1987

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

reasoningcompletionequational inferencerewriting modulo a congruence

Mathematics Subject Classification ID

Equational logic, Mal'tsev conditions (08B05)

Related Items (16)

Completion procedures as semidecision procedures ⋮ Complete sets of reductions modulo associativity, commutativity and identity ⋮ Consider only general superpositions in completion procedures ⋮ Extension of the associative path ordering to a chain of associative commutative symbols ⋮ Critical pair criteria for completion ⋮ Linear and unit-resulting refutations for Horn theories ⋮ Unnamed Item ⋮ Equational completion in order-sorted algebras ⋮ Learning domain knowledge to improve theorem proving ⋮ Term rewriting induction ⋮ Unnamed Item ⋮ Theorem proving modulo associativity ⋮ Schematization of infinite sets of rewrite rules generated by divergent completion processes ⋮ Automating Theories in Intuitionistic Logic ⋮ The equational part of proofs by structural induction ⋮ Proving termination of (conditional) rewrite systems. A semantic approach

This page was built for publication: