Abstract
In this article, we first briefly present a proof assistant called the Predicate Prover, which essentially offers two functionalities: (1) an automatic semi-decision procedure for First Order Predicate Calculus, and (2) a systematic translation of statements written within Set Theory into equivalent ones in First Order Predicate Calculus. We then show that the automatic usage of this proof assistant is limited by several factors. We finally present (and this is the main part of this article) the principles that we have used in the construction of a proactive interface aiming at circumventing these limitations. Such principles are based on our practical experience in doing many interactive proofs (within Set Theory).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abrial, J.-R., Cansell, D., Lafitte, G.: Higher-Order Mathematics in B. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 370–393. Springer, Heidelberg (2002)
Abrial, J.R.: The B Book – Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996) ISBN 0-521-49619-5
Aspinall, D.: LEGO Manual version 1.3.1. Edimburgh University, Edimburgh (1998), www.lama.dcs.ed.ac.uk/home/lego
Aspinall, D.: Proof general – a generic tool for proof development. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, p. 38. Springer, Heidelberg (2000)
Barras, B., Boutin, S., Cornes, C., Courant, J., Coscoy, Y., Delahaye, D., de Rauglaudre, D., Filliâtre, J.C., Giménez, E., Herbelin, H., Huet, G., Laulhère, H., Loiseleur, P., Muñoz, C., Murthy, C., Parent, C., Paulin, C., Saïbi, A., Werner, B.: The Coq Proof Assistant Reference Manual – Version V6.3 (July 1999)
ClearSy, Aix-en-Provence (F).Atelier B, Version 3.6 (2001), http://www.atelierb.societe.com
Fitting, M.: First-order logic and automated theorem proving, 2nd edn. Springer, New York (1996)
Gordon, M.J.C.: Hol: A proof generating system for higher-order logic. In: Birtwistle, G., Subrahmanyam, P.A. (eds.) VLSI Specification, Verification and Synthesis, pp. 73–128 (1988)
Hutter, D., Langenstein, B., Sengler, C., Siekmann, J.H., Stephan, W.: Deduction in the verificationsupport environment (vse). In: Gaudel, M.-C., Woodcock, J.C.P. (eds.) FME 1996. LNCS, vol. 1051. Springer, Heidelberg (1996)
Kalman, J.A.: Automated reasoning with Otter. Rinton Press (2001)
Owre, S., Shankar, N., Rushby, J.M.: The PVS specification language. Technical report, SRI International, June 14 (1993)
Paulson, L.: Isabelle. LNCS, vol. 828. Springer, Heidelberg (1994)
Raffalli, C.: The Phox proof assistant version 0.8. Université de savoie, Chambéry (F) (2002)
Kahn, G., Bertot, Y., Théry, L.: Proof by Pointing. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789. Springer, Heidelberg (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Abrial, JR., Cansell, D. (2003). Click’n Prove: Interactive Proofs within Set Theory. In: Basin, D., Wolff, B. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2003. Lecture Notes in Computer Science, vol 2758. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10930755_1
Download citation
DOI: https://doi.org/10.1007/10930755_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40664-8
Online ISBN: 978-3-540-45130-3
eBook Packages: Springer Book Archive