InKa - an inductive theorem prover. InKa: INduktionsbeweiser KArlsruhe is a semi-automated inductive theorem prover actively developed from 1985 till 1999. It is written in LISP (two versions: CMU-Lisp and Allegro-Lisp) and TCL/TK.
Keywords for this software
References in zbMATH (referenced in 9 articles )
Showing results 1 to 9 of 9.
- Aoto, Takahito: Sound lemma generation for proving inductive validity of equations (2008)
- Kohlhase, Michael; Franke, Andreas: MBase: Representing knowledge and context for the integration of mathematical software systems (2001)
- Walther, Christoph; Kolbe, Thomas: On terminating lemma speculations. (2000)
- Walther, C.; Kolbe, T.: Proving theorems by reuse (2000)
- Basin, David A.; Walsh, Toby: A calculus for and termination of rippling (1996)
- Bronsard, Francois; Reddy, Uday S.; Hasker, Robert W.: Induction using term orders (1996)
- Kraan, Ina; Basin, David; Bundy, Alan: Middle-out reasoning for synthesis and induction (1996)
- Barnett, Richard; Basin, David; Hesketh, Jane: A recursion planning analysis of inductive completion (1993)
- Protzen, Martin: Disproving conjectures (1992)