Deductive and inductive synthesis of equational programs
From MaRDI portal
Publication:1322836
DOI10.1016/S0747-7171(06)80002-7zbMath0791.68106MaRDI QIDQ1322836
Uday S. Reddy, Nachum Dershowitz
Publication date: 9 June 1994
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
program transformationlogic programsspecificationprogram synthesisequational programsfunctional programsinductive proofordered rewriting
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (5)
An integrated framework for the diagnosis and correction of rule-based programs ⋮ Mechanically certifying formula-based Noetherian induction reasoning ⋮ Canonical Ground Horn Theories ⋮ Mechanizable inductive proofs for a class of ∀ ∃ formulas ⋮ Improving rewriting induction approach for proving ground confluence
Uses Software
Cites Work
- 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
- Unnamed Item
- Unnamed Item
- Unnamed Item
- NQTHM
- A completion procedure for conditional equations
- Automating inductionless induction using test sets
- Proofs by induction in equational theories with constructors
- On ground-confluence of term rewriting systems
- Top-down synthesis of divide-and-conquer algorithms
- Proof by consistency
- Termination of rewriting
- Simplifying conditional term rewriting systems: Unification, termination and confluence
- Conditional rewrite rules: Confluence and termination
- A strong restriction of the inductive completion procedure
- Automatic proofs by induction in theories without constructors
- Some Techniques for Recursion Removal from Recursive Functions
- A Technique for Establishing Completeness Results in Theorem Proving with Equality
- Computing with rewrite systems
- Semantic confluence tests and completion methods
- A simplified proof of the characterization theorem for Gröbner-bases
- Derivation of Logic Programs
- A Deductive Approach to Program Synthesis
- A System for Assisting Program Transformation
- Proving Theorems with the Modification Method
- Data Types as Lattices
- A Transformation System for Developing Recursive Programs
- Equational inference, canonical proofs, and proof orderings
- Proving refutational completeness of theorem-proving strategies
- Computing ground reducibility and inductively complete positions
- Rewriting techniques for program synthesis
- Program transformation and rewriting
- Reduction techniques for first-order reasoning
- Conditional rewriting in focus
- Clausal rewriting
This page was built for publication: Deductive and inductive synthesis of equational programs
