Theory exploration powered by deductive synthesis

DOI10.1007/978-3-030-81688-9_6zbMath1493.68388arXiv2009.04826OpenAlexW3185574054MaRDI QIDQ832255

Eytan Singher, Shachar Itzhaky

Publication date: 25 March 2022

Full work available at URL: https://arxiv.org/abs/2009.04826

zbMATH Keywords

synthesisautomatic theorem provingtheory exploration

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• Coq
• Dafny
• Theorema
• VAMPIRE
• z3
• SIMPLIFY
• HipSpec
• Leon
• CVC4
• Hipster
• TRANSIT
• FlashMeta
• egg
• IsaCoSy

Cites Work

• Unnamed Item
• Unnamed Item
• Conjecture synthesis for inductive theories
• \textit{Theorema}: Towards computer-aided mathematical theory exploration
• Fast congruence closure and extensions
• Programming by demonstration using version space algebra
• Superposition with structural induction
• Automated theory exploration for interactive theorem proving: an introduction to the Hipster system
• Synthesis with abstract examples
• Program synthesis with equivalence reduction
• Maximal specification synthesis
• Dafny: An Automatic Program Verifier for Functional Correctness
• Congruence Closure with Free Variables
• TIP: Tons of Inductive Problems
• Simplify: a theorem prover for program checking
• Fast Decision Procedures Based on Congruence Closure
• Automating Inductive Proofs Using Theory Exploration
• Induction for SMT Solvers
• Equality saturation
• Synthesis of Circular Compositional Program Proofs via Abduction
• Quick specifications for the busy programmer
• Hipster: Integrating Theory Exploration in a Proof Assistant
• Case-Analysis for Rippling and Inductive Proof
• Into the Infinite - Theory Exploration for Coinduction

This page was built for publication: Theory exploration powered by deductive synthesis