All

What are you looking for?

All
Projects
Results
Organizations

Quick search

  • Projects supported by TA ČR
  • Excellent projects
  • Projects with the highest public support
  • Current projects

Smart search

  • That is how I find a specific +word
  • That is how I leave the -word out of the results
  • “That is how I can find the whole phrase”

Automating Formalization by Statistical and Semantic Parsing of Mathematics

The result's identifiers

  • Result code in IS VaVaI

    <a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F17%3A00319005" target="_blank" >RIV/68407700:21730/17:00319005 - isvavai.cz</a>

  • Result on the web

    <a href="https://doi.org/10.1007/978-3-319-66107-0_2" target="_blank" >https://doi.org/10.1007/978-3-319-66107-0_2</a>

  • DOI - Digital Object Identifier

    <a href="http://dx.doi.org/10.1007/978-3-319-66107-0_2" target="_blank" >10.1007/978-3-319-66107-0_2</a>

Alternative languages

  • Result language

    angličtina

  • Original language name

    Automating Formalization by Statistical and Semantic Parsing of Mathematics

  • Original language description

    We discuss the progress in our project which aims to automate formalization by combining natural language processing with deep semantic understanding of mathematical expressions. We introduce the overall motivation and ideas behind this project, and then propose a context-based parsing approach that combines efficient statistical learning of deep parse trees with their semantic pruning by type checking and large-theory automated theorem proving. We show that our learning method allows efficient use of large amount of contextual information, which in turn significantly boosts the precision of the statistical parsing and also makes it more efficient. This leads to a large improvement of our first results in parsing theorems from the Flyspeck corpus.

  • Czech name

  • Czech description

Classification

  • Type

    D - Article in proceedings

  • CEP classification

  • OECD FORD branch

    10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Result continuities

  • Project

    <a href="/en/project/EF15_003%2F0000466" target="_blank" >EF15_003/0000466: Artificial Intelligence and Reasoning</a><br>

  • Continuities

    P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Others

  • Publication year

    2017

  • Confidentiality

    S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Data specific for result type

  • Article name in the collection

    Interactive Theorem Proving

  • ISBN

    978-3-319-66106-3

  • ISSN

  • e-ISSN

  • Number of pages

    16

  • Pages from-to

    12-27

  • Publisher name

    Springer

  • Place of publication

    Basel

  • Event location

    Brasilia

  • Event date

    Sep 26, 2017

  • Type of event by nationality

    WRD - Celosvětová akce

  • UT code for WoS article