Meetings

July 2012 (Strasbourg)

Participants: Xiaoyu Chen, Predrag Janicic, Julien Narboux, Pascal Schreck and Pascal Mathis

• Pascal Mathis:
  • Geometric constraints in CAD

• Julien Narboux:
  • Representation change formalization of geometry in Coq.

• Predrag Janicic:
  • GCLC, Construction problems, Coherent Logic and all that.

• Pascal Schreck:
  • GCMLa geometric constraint mark-up language,
  • geometric construction problems in CAL and Progé,
  • Ruler and Compass constructibility.

private comments

September 2012 (Strasbourg)

Participants: Filip Maric, Julien Narboux, Pascal Schreck

Filip Maric: Formalization of Poincarré disc model

Julien Narboux: Formalization of High-School Geometry

December 2012 (Belgrade)

Participants: Predrag Janicic, Filip Maric, Vesna Marinkovic Danijela Petrovic, Ivan Petrovic, Sana Stojanovic, Julien Narboux and Pascal Schreck

Weather: snow, (bodyguard: Milan)

Subjects:

• CL based automated formalization of Tarski, TPTP formats (Julien, Pascal, Sana, Predrag).
• Formalizing Avigad's axiomatizaton (Julien, Pascal, Sana, Filip, Predrag)
• Algebraic theorem provers (Julien, Pascal, Ivan, Danijela, Filip, Predrag)
• ARGO seminar - two talks by Pascal and Julien
• Formalization of Tarski and Hilbert + hyperbolic geometry (Julien, Pascal, Danijela, Filip).
• Defining high school goemetry knowledge base (Julien, Pascal, Filip).
• Construction problems and integrated solver (Julien, Pascal, Vesna, Predrag).
• Repository of goemetry resources (Julien, Pascal, Filip, Predrag)

Documents:

• talk of Julien for ARGO seminar

• talk of Pascal for ARGO seminar
  • About RC-(un)constructibily