NLSR Home Page

Sponsored by FoLLI icon


NLSR is a forum to gather researchers interested in the natural language aspects of:

  • Multilingual on-line accessible mathematical content
  • Advanced tools for automated and interactive theorem proving and problem solving.
  • Rigorous reasoning methods and tools;
  • Formal methods and tools (making them more accessible to non-experts).
  • Generating explanations from business rules.

Call for Papers

Call for Papers



The complexity of ATP and ITP makes them only usable by experts.  One of the cornerstones of addressing a more general audience is the ability to be queried and to generate results in natural language. This necessity is palpable from the fact that many systems in the TP community (Coq, Isabelle, PROVERB, Nuprl, P.rex, THEOREMA, etc.) try hard to make proofs as close as possible to the "natural language'' of mathematicians.

In the area of education, intelligent tools such as automated and interactive theorem provers, the automatic discovery of properties, tools, problems repositories, the formalisation of theories fragments, etc., can bring a whole new dimension to mathematical education. The current development of these tools is focused on usability for experts, and it is still a major challenge to make such tools ready for widespread use. However, for some tools it seems to be the right time to begin addressing the next challenge, i.e., to link and adapt them for specific educational needs.

On the side of language technology, some dialog managers use theorem provers to drive the underlying logic and controlled natural languages exist based on abstract representations compatible to the ones used in reasoners. A third aspect comes from formal representation of mathematics with the aim of automatic checking or translation of existing material.

It is important to have a meeting to explore collaboration for effective translation of machine and human-readable form, including sentence planning, robust parsing of natural language, multi-linguality and fluency of the result.

Previous conferences on this area: ThEduCNL.




Program committee

Scientific committee:

  • Yannis Haralambous (Telecom Bretagne);
  • Bengt Nordström (Chalmers University of Technology).