ISABELLE est un environnement logiciel permettant de définir des systèmes de déduction et de les utiliser pour prouver des théorèmes. Un certain nombre de théories ou logiques sont déja implémentées et peuvent être directement utilisées.
