LogiCoq
--- Introduction ---

LogiCoq est un ensemble d'exercices de logique dont les démonstrations sont faites interactivement à l'aide de l'assistant de preuve Coq.

Pour une introduction à Coq (en anglais), on peut lire le Tutorial .


Vous pouvez choisir un exercice d'initiation,

ou un exercice tiré du Tutorial de Coq

ou un exercice parmi ceux proposés et démontrés par les utilisateurs,

ou bien donner votre énoncé (dans la syntaxe de Coq, pour l'instant...):

puis le

Si vous le démontrez, il pourra faire partie des exercices proposés par les utilisateurs...


Cette page n'est pas dans son apparence habituelle parce que WIMS n'a pas pu reconnaître votre navigateur de web.

Pour accéder aux services de WIMS, vous avez besoin d'un navigateur qui connait les formes. Afin de tester le navigateur que vous utilisez, veuillez taper le mot wims ici : puis appuyez sur ``Entrer''.

Veuillez noter que les pages WIMS sont générées interactivement; elles ne sont pas des fichiers HTML ordinaires. Elles doivent être utilisées interactivement EN LIGNE. Il est inutiles pour vous de les ramassez par un programme robot.

Description: preuves interactives de la logique de premier ordre. This is the main site of WIMS (WWW Interactive Multipurpose Server): interactive exercises, online calculators and plotters, mathematical recreation and games

Keywords: wims, mathematics, mathematical, math, maths, interactive mathematics, interactive math, interactive maths, mathematic, online, calculator, graphing, exercise, exercice, puzzle, calculus, K-12, algebra, mathématique, interactive, interactive mathematics, interactive mathematical, interactive math, interactive maths, mathematical education, enseignement mathématique, mathematics teaching, teaching mathematics, algebra, geometry, calculus, function, curve, surface, graphing, virtual class, virtual classes, virtual classroom, virtual classrooms, interactive documents, interactive document, logic, logic, proof