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 4 articles )
Showing results 1 to 4 of 4.
- Eberhard, Sebastian; Hetzl, Stefan: Inductive theorem proving based on tree grammars (2015)
- Grechanik, S.A.: Proving properties of functional programs by equality saturation (2015)
- Rosén, Dan; Smallbone, Nicholas: TIP: tools for inductive provers (2015)
- Claessen, Koen; Johansson, Moa; Rosén, Dan; Smallbone, Nicholas: Automating inductive proofs using theory exploration (2013)