Small TYPES workshop Curry-Howard Implementation Techniques/Connecting Humans and Type-checkers 2006 The CHIT Workshop discuss implementation issues.Keywords: * Terms and binders * Type inference, type constraints and unification * Reduction, evaluation and compilation * Proof refinement/Proof engine * State handling, library, modules, saving format * Coercions * Termination checking The CHAT workshop will focus on interaction between users and proof environments, graphical interfaces, and on network-based interaction. Keywords: * Declarative versus procedural proof styles (structured proofs, XML) * Web based interfaces (including cooperative environments) * Libraries and information retrieval (including search engines) * Proof documentation (literate proving) * Protocols for UI-interaction
ProofWeb is a system for practising natural deduction on the computer based on the Coq proof assistant and runs in browser. ProofWeb one runs logic exercises on a web server. ProofWeb comes with a database of basic logic exercises that are graded according to difficulty. The ProofWeb system automatically grades the exercises of the students. user talks to the Coq system on the server without any translation. There just are a few additional tactics to make Coq's behavior follow the logic textbooks. This means that in ProofWeb the full power of Coq is available, even to beginner students. On the other hand ProofWeb tries hard to present deductions exactly the way they look in the textbooks. In particular ProofWeb exactly follows the conventions of a well-known logic textbook Logic in Computer Science: Modelling and Reasoning about Systems by Michael Huth and Mark Ryan.
Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. Isabelle is developed at University of Cambridge (Larry Paulson) and Technische Universität München (Tobias Nipkow). See the Isabelle overview for a brief introduction. Now available: Isabelle2008 Some notable improvements: * HOL: significant speedup of Metis prover; proper support for multithreading. * HOL: new version of primrec command supporting type-inference and local theory targets. * HOL: improved support for termination proofs of recursive function definitions. * New local theory targets for class instantiation and overloading. * Support for named dynamic lists of theorems.
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
This site is an experimental HTML rendering of fragments of the IsarMathLib project. IsarMathLib is a library of mathematical proofs formally verified by the Isabelle theorem proving environment. The formalization is based on the Zermelo-Fraenkel set theory. The Introduction provides more information about IsarMathLib. The software for exporting Isabelle's Isar language to HTML markup is at an early beta stage, so some proofs may be rendered incorrectly. In case of doubts, compare with the Isabelle generated IsarMathLib proof document.
* Higher-Order Logic * o HOL (Higher-Order Logic) o HOLCF (Higher-Order Logic of Computable Functions) * First-Order Logic * o FOL (Many-sorted First-Order Logic) o ZF (Set Theory) o CCL (Classical Computational Logic) o LCF (Logic of Computable Functions) o FOLP (FOL with Proof Terms) * Miscellaneous * o Sequents (first-order, modal and linear logics) o CTT (Constructive Type Theory) o Cube (The Lambda Cube)