A rationale for conditional equational programming

DOI10.1016/0304-3975(90)90064-OzbMath0702.68034MaRDI QIDQ915429

Nachum Dershowitz, Mitsuhiro Okada

Publication date: 1990

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

rewritinglogic programmingfunctional programmingnarrowingconditional equational programmingground confluence

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Logic programming (68N17) General topics in the theory of software (68N01)

Related Items

Sufficient conditions for modular termination of conditional term rewriting systems ⋮ Termination of combined (rewrite and λ-calculus) systems ⋮ Semantics for positive/negative conditional rewrite systems ⋮ A maximal-literal unit strategy for horn clauses ⋮ Extended term rewriting systems ⋮ Conditional rewriting logic: Deduction, models and concurrency ⋮ Completeness results for basic narrowing ⋮ Unnamed Item ⋮ The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors ⋮ Termination proofs and the length of derivations ⋮ Open problems in rewriting ⋮ More problems in rewriting ⋮ Level-confluence of conditional rewrite systems with extra variables in right-hand sides ⋮ Problems in rewriting III ⋮ Structures for abstract rewriting ⋮ Dependency pairs for proving termination properties of conditional term rewriting systems ⋮ Incremental constraint satisfaction for equational logic programming ⋮ A new generic scheme for functional logic programming with constraints ⋮ Rewriting systems over similarity and generalized pseudometric spaces and their properties ⋮ Higher order conditional rewriting and narrowing ⋮ Abstract data type systems ⋮ Local confluence of conditional and generalized term rewriting systems ⋮ Term rewriting systems with sort priorities ⋮ Elimination of conditions ⋮ Specification and proof in membership equational logic ⋮ Logicality of conditional rewrite systems ⋮ R n - and G n -logics ⋮ On the confluence of lambda-calculus with conditional rewriting ⋮ Conditional narrowing modulo a set of equations ⋮ Operational termination of conditional term rewriting systems ⋮ Automata-driven automated induction

Cites Work

• Simplifying conditional term rewriting systems: Unification, termination and confluence
• Note on a proof of the extended Kirby-Paris theorem on labelled finite trees
• Conditional rewrite rules: Confluence and termination
• Computing in systems described by equations
• Proof by semantic attributes of a LISP compiler
• Computing with rewrite systems
• Semantic confluence tests and completion methods
• The relation between logic and functional languages: a survey
• An implementation of narrowing
• Proving termination with multiset orderings
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
• Completion-time optimization of rewrite-time goal solving
• Intensional interpretations of functionals of finite type I
• Equality, types, modules, and (why not?) generics for logic programming
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item