scientific article
From MaRDI portal
Publication:2751361
zbMath0992.68123MaRDI QIDQ2751361
Nachum Dershowitz, David Alan Plaisted
Publication date: 27 August 2002
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Grammars and rewriting systems (68Q42) Word problems, etc. in computability and recursion theory (03D40)
Related Items (33)
Interpolation systems for ground proofs in automated deduction: a survey ⋮ Modular Termination and Combinability for Superposition Modulo Counter Arithmetic ⋮ Things to know when implementing KBO ⋮ The disconnection tableau calculus ⋮ Dealing with explicit preferences and uncertainty in answer set programming ⋮ On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories ⋮ Tableaux and hypersequents for justification logics ⋮ Equational Theorem Proving for Clauses over Strings ⋮ Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ Rewriting-based repairing strategies for XML repositories ⋮ Efficient general AGH-unification ⋮ Deciding expressive description logics in the framework of resolution ⋮ Making theory reasoning simpler ⋮ Strict coherence of conditional rewriting modulo axioms ⋮ Automated verification of selected equivalences for security protocols ⋮ Canonical Ground Horn Theories ⋮ Narrowing Based Inductive Proof Search ⋮ Canonicity1 1This research was supported in part by the Israel Science Foundation (grant no. 254/01). ⋮ New Undecidability Results for Properties of Term Rewrite Systems ⋮ Proving weak properties of rewriting ⋮ SCL(EQ): SCL for first-order logic with equality ⋮ Abstract canonical presentations ⋮ Efficient General Unification for XOR with Homomorphism ⋮ Selecting the Selection ⋮ Equational theorem proving modulo ⋮ Deciding knowledge in security protocols under some e-voting theories ⋮ Timed Term Rewrite Systems ⋮ Theory decision by decomposition ⋮ Rewrite-Based Decision Procedures ⋮ Set of support, demodulation, paramodulation: a historical perspective ⋮ A posthumous contribution by Larry Wos: excerpts from an unpublished column ⋮ SCL(EQ): SCL for first-order logic with equality ⋮ On interpolation in automated theorem proving
This page was built for publication: