Mud for Agda

Automatically transform Natural Language into Agda with Mud provides a complete symbolic derivation
from Natural Language Statements to Agda, using Lambeq, CCG, λ-Calculus, and Dependent Type Theory.

Try it Out · Learn Agda · Report Bug · Request Feature

What is Mud Theorem Prover?

Mud is a symbolic theorem prover designed to reason with Natural Langauge statements through the derivation of dependent types, expressed in Agda. This work is inspired by research led by Aarne Ranta, Robin Cooper and aims to provide an automated, end-to-end type-theoretic implementation of natural language reasoning.

• Easily translate, and formalise natural language statements into a dependent-type theory.
• Prove properties between natural langauge statements, i.e. entailment & contradiction.
• Visualise and understand step-by-step derivations on our dedicated web compiler.

How does Mud Theorem Prover work?

Each lexeme (word) in a natural language statement is assigned a part-of-speech tag, e.g. verb, noun, adverb. Then, syntactic-categories are derived and the sentence is reduced as a tree like structure to a base type S (Sentence), these categories include bi-directional functor types that when applied can reduce the sentence. From here, we map rules in the CCG to type-theoretic derivations (similar to Montague's Universal Grammar), and compile to Agda. For more information on the details of how this works, please refer to our paper.

1. Words are tagged using a Brill Tagger, a transformational system.
2. CCG is generated, each word maps to a syntactic type.
3. Functors in the CCG are converted to λ-Calculus, with types being inferred.
4. Code is generated (by records) to Agda
5. Agsy (or auto tactics) are used to fill the theorem hole, providing a constructive proof.

Contributors

Mud Theorem Prover is designed, and developed by Amber Swarbrick and Toby Clark in a joint-disseration for masters in Computer Science under the supervision of Professor. Thorsten Altenkirch at University of Nottingham. If you're interested in contributing, have a question or are interested, please get in touch!