A Deductive Approach to Program Synthesis
From MaRDI portal
Publication:3922132
DOI10.1145/357084.357090zbMath0468.68009OpenAlexW2012436850WikidataQ29026674 ScholiaQ29026674MaRDI QIDQ3922132
Zohar Manna, Richard Waldinger
Publication date: 1980
Published in: ACM Transactions on Programming Languages and Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/357084.357090
Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)
Related Items
\textit{AlCons}: deductive synthesis of sorting algorithms in \textit{Theorema} ⋮ Analyzing generalized planning under nondeterminism ⋮ Concise Read-Only Specifications for Better Synthesis of Programs with Pointers ⋮ Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper) ⋮ Church's Problem Revisited ⋮ Toward formal development of programs from algebraic specifications: Implementations revisited ⋮ Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs ⋮ Mechanical translation of set theoretic problem specifications into efficient RAM code - a case study ⋮ The McCarthy's recursion induction principle: oldy but goody ⋮ A theory of formal synthesis via inductive learning ⋮ Direct deductive computation on discourse representation structures ⋮ Machine learning and logic: a new frontier in artificial intelligence ⋮ The pragmatic proof: Hypermedia API composition and execution ⋮ Model checking and synthesis for branching multi-weighted logics ⋮ Flexible Correct-by-Construction Programming ⋮ Iterative genetic improvement: scaling stochastic program synthesis ⋮ Learning higher-order logic programs ⋮ Complexity of synthesis of composite service with correctness guarantee ⋮ Completely non-clausal theorem proving ⋮ Synthesis from scenario-based specifications ⋮ Proofs and programs: A naïve approach to program extraction ⋮ Automatic theorem proving. II ⋮ Unnamed Item ⋮ An approach to automatic deductive synthesis of functional programs ⋮ Synthesis of list algorithms by mechanical proving ⋮ Algebra-based synthesis of loops and their invariants (invited paper) ⋮ Metaheuristics ``In the large ⋮ SYNTHESIZING STATE-BASED OBJECT SYSTEMS FROM LSC SPECIFICATIONS ⋮ Synthesis of sorting algorithms using multisets in \textit{Theorema} ⋮ Superposition with equivalence reasoning and delayed clause normal form transformation ⋮ Linearity and regularity with negation normal form ⋮ A higher-order interpretation of deductive tableau ⋮ Building Theorem Provers ⋮ Refutation-based synthesis in SMT ⋮ Synthesis of induction orderings for existence proofs ⋮ Tactic theorem proving with refinement-tree proofs and metavariables ⋮ A correctness result for synthesizing plans with loops in stochastic domains ⋮ Submodule construction as equation solving in CCS ⋮ COCHIS: Stable and coherent implicits ⋮ Superposition with first-class booleans and inprocessing clausification ⋮ Synthetic programming ⋮ Deductive synthesis of sorting programs ⋮ Automatic Synthesis of Merging and Inserting Algorithms on Binary Trees Using Multisets in Theorema ⋮ Automatic programming: A tutorial on formal methodologies ⋮ Top-down synthesis of divide-and-conquer algorithms ⋮ Deductive and inductive synthesis of equational programs ⋮ Logical debugging ⋮ Resourceful program synthesis from graded linear types
