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). © Springer-Verlag Berlin Heidelberg 2003.
CITATION STYLE
Abrial, J. R., & Cansell, D. (2003). Click’n prove: Interactive proofs within set theory. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2758, 1–24. https://doi.org/10.1007/10930755_1
Mendeley helps you to discover research relevant for your work.