Deduction using the ProofWeb system (2009)
Cezary Kaliszyk, Femke Van Raamsdonk, Freek Wiedijk, Maxim Hendriks, Roel De Vrijer
This is the manual of the ProofWeb system that was implemented at the Radboud University Nijmegen and the Free University Amsterdam in the SURF education innovation project Web deduction for...
Computing with Classical Real Numbers (2008)
Kaliszyk, Cezary, O'Connor, Russell
There are two incompatible Coq libraries that have a theory of the real numbers; the Coq standard library gives an axiomatic treatment of classical real numbers, while the CoRN library from Nijmegen...
Teaching logic using a state-of-the-art (2008)
Cezary Kaliszyk, Freek Wiedijk, Maxim Hendriks, Femke Raamsdonk
proof assistant
Certified Computer Algebra on top of an Interactive Theorem Prover (2008)
Cezary Kaliszyk, Freek Wiedijk
1 Introduction Computer algebra systems do not always give correct answers. This happensbecause those systems do not certify the operations performed. There can be various reasons for errors in a...
Institute for Computing and Information Sciences, (2008)
Cezary Kaliszyk, Freek Wiedijk
Abstract. We present a prototype of a computer algebra system that is built on top of a proof assistant, HOL Light. This architecture guarantees that one can be certain that the system will make no...
Teaching logic using a state-of-the-art (2008)
Cezary Kaliszyk, Freek Wiedijk, Maxim Hendriks, Femke Raamsdonk
proof assistant
SIE -- Intelligent Web Proxy Framework (2008)
Grzegorz Andruszkiewicz Andruszkiewicz, Cezary Kaliszyk
In this paper we would like to present and describe SIE, a transparent, intelligent Web proxy framework. Its aim is to provide efficient and robust platform for implementing various ideas in broad...