Skip to content
Snippets Groups Projects
index.md 2.43 KiB
Newer Older
  • Learn to ignore specific revisions
  • Michael Kohlhase's avatar
    Michael Kohlhase committed
    ---
    layout: default
    title: Home
    ---
    
    
    The ability to *represent knowledge about the world* and to *draw logical inferences* is one of the central components of intelligent behavior, as a consequence, reasoning components of some form are at the heart of many artificial intelligence systems.
    
    
    Michael Kohlhase's avatar
    Michael Kohlhase committed
    #### Research
    
    The KWARC research group conducts research in knowledge representation and reasoning techniques with a view towards applications in knowledge management. 
    We extend techniques from [formal methods](http://kwarc.info/semantics.html#fm) so that they can be used in settings where formalization is either infeasible or too costly. 
    We concentrate on developing techniques for marking up the [structural semantics](http://kwarc.info/semantics.html#ssem) in technical documents. 
    This level of markup allows for offering interesting [knowledge management services](http://kwarc.info/projects/) without forcing the author to formalize the document contents.
    
    
    Michael Kohlhase's avatar
    Michael Kohlhase committed
    ##### Approach: Corpus-based Meta-Mathematics
    
    Michael Kohlhase's avatar
    Michael Kohlhase committed
    In this title we have three components that warrant explanation: 
    
    Michael Kohlhase's avatar
    Michael Kohlhase committed
    1. **Mathematics**: we use the  mathematical knowledge and mathematical documents as a test
    
    Michael Kohlhase's avatar
    Michael Kohlhase committed
      tube for our research as the knowledge and document structures are quite explicit and
      overt and the content of mathematics is well-understood. Anything that has the same
      properties we consider to be "mathematics" as well. 
    
    Michael Kohlhase's avatar
    Michael Kohlhase committed
    2. **Meta**: we develop Meta-Artefacts, i.e. we
    
    Michael Kohlhase's avatar
    Michael Kohlhase committed
       * design **representation languages** (logics) that allow to talk *about* mathematical objects,
       their properties, and relations,
       * invent **algorithms** that analyze and transform these representations, and
       * implement them in **end-user systems** that utilize both. 
    
    Michael Kohlhase's avatar
    Michael Kohlhase committed
    3. **Corpus-based**: we do this as a natural science by looking at data (i.e. corpora of
    
    jfschaefer's avatar
    jfschaefer committed
    documents and formalizations).
    
    Michael Kohlhase's avatar
    Michael Kohlhase committed
    ##### KWARC Process
    
    Michael Kohlhase's avatar
    Michael Kohlhase committed
    We approach Corpus-Based Meta-Mathematics (iteratively) in three steps:
    1. **Analysis**: we analyze the corpora for patterns and structures.
    2. **Synthesis**: we design and build meta-artefacts (languages, algorithms, and systems)
    and derive data sets from the corpora.
    
    Michael Kohlhase's avatar
    Michael Kohlhase committed
    3. **Experimentation**: we evaluate the representation languages and algorithms on the
    
    Michael Kohlhase's avatar
    Michael Kohlhase committed
       corpora and the systems on end users (mathematicians).
    
    Michael Kohlhase's avatar
    Michael Kohlhase committed
    #### Recent News ([see all](/news/))
    
    Michael Kohlhase's avatar
    Michael Kohlhase committed
     
    
    Tom Wiesing's avatar
    Tom Wiesing committed
    <ul class="collection">
        {% for post in site.posts limit:5 %}
    
    Tom Wiesing's avatar
    Tom Wiesing committed
            {% include post_link.html post=post %}
    
    Tom Wiesing's avatar
    Tom Wiesing committed
        {% endfor %}
    
    Michael Kohlhase's avatar
    Michael Kohlhase committed
    </ul>
    
    Michael Kohlhase's avatar
    Michael Kohlhase committed
    
    <!--  LocalWords:  endfor analyze
     -->