Crate logicaffeine_language 

logicaffeine-language

Natural language to first-order logic transpilation pipeline.

This crate provides a complete system for parsing English sentences and producing formal logical representations in various notations.

Quick Start

use logicaffeine_language::compile;

let fol = compile("Every philosopher is wise.").unwrap();
assert!(fol.contains("∀"));

Architecture

The pipeline consists of several stages:

1. Lexer (lexer) - Tokenizes natural language input into a stream of Tokens, handling vocabulary lookup and morphological analysis.

2. Parser (parser) - Constructs a logical AST with discourse tracking via Discourse Representation Structures (drs).

3. Semantics (semantics) - Applies axiom expansion, Kripke lowering for modal logic, and intensional readings.

4. Transpiler (transpile) - Renders the AST to Unicode, LaTeX, or ASCII first-order logic notation.

Output Formats

Format	Example	Use Case
Unicode	∀x(P(x) → Q(x))	Terminal display
LaTeX	\forall x(P(x) \to Q(x))	Academic papers
SimpleFOL	Ax(P(x) -> Q(x))	ASCII-only environments
Kripke	Explicit world quantification	Modal logic analysis

Multi-Sentence Discourse

For pronoun resolution and anaphora across sentences, use Session:

use logicaffeine_language::Session;

let mut session = Session::new();
session.eval("A man walked in.").unwrap();
session.eval("He sat down.").unwrap(); // "He" resolves to "a man"

Ambiguity Handling

Natural language is inherently ambiguous. The crate provides several strategies:

• compile_forest - Returns all valid parse readings for lexical and structural ambiguity (noun/verb, PP attachment).

• compile_all_scopes - Returns all quantifier scope permutations (“Every woman loves a man” → surface and inverse readings).

Feature Flags

• dynamic-lexicon - Enable runtime lexicon loading via the runtime_lexicon module (when enabled)

Re-exports

pub use proof_convert::logic_expr_to_proof_expr;

pub use proof_convert::term_to_proof_term;

pub use token::BlockType;

pub use token::FocusKind;

pub use token::MeasureKind;

pub use token::PresupKind;

pub use token::Span;

pub use token::Token;

pub use token::TokenType;

pub use lexer::Lexer;

pub use lexer::LineLexer;

pub use lexer::LineToken;

pub use parser::Parser;

pub use parser::ParserMode;

pub use parser::NegativeScopeMode;

pub use parser::QuantifierParsing;

pub use error::ParseError;

pub use error::ParseErrorKind;

pub use error::socratic_explanation;

pub use drs::Drs;

pub use drs::BoxType;

pub use drs::WorldState;

pub use analysis::TypeRegistry;

pub use registry::SymbolRegistry;

pub use arena_ctx::AstContext;

pub use session::Session;

pub use compile::compile;

pub use compile::compile_simple;

pub use compile::compile_kripke;

pub use compile::compile_with_options;

pub use compile::compile_with_world_state;

pub use compile::compile_with_world_state_options;

pub use compile::compile_with_discourse;

pub use compile::compile_with_world_state_interner_options;

pub use compile::compile_all_scopes;

pub use compile::compile_all_scopes_with_options;

pub use compile::compile_forest;

pub use compile::compile_forest_with_options;

pub use compile::MAX_FOREST_READINGS;

pub use compile::compile_discourse;

pub use compile::compile_discourse_with_options;

pub use compile::compile_ambiguous;

pub use compile::compile_ambiguous_with_options;

pub use compile::compile_theorem;

Modules

analysis

Static analysis passes for type and policy discovery.

arena

arena_ctx

Arena context for AST allocation.

ast

Abstract Syntax Tree types for both logical expressions and imperative statements.

compile

Compilation API

debug

Debug display utilities for AST types with interner access.

drs

Discourse Representation Structure (DRS) for anaphora resolution and scope tracking.

error

Error types and display formatting for parse errors.

formatter

Output formatters for logical expressions.

intern

lambda

Lambda calculus transformations for Montague-style compositional semantics.

lexer

Two-stage lexer for LOGOS natural language input.

lexicon

Lexicon: Vocabulary lookup functions

mwe

Multi-Word Expression (MWE) processing.

ontology

Ontology module for bridging anaphora and sort compatibility checking.

parser

Recursive descent parser for natural language to first-order logic.

pragmatics

Post-parse pragmatic inference transformations.

proof_convert

Conversion from parser AST to proof engine representation.

registry

Symbol registry for consistent variable naming in FOL output.

runtime_lexicon

Runtime JSON-based lexicon loading (requires dynamic-lexicon feature).

scope

Scope stack for variable binding during code generation.

semantics

Semantic transformations for logical expressions.

session

Session Manager for Incremental Evaluation

style

ANSI terminal color styling for error messages.

suggest

Spelling suggestions for unknown words.

symbol_dict

Symbol Dictionary Extraction

token

Token types for the LOGOS lexer and parser.

transpile

Transpilation from AST to first-order logic notation.

view

Owned view types for AST serialization and display.

visitor

AST visitor pattern for traversing logical expressions.

Structs

Arena

A bump allocator for stable, arena-allocated references.

BaseSpan

A byte-offset range in source text.

CompileOptions

Interner

A string interner providing O(1) equality comparison via Symbol handles.

Symbol

A lightweight handle to an interned string.

TranspileContext

Enums

Case

Grammatical case (for pronouns).

Gender

Grammatical gender (for pronouns and agreement).

Number

Grammatical number for nouns and agreement.

OutputFormat

Traits

SymbolEq

Convenience trait for comparing a Symbol to a string literal.