Automating inductive proofs using theory exploration. HipSpec is a system for automatically deriving and proving properties about functional programs. It uses a novel approach, combining theory exploration, counterexample testing and inductive theorem proving. HipSpec automatically generates a set of equational theorems about the available recursive functions of a program. These equational properties make up an algebraic specification for the program and can in addition be used as a background theory for proving additional user-stated properties. Experimental results are encouraging: HipSpec compares favourably to other inductive theorem provers and theory exploration systems.

References in zbMATH (referenced in 14 articles )

Showing results 1 to 14 of 14.
Sorted by year (citations)

  1. Echenim, M.; Peltier, N.: Combining induction and saturation-based theorem proving (2020)
  2. Hajdú, Márton; Hozzová, Petra; Kovács, Laura; Schoisswohl, Johannes; Voronkov, Andrei: Induction with generalization in superposition reasoning (2020)
  3. Hetzl, Stefan; Vierling, Jannik: Clause set cycles and induction (2020)
  4. Drămnesc, Isabela; Jebelean, Tudor; Stratulat, Sorin: Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques (2019)
  5. Demba, Moussa: Equivalence checking of two functional programs using inductive theorem provers (2018)
  6. Cruanes, Simon: Superposition with structural induction (2017)
  7. Smallbone, Nicholas; Johansson, Moa; Claessen, Koen; Algehed, Maximilian: Quick specifications for the busy programmer (2017)
  8. Brotherston, James; Gorogiannis, Nikos: Disproving inductive entailments in separation logic via base pair approximation (2015)
  9. Claessen, Koen; Johansson, Moa; Rosén, Dan; Smallbone, Nicholas: TIP: tons of inductive problems (2015)
  10. Eberhard, Sebastian; Hetzl, Stefan: Inductive theorem proving based on tree grammars (2015)
  11. Grechanik, S. A.: Proving properties of functional programs by equality saturation (2015)
  12. Rosén, Dan; Smallbone, Nicholas: TIP: tools for inductive provers (2015)
  13. Johansson, Moa; Rosén, Dan; Smallbone, Nicholas; Claessen, Koen: Hipster: integrating theory exploration in a proof assistant (2014)
  14. Claessen, Koen; Johansson, Moa; Rosén, Dan; Smallbone, Nicholas: Automating inductive proofs using theory exploration (2013)