An experiment concerning mathematical proofs on computers with French undergraduate students

DOI10.1016/j.jal.2004.02.002zbMath1051.03502OpenAlexW2095241014MaRDI QIDQ1884267

René David, Christophe Raffalli

Publication date: 28 October 2004

Published in: Journal of Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jal.2004.02.002

zbMATH Keywords

proof assistant PhoX

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Problem books, competitions, examinations (aspects of mathematics education) (97U40)

Uses Software

• ACL2
• Coq
• Isabelle
• PVS
• Proof General
• HOL Light
• LEGO

Cites Work

• HOL Light: An Overview
• Mechanizing UNITY in Isabelle
• Unnamed Item
• Unnamed Item

This page was built for publication: An experiment concerning mathematical proofs on computers with French undergraduate students