Computing with rewrite systems
From MaRDI portal
Publication:3707361
DOI10.1016/S0019-9958(85)80003-6zbMath0584.68020MaRDI QIDQ3707361
Publication date: 1985
Published in: Information and Control (Search for Journal in Brave)
predicate calculusprogram specificationHorn clausesnegationlogic programmingterm rewriting systemsprogram synthesisKnuth-Bendix completion procedureequivalence-preserving rulesnarrowing procedure
Specification and verification (program logics, model checking, etc.) (68Q60) General topics in the theory of software (68N01) Varieties (08B99)
Related Items (26)
On sufficient-completeness and related properties of term rewriting systems ⋮ A proof system for conditional algebraic specifications ⋮ A survey of ordinal interpretations of type ɛ0 for termination of rewriting systems ⋮ Completion procedures as semidecision procedures ⋮ Rewriting, and equational unification: the higher-order cases ⋮ Proofs in parameterized specifications ⋮ Program transformation and rewriting ⋮ Encompassment properties and automata with constraints ⋮ Unification modulo an equality theory for equational logic programming ⋮ Sufficient-completeness, ground-reducibility and their complexity ⋮ Category-based modularisation for equational logic programming ⋮ Critical pair criteria for completion ⋮ Fast Knuth-Bendix completion with a term rewriting system compiler ⋮ Enumerating outer narrowing derivations for constructor-based term rewriting systems ⋮ Linear and unit-resulting refutations for Horn theories ⋮ Set-theoretic graph rewriting ⋮ An introduction to category-based equational logic ⋮ A rationale for conditional equational programming ⋮ Canonical Inference for Implicational Systems ⋮ When is an extension of a specification consistent? Decidable and undecidable cases ⋮ Towards a foundation of completion procedures as semidecision procedures ⋮ Canonical Ground Horn Theories ⋮ Unnamed Item ⋮ Synthetic programming ⋮ Termination orderings for associative-commutative rewriting systems ⋮ Deductive and inductive synthesis of equational programs
This page was built for publication: Computing with rewrite systems
