The Lurch Deductive Engine (LDE) Source Code Documentation

This repository is in the process of rebuilding the LDE, discarding an old design and replacing it with a better, updated design. That work is still in progress, and is perhaps 50% complete.

The navigation menu on the left shows classes and namespaces in alphabetical order, but the overview below is more logically organized.

Tutorials

Probably the easiest way to get familiar with the classes and methods defined in this repository, together with how to use them, is to read the tutorials:

• Constructing LCs
• Methods in each LC subclass
• LC tree hierarchies
• Serialization and attributes of LCs
• Free and bound variables
• Connections among LCs
• Pattern matching
• Lurch Node REPL

Foundational classes

Every symbolic math software needs some data structure for storing trees of mathematical symbols that represent mathematical meaning. In the LDE, the most generic of these is the Math Concept.

Later, complex math concepts will be able to be compiled down to a set of simpler special cases that can be processed by the LDE. We call that simpler subset the Logic Concepts, or LCs for short.

Logic concepts come in three types: Environment, Declaration, and Expression.

Environments are either the base type, Environment, or a subclass called Binding Environment, which can bind symbols, such as when constructing subproofs about arbitrary variables.

Expressions come in three types: Symbol, Application, and Binding Expression.

Other tools

Other basic tools support the classes above, including:

• a class for connecting math concept instances irrespective of tree structure,
• functions for working with JSON and serializing it.

There is also a host of advanced tools for doing pattern matching with Logic Concept instances.

And when working in the test suite, feel free to import the Database module for access to a library of Logic Concept instances written in putdown notation, with corresponding metadata.

GitHub

Source code (including a README on how to set up your own development environment)

Design wiki (currently out-of-date; do not trust the content of that wiki until it has been updated, at which point we will update this note to reflect that it has been updated)