Deductive and inductive synthesis of equational programs
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 4016226 (Why is no real title available?)
- scientific article; zbMATH DE number 4191131 (Why is no real title available?)
- scientific article; zbMATH DE number 3870641 (Why is no real title available?)
- scientific article; zbMATH DE number 3829296 (Why is no real title available?)
- scientific article; zbMATH DE number 3907753 (Why is no real title available?)
- scientific article; zbMATH DE number 3943001 (Why is no real title available?)
- scientific article; zbMATH DE number 3963167 (Why is no real title available?)
- scientific article; zbMATH DE number 4053061 (Why is no real title available?)
- scientific article; zbMATH DE number 4074466 (Why is no real title available?)
- scientific article; zbMATH DE number 4089521 (Why is no real title available?)
- scientific article; zbMATH DE number 42475 (Why is no real title available?)
- scientific article; zbMATH DE number 44213 (Why is no real title available?)
- scientific article; zbMATH DE number 3550181 (Why is no real title available?)
- scientific article; zbMATH DE number 1142316 (Why is no real title available?)
- scientific article; zbMATH DE number 3299786 (Why is no real title available?)
- scientific article; zbMATH DE number 3349331 (Why is no real title available?)
- scientific article; zbMATH DE number 3351184 (Why is no real title available?)
- scientific article; zbMATH DE number 958048 (Why is no real title available?)
- A Deductive Approach to Program Synthesis
- A System for Assisting Program Transformation
- A Technique for Establishing Completeness Results in Theorem Proving with Equality
- A Transformation System for Developing Recursive Programs
- A completion procedure for conditional equations
- A simplified proof of the characterization theorem for Gröbner-bases
- A strong restriction of the inductive completion procedure
- Automatic proofs by induction in theories without constructors
- Automating inductionless induction using test sets
- Clausal rewriting
- Complete sets of reductions with constraints
- Computing ground reducibility and inductively complete positions
- Computing with rewrite systems
- Conditional rewrite rules: Confluence and termination
- Conditional rewriting in focus
- Data Types as Lattices
- Derivation of Logic Programs
- Equational inference, canonical proofs, and proof orderings
- NQTHM
- On ground-confluence of term rewriting systems
- Ordered rewriting and confluence
- Program transformation and rewriting
- Proof by consistency
- Proofs by induction in equational theories with constructors
- Proving Theorems with the Modification Method
- Proving refutational completeness of theorem-proving strategies
- Reduction techniques for first-order reasoning
- Resolution of equations in algebraic structures. Volume II: Rewriting techniques
- Rewriting techniques for program synthesis
- Semantic confluence tests and completion methods
- Simplifying conditional term rewriting systems: Unification, termination and confluence
- Some Techniques for Recursion Removal from Recursive Functions
- Term rewriting induction
- Termination of rewriting
- Top-down synthesis of divide-and-conquer algorithms
Cited in
(32)- Turning Inductive into Equational Specifications
- scientific article; zbMATH DE number 408777 (Why is no real title available?)
- An approach to automatic deductive synthesis of functional programs
- scientific article; zbMATH DE number 1973864 (Why is no real title available?)
- Synthesis of induction orderings for existence proofs
- scientific article; zbMATH DE number 139988 (Why is no real title available?)
- Canonical ground Horn theories
- scientific article; zbMATH DE number 5572668 (Why is no real title available?)
- Formal deduction with transfinite induction and its transformation for easier program synthesis
- Improving rewriting induction approach for proving ground confluence
- Automatic Deductive Synthesis of Lisp Programs in the System ALISA
- Inductive synthesis of functional programs: an explanation based generalization approach
- Well-definedness and observational equivalence for inductive–coinductive programs
- Deductive synthesis of sorting programs
- A theory for deductive synthesis of algorithms in the computing milieu
- An integrated framework for the diagnosis and correction of rule-based programs
- scientific article; zbMATH DE number 792049 (Why is no real title available?)
- Rewriting techniques for program synthesis
- scientific article; zbMATH DE number 3907753 (Why is no real title available?)
- Synthesis of rewrite programs by higher-order and semantic unification
- Equational formulae with membership constraints
- scientific article; zbMATH DE number 2090035 (Why is no real title available?)
- A unified view of induction reasoning for first-order logic
- scientific article; zbMATH DE number 3845028 (Why is no real title available?)
- A rationale for conditional equational programming
- Programming by predicates: a formal model for interactive synthesis
- Mechanically certifying formula-based Noetherian induction reasoning
- Inductive synthesis of recursive processes from logical properties
- scientific article; zbMATH DE number 108494 (Why is no real title available?)
- scientific article; zbMATH DE number 4049000 (Why is no real title available?)
- Mechanizable inductive proofs for a class of \(\forall \exists\) formulas
- Programming in equational logic: Beyond strong sequentiality
This page was built for publication: Deductive and inductive synthesis of equational programs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1322836)
