Automating Inductive Proofs Using Theory Exploration
From MaRDI portal
Recommendations
- scientific article; zbMATH DE number 1389654
- scientific article; zbMATH DE number 3880144
- Automatic inductive theorem proving using Prolog
- Automated theorem proving by test set induction
- Automated Certification of Implicit Induction Proofs
- Automated constructivization of proofs
- Automatic proofs by induction in theories without constructors
- scientific article; zbMATH DE number 49488
- scientific article; zbMATH DE number 4043814
- Automating Induction with an SMT Solver
Cited in
(43)- Inductive theorem proving based on tree grammars
- Quick specifications for the busy programmer
- Equivalence checking of two functional programs using inductive theorem provers
- Into the Infinite - Theory Exploration for Coinduction
- Disproving inductive entailments in separation logic via base pair approximation
- Automatic inductive theorem proving using Prolog
- Automating Induction with an SMT Solver
- Focused Inductive Theorem Proving
- Lemmaless induction in trace logic
- TIP: tons of inductive problems
- Proving properties of functional programs by equality saturation
- Inductive prover based on equality saturation for a lazy functional language
- Refinements to depth-first iterative-deepening search in automatic theorem proving
- scientific article; zbMATH DE number 1341622 (Why is no real title available?)
- Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques
- Deep reinforcement learning for synthesizing functions in higher-order logic
- Rewriting and inductive reasoning
- A mathematical benchmark for inductive theorem provers
- Teaching Automated Theorem Proving by Example: PyRes 1.2
- Lemma discovery and strategies for automated induction
- Automated Certification of Implicit Induction Proofs
- Quantifier-free induction for lists
- Automata-driven automated induction
- Alien coding
- Automatic Learning of Proof Methods in Proof Planning
- Automated natural deduction prover and experiments
- An Investigation of Hilbert’s Implicit Reasoning through Proof Discovery in Idle-Time
- The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions
- Induction in saturation-based proof search
- Conjectures, tests and proofs: an overview of theory exploration
- Theory exploration powered by deductive synthesis
- Unprovability results for clause set cycles
- Machine Learning for Inductive Theorem Proving
- Integer induction in saturation
- Checking equivalence in a non-strict language
- Automated theory exploration for interactive theorem proving: an introduction to the Hipster system
- Clause set cycles and induction
- Getting saturated with induction
- Induction and Skolemization in saturation theorem proving
- Logic Based Program Synthesis and Transformation
- Hipster: integrating theory exploration in a proof assistant
- Removing algebraic data types from constrained Horn clauses using difference predicates
- Combining induction and saturation-based theorem proving
This page was built for publication: Automating Inductive Proofs Using Theory Exploration
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4928454)
