ProofWeb is both a system for teaching logic and for using proof assistants through the web.
ProofWeb can be used in three ways. First, one can use the guest login, for which one does not even need to register. Secondly, a user can be a student in a logic or proof assistants course. We are hosting courses free of charge. If you are a teacher and would like to host your course on this server, send email to proofweb@cs.ru.nl. Thirdly, if teachers do not want to trust us with their students' files, they can freely download the ProofWeb system and run it on a server of their own.
HOL4 is the latest version of the HOL interactive proof assistant for higher order logic: a programming environment in which theorems can be proved and proof tools implemented. Built-in decision procedures and theorem provers can automatically establish many simple theorems (users may have to prove the hard theorems themselves!) An oracle mechanism gives access to external programs such as SAT and BDD engines. HOL 4 is particularly suitable as a platform for implementing combinations of deduction, execution and property checking. several widely used versions of the HOL system: 1. HOL88 from Cambridge; 2. HOL90 from Calgary and Bell Labs; 3. HOL98 from Cambridge, Glasgow and Utah. HOL 4 is the successor to these. Its development was partly supported by the PROSPER project. HOL 4 is based on HOL98 and incorporates ideas and tools from HOL Light. The ProofPower system is another implementation of HOL.
IsaPlanner is a generic framework for proof planning in the interactive theorem prover Isabelle. It facilitates the encoding of reasoning techniques, which can be used to conjecture and prove theorems automatically. The system provides an interactive tracing tool that allows you to interact the proof planning attempt. (see the screenshot of IsaPlanner being used with Isabelle and Proof General) It is based on the Isabelle theorem prover and the Isar language. The main proof technique written in IsaPlanner is an inductive theorem prover based on Rippling. This is applicable within Isabelle's Higher Order Logic, and can easily be adapted to Isabelle's other logics. The system now the main platform for proof planning research in the Edinburgh mathematical reasoning group
T. Mossakowski, and A. Tarlecki. 17th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), volume 8412 of Lecture Notes in Computer Science, page 441-456. Springer-Verlag Berlin Heidelberg, (2014)
K. Heng. (2014)cite arxiv:1404.6248Comment: Published in American Scientist: Volume 102, Number 3, Pages 174 to 177 (http://www.americanscientist.org/issues/pub/2014/3/the-nature-of-scientific-proof-in-the-age-of-simulations).
M. Codescu, and T. Mossakowski. Algebra and Coalgebra in Computer Science, CALCO'11, volume 6859 of Lecture Notes in Computer Science, page 145-160. Springer, (2011)
M. Schiller, and C. Benzmüller. Artificial Intelligence in Education -- Building Learning Systems tat Care: From Knowledge Representation to Affective Modelling, 200, page 599--601. Amsterdam, IOS Press, (2009)
T. Mossakowski, A. Haxthausen, D. Sannella, and A. Tarlecki. Logics of formal specification languages, volume 22 of Monographs in Theoretical Computer Science, chapter 3, Springer-Verlag Heidelberg, (2008)
T. Mossakowski, C. Maeder, and K. Lüttich. TACAS 2007, volume 4424 of Lecture Notes in Computer Science, page 519-522. Springer-Verlag Heidelberg, (2007)
H. Cao, and X. Zhu. (2006)cite arxiv:math/0612069Comment: This is a revised version of the article by the same authors that originally appeared in Asian J. Math., 10(2) (2006), 165--492.
R. Gheyi, T. Massoni, and P. Borba. ASE '05: Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering, page 372--375. New York, NY, USA, ACM, (2005)
N. Matsuda, and K. VanLehn. Proceedings of The 12th International Conference on Artificial Intelligence in Education, page 443 -- 450. Amsterdam, IOS Press, (2005)
T. Mossakowski, P. Hoffman, S. Autexier, and D. Hutter. CASL Reference Manual, volume 2960 of Lecture Notes in Computer Science, chapter ÏV, Springer Verlag, London, Ëdited by T. Mossakowski.(2004)
G. Delzanno. Electronic Notes in Theoretical Computer Science, 50 (4):
371--385(2001)VEPAS 2001, Verification of Parameterized Systems (Satellite Workshop of ICALP 2001).
F. Arzarello. the 24th Conference of the International Group for the Psychology of Mathematics Education (PME), 1, page 23--38. Hiroshima, Japan, (2000)
J. Paakki. Conference record of POPL '94, 21st ACM SIGPLAN-SIGACT Symposium
on Principles of Programming Languages: papers presented at the Symposium:
Portland, Oregon, January 17--21, 1994, page 361--374. New York, NY, USA, ACM Press, (1994)
T. Huang, and J. Lin. Proceedings of the 1994 International Conference on Parallel and Distributed Systems, page 759--768. Washington, DC, USA, IEEE Computer Society, (1994)
J. Søgaard-Andersen, S. Garl, J. Guttag, N. Lynch, and A. Pogosyants. PROCEEDINGS OF THE 5TH INTERNATIONAL CONFERENCE ON COMPUTER AIDED VERIFICATION, ELOUNDA, GREECE, VOLUME 697 OF LECTURE, page 305--319. Springer Verlag, (1993)
E. Stark. Foundations of Software Technology and Theoretical Computer Science, volume 206 of Lecture Notes in Computer Science, Springer Berlin / Heidelberg, (1985)