References
L. Bachmair, N. Dershowitz, and J. Hsiang. Orderings for equational proofs. In Proceedings 1st IEEE Symposium on Logic in Computer Science, Cambridge (Massachusetts, USA), pages 346–357. IEEE, 1986.
A. Bouhoula, E. Kounalis, and M. Rusinowitch. Automated mathematical induction. Technical Report 1636, INRIA, 1992.
A. Bouhoula. Preuve automatique par paramodulation, réécriture et induction. Rapport interne 91-R-204, Centre de Recherche en Informatique de Nancy, Vandœuvre-lès-Nancy, 1991.
B. el Ayeb, P. Marquis, and M. Rusinowitch. Conjecturing diagnoses. Technical Report 92-LE-LAB-001, Université Sherbrooke, Canada, January 1992. Submitted.
J. Hsiang and M. Rusinowitch. Proving refutational completeness of theorem proving strategies: The transfinite semantic tree method. Journal of the Association for Computing Machinery, 38(3):559–587, July 1991.
E. Kounalis and M. Rusinowitch. On word problem in Horn logic. In J.-P. Jouannaud and S. Kaplan, editors, Proceedings 1st International Workshop on Conditional Term Rewriting Systems, Orsay (France), volume 308 of LNCS, pages 144–160. Extended version in Journal of Symbolic Computation, 11(1 & 2), 1991.
E. Kounalis and M. Rusinowitch. Mechanizing inductive reasoning. Bulletin of European Association for Theoretical Computer Science, 41:216–226, June 1990.
P. Lescanne. Implementation of completion by transition rules + control: ORME. In H. Kirchner and W. Wechler, editors, Proceedings 2nd International Workshop on Algebraic and Logic Programming, Nancy (France), volume 463 of LNCS, pages 262–269. Springer-Verlag, 1990.
Pelletier, Francis, and Jeffry. Seventy five problems for testing automatic theorem provers. Journal of Automated Reasoning, pages 191–216, 1986.
Projet Formel Inria. The CAML Reference Manual, March 1989. Version 2.6.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bouhoula, A., Kounalis, E., Rusinowitch, M. (1992). SPIKE, an automatic theorem prover. In: Voronkov, A. (eds) Logic Programming and Automated Reasoning. LPAR 1992. Lecture Notes in Computer Science, vol 624. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0013087
Download citation
DOI: https://doi.org/10.1007/BFb0013087
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55727-2
Online ISBN: 978-3-540-47279-7
eBook Packages: Springer Book Archive