Lab for Automated Reasoning and Analysis LARA

Resources and papers on semantic-enriched text


Computational Semantics


Textual Inference

Machine Reading

Type Coercion

Semantic-web work

Semantic Annotation

Controlled languages

Controlled languages are interesting in technical domains. On the one hand, one can formula first-order logic in english-like formalism, but that remains first-order logic. Similarly, one can simply restrict English to a smaller vocabulary, without providing formal semantics for such restricted language. There is a large space of possibilities of combining these two directions.

Translation: Controlled English for Knowledge-Based Machine Translation

Controlled Language and Decription Logics: CalvaneseNaturalLanguageDL1, CalvaneseNaturalLanguageDL2

Documentation Systems

  • Presenting Theories, Chapter 4 in Isabelle tutorial
  • documentation systems such as JavaDOC, OcamlDoc, Web etc. usually have a subset of features of Isabelle documentation

Precise natural language understanding

These two dissertations are examples of work on natural language processing that uses explicit precise semantic models (as opposed to implicitly encoding semantic information, if at all):

Uses of natural language in specifying and verifying program properties

Introducing natural language program analysis,

We can also give English text representation to meanings of specification languages for software. The KeY project did this for OCL language in the UML modelling language:

Natural Language Specifications, note the quote: “However, the provided natural language translations are on the same ab- straction level as the original OCL specifications (as noted above). The intended reader of the translations must therefore be comfortable with this abstraction level. For instance, we cannot expect a translation of OCL specifications involving low-level implementation issues to be understandable to a customer.”

JACK tool had a part that translates English sentences to temporal logic (with some dialog for disambiguation):

The Integration Project for the JACK Environement (1994)

Obtaining Models for Test Generation from Natural Language-Like Functional Specifications

Debugging method names and related papers

Computational Law

Programming and Natural Languages

Natural language generation

If we have precise semantic representation, generating natural language text from it is easier than generating semantic representation from natural language text. Therefore, exploring natural language generation for semantic representations is very relevant.

Overview of NL generation

Verbalization of High-Level Formal Proofs

Special issue of JAPL, esp. Supporting the formal verification of mathematical texts


Statistical reasoning

Some general links on statistical reasoning (if relevant):


Mallet tools from UMass Amherst and Similar software

Research groups


semantic.txt · Last modified: 2013/10/20 23:40 by vkuncak