La vérification de preuves avec PhoX

Le logiciel PhoX permet l'écriture et la vérification de preuves en interaction avec l'ordinateur. Pour récupérer le logiciel, des informations à son sujet, ... le site de référence de PhoX est maintenu par le créateur et principal développeur du logiciel, Christophe Raffalli. On y trouve le manuel de référence en ligne ou pour impression.

ce logiciel est utilisé pour l'enseignement de la logique en licence depuis quelques années à l'université de Chambéry, et depuis l'année 2001-2002, à l'université Paris 7.

Voici un petit polycopié d'introduction à l'utilisation de PhoX distribué aux étudiants à Paris 7. Il est partiellement inspiré d'un document relatant l'expérience d'enseignement de Chambéry.

Le fichier intro_quest.phx est destiné à l'apprentissage des premières notions de PhoX : définir une théorie, preuves élémentaires utilisant les connecteurs propositionnels usuels, l'égalité et le quantificateur universel.

Le fichier intro2_quest.phx est la suite du précédent : preuves élémentaires utilisant le quantificateur existentiel, un usage (très partiel) de l'opérateur de description définie.