A shell for generic interactive proof search. (English) Zbl 0955.03503


03B35 Mechanization of proofs and logical operations
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI


[1] Rasiowa, H. and Sikorski, R. 1963. ”The Mathematics of Metamathematics, Warszawa”. · Zbl 0122.24311
[2] Barwise, J. and Etchemendy, J. 1994. ”Hyperproof. CSLI”. · Zbl 0860.03004
[3] MacLogic. 1991. ”MALT project St Andrews University”.
[4] Feferman S., The number systems (1963) · Zbl 0117.25803
[5] Smirnov, V. 1972. ”Formal inference and logical calculus, Moscow”. (in Russian)
[6] Smirnov, V. 1990. ”Moscow”. Logic and computer. (in Russian)
[7] Smirnov, A. and Novodvorsky, A. 1993. ”Logical systems description language, ILCSDP, Moscow”.
[8] Suppes, P. 1990. ”Uses of Artificial Intelligence in computer-based instruction. In Artificial Intelligence in Higher Education. Springer-Verlag”.
[9] Constable, R. L. 1986. ”Implementing Mathematics with the NuPRL proof development system”. Prentice-Hall”. .
[10] Dowek, G. 1991. ”The Coq Proof Assistant User’s Guide”. Rapport Technique INRIA”. .
[11] Caferra, R. and Herment, M. 1993. ”GLEFatinf, A Graphic Framework for Combining Provers and Editing Proofs for Different Logics,” Proc. DISG’0’93, LNCS 722, Springer-Verlag”. · Zbl 0836.68106
[12] Trybulec, A. and Blair, H. 1985. ”Computer aided reasoning”. Logic of programs, Brooklyn”. LNCS 193 · Zbl 0568.68070
[13] Bertot, Y., Kahn, G. and Thery, L. 1994. ”Proof by Pointing” Proc. TACS’94, LNCS 789, Springer-Verlag”.
[14] Limongelli C., ”Design and implementation of symbolic computation systems, Proc. IFIP W.G. 2.5 Conference (1991)
[15] Paulson L. C., Journal of automated reasoning 5 (1989) · Zbl 0679.68173
[16] Harper R., Proc. of the 2nd Annual Logic in Computer Sc. Conf (1987)
[17] Sawamura H., Proc 7th Int. Conf on Logic Programming (1990)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.