Module compile 

Compilation API

This module provides the public entry points for natural language to first-order logic translation.

Compilation Functions

Function	Use Case
compile	Single sentence, Unicode output
compile_simple	Single sentence, ASCII output
compile_kripke	Modal logic with world quantification
compile_with_discourse	Multi-sentence with anaphora resolution
compile_forest	Ambiguous sentences, all readings
compile_all_scopes	All quantifier scope permutations
compile_discourse	Multi-sentence with temporal ordering
compile_theorem	Theorem proving with backward chaining

Example

use logicaffeine_language::{compile, compile_forest};

// Simple compilation
let fol = compile("John loves Mary.").unwrap();
assert!(fol.contains("Love"));

// Handle ambiguity
let readings = compile_forest("Every woman loves a man.");
assert!(readings.len() >= 1); // Surface and possibly inverse scope

Constants

MAX_FOREST_READINGS

Maximum number of readings in a parse forest. Prevents exponential blowup from ambiguous sentences.

Functions

compile

Compile natural language input to first-order logic with default options.

compile_all_scopes

Returns all possible scope readings for a sentence. For sentences with multiple quantifiers, this returns all permutations. Example: “Every woman loves a man” returns both:

compile_all_scopes_with_options

Returns all scope readings with specified output format.

compile_ambiguous

Compile with PP attachment ambiguity detection. Returns multiple readings if structural ambiguity exists.

compile_ambiguous_with_options

Compile with PP attachment ambiguity detection and specified options.

compile_discourse

Compile multiple sentences as a discourse, tracking temporal ordering.

compile_discourse_with_options

Compile multiple sentences as a discourse with specified options.

compile_forest

Compile natural language input, producing all valid parse readings. Handles lexical ambiguity (Noun/Verb) and structural ambiguity (PP attachment).

compile_forest_with_options

Compile natural language input with options, producing all valid parse readings.

compile_kripke

Compile with Kripke semantics lowering. Modal operators are transformed into explicit possible world quantification.

compile_simple

Compile with simple FOL format.

compile_theorem

Compile and prove a theorem block.

compile_with_discourse

Compile with shared WorldState AND Interner for proper cross-sentence discourse. Use this when you need pronouns to resolve across multiple sentences.

compile_with_options

Compile natural language input to first-order logic with specified options.

compile_with_world_state

Compile with shared WorldState for cross-sentence discourse.

compile_with_world_state_interner_options

Compile with full control over WorldState, Interner, and options.

compile_with_world_state_options

Compile with shared WorldState and options.