Deductive and inductive synthesis of equational programs
type: Item
instance of: scholarly article
title: Deductive and inductive synthesis of equational programs
zbMATH Open document ID: 0791.68106
DOI: 10.1016/S0747-7171(06)80002-7
author: Nachum Dershowitz
author: Uday S. Reddy
published in: Journal of Symbolic Computation
publication date: 1994-06-09T00:00:00Z
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 566063
zbMATH Keywords: equational programs
zbMATH Keywords: program transformation
zbMATH Keywords: functional programs
zbMATH Keywords: ordered rewriting
zbMATH Keywords: logic programs
zbMATH Keywords: specification
zbMATH Keywords: inductive proof
zbMATH Keywords: program synthesis
cites work: NQTHM
cites work: Some Techniques for Recursion Removal from Recursive Functions
cites work: A simplified proof of the characterization theorem for Gröbner-bases
cites work: Equational inference, canonical proofs, and proof orderings
cites work: Q3427354
cites work: Program transformation and rewriting
cites work: Conditional rewrite rules: Confluence and termination
cites work: Q3731007
cites work: Q3992424
cites work: Proving Theorems with the Modification Method
cites work: Conditional rewriting in focus
cites work: Reduction techniques for first-order reasoning
cites work: Computing ground reducibility and inductively complete positions
cites work: A Transformation System for Developing Recursive Programs
cites work: Computing with rewrite systems
cites work: Termination of rewriting
cites work: Q3993363
cites work: Q4385532
cites work: Q3210187
cites work: A System for Assisting Program Transformation
cites work: A strong restriction of the inductive completion procedure
cites work: A completion procedure for conditional equations
cites work: Q5626277
cites work: Derivation of Logic Programs
cites work: Q3674088
cites work: Q3028369
cites work: Proving refutational completeness of theorem-proving strategies
cites work: Proofs by induction in equational theories with constructors
cites work: Automatic proofs by induction in theories without constructors
cites work: Simplifying conditional term rewriting systems: Unification, termination and confluence
cites work: Proof by consistency
cites work: Q3685174
cites work: On ground-confluence of term rewriting systems
cites work: Automating inductionless induction using test sets
cites work: Q3805891
cites work: Q5581665
cites work: Q3818295
cites work: Q3713575
cites work: Q4124327
cites work: A Deductive Approach to Program Synthesis
cites work: Clausal rewriting
cites work: Q5687569
cites work: A Technique for Establishing Completeness Results in Theorem Proving with Equality
cites work: Semantic confluence tests and completion methods
cites work: Rewriting techniques for program synthesis
cites work: Q5624683
cites work: Data Types as Lattices
cites work: Top-down synthesis of divide-and-conquer algorithms
cites work: Q3336737
cites work: Q3789100
cites work: Ordered rewriting and confluence
cites work: Complete sets of reductions with constraints
cites work: Term rewriting induction
describes a project that uses: NQTHM
describes a project that uses: ML
MaRDI profile type: Publication
description: scientific article; zbMATH DE number 566063