Early Stage Researcher at UU

UU - Utrecht University (Netherlands) Department of Information and Computing Sciences

Universiteit Utrecht (UU)
Department of Information and Computing Sciences
Heidelberglaan 8,
Utrecht 3584 CS


  • +3
  • @


  • @

Explaining Logical Formulas

PhD research topic


Mathematical Logic plays an important role in many areas of study, including Artificial Intelligence, Philosophy, and Linguistics. Yet students and users of mathematical logic sometimes struggle to grasp the exact meaning of logical formulas. This happens when formulas are very complex, or when they have an unusual structure (for example when they are produced by a computational theorem prover). It also happens when learners are not yet fully accustomed to the conventions employed by the logic (e.g., the meaning of connectives in the so-called paradoxes of material implication).

To investigate how Natural Language Generation (NLG) techniques can be employed to automatically and effectively explain logical formulas to non-experts using texts that are formulated in ordinary language (e.g., in English, Dutch, or Chinese), the candidate will investigate computational techniques for simplifying and translating logical formulas into optimally intelligible NL text, and empirically evaluating the usefulness of the resulting text for users.

A key task is to convert a given formula into a form that makes it most intelligible to people, for example by removing parts of the formula that follow from background knowledge, and by exploiting particular strengths of Natural Language. But Natural Language has weaknesses as well: an important challenge is to minimize textual ambiguities (e.g., when a sentence is produced that can be parsed in two different ways). The project will focus on First-Order Predicate Logic in the first instance, and on producing explanations in English. Results in an additional language (e.g., Chinese or Dutch, both of which are studied actively in the department) will be welcome.

Expected Results:

– Algorithms for finding the simplest formula equivalent to a given input logical formula, given some background axioms.

– Algorithms for expressing the content of a (simplified) logical formula in Natural Language text.

– An interface that allows a user to enter an input formula and background axioms, and that produces different types of Natural Language output (i.e., using a range of simplification strategies).

– Evaluation results regarding the effectiveness for human users of the above techniques