> ## Documentation Index
> Fetch the complete documentation index at: https://mintlify.com/lovishchopra/NL2FOL/llms.txt
> Use this file to discover all available pages before exploring further.

# Translation Pipeline

> Multi-stage pipeline for converting natural language to first-order logic

## Pipeline Overview

The NL2FOL system uses a sophisticated multi-stage pipeline to convert natural language statements into first-order logic formulas. Each stage progressively refines the representation, ultimately producing a formal logical formula that can be verified by SMT solvers.

<Info>
  The pipeline is implemented in the `NL2FOL` class (`src/nl_to_fol.py:15-388`) and orchestrates multiple LLM calls with specialized prompts to extract logical structure from text.
</Info>

## Architecture

```mermaid theme={null}
graph TD
    A[Natural Language Input] --> B[Stage 1: Claim & Implication Extraction]
    B --> C[Stage 2: Referring Expressions]
    C --> D[Stage 3: Entity Relations]
    D --> E[Stage 4: Entity Mapping]
    E --> F[Stage 5: Property Extraction]
    F --> G[Stage 6: FOL Generation]
    G --> H[Stage 7: Quantifier Application]
    H --> I[Final FOL Formula]
    I --> J[SMT Verification]
```

## Stage 1: Claim and Implication Extraction

The first stage separates the argument into its premise (claim) and conclusion (implication).

### Implementation

```python theme={null}
# From src/nl_to_fol.py:71-83
def extract_claim_and_implication(self):
    with open("prompts/prompt_nl_to_ci.txt", encoding="ascii", errors="ignore") as f:
        prompt = f.read() + self.sentence
    result = self.get_llm_result(prompt)
    
    for line in result.split("\n"):
        if 'Claim' in line:
            self.claim = line[line.find(':') + 1:]
        if 'Implication' in line:
            self.implication = line[line.find(':') + 1:]
```

### Prompt Template

The system uses few-shot learning with examples:

```
Input: "I met a tall man who loved to eat cheese, now I believe all tall people like cheese"

Output:
Claim: "A tall man loves cheese."
Implication: "All tall people like cheese."
```

<Note>
  The prompt instructs the LLM to:

  * Identify multiple claims if present, but only one implication
  * Remove subordinating conjunctions from implications
  * Replace pronouns with appropriate nouns for clarity
</Note>

### Example Transformations

<Accordion title="Example 1: Simple Generalization">
  **Input**: "The two courses I took at UF were not very interesting. I don't think it's a good university."

  **Extracted**:

  * Claim: "Two courses at UF were not very interesting"
  * Implication: "UF is not a good university"
</Accordion>

<Accordion title="Example 2: Authority Fallacy">
  **Input**: "What can our new math teacher know? Have you seen how fat she is?"

  **Extracted**:

  * Claim: "The new math teacher is fat"
  * Implication: "The new math teacher doesn't know anything"
</Accordion>

## Stage 2: Referring Expressions

This stage identifies all noun phrases, pronouns, and proper names that refer to entities in the argument.

### Implementation

```python theme={null}
# From src/nl_to_fol.py:85-103
def get_referring_expressions(self):
    with open("prompts/prompt_referring_expressions.txt", encoding="ascii", errors="ignore") as f:
        prompt = f.read()

    result_claim = self.get_llm_result(prompt + self.claim)
    for line in result_claim.split("\n"):
        if "Referring expressions" in line:
            self.claim_ref_exp = line[line.find(':') + 1:]
            break

    result_implication = self.get_llm_result(prompt + self.implication)
    for line in result_implication.split("\n"):
        if "Referring expressions" in line:
            self.implication_ref_exp = line[line.find(':') + 1:]
            break
```

### What are Referring Expressions?

Referring expressions are linguistic elements that reference entities:

<CardGroup cols={3}>
  <Card title="Noun Phrases" icon="text">
    "a tall man"
    "the new teacher"
    "all students"
  </Card>

  <Card title="Pronouns" icon="user">
    "he", "she", "it"
    "they", "them"
    "this", "that"
  </Card>

  <Card title="Proper Names" icon="signature">
    "Harvard"
    "Michael Vick"
    "New York"
  </Card>
</CardGroup>

### Examples

```
Input: "A tall man loved cheese"
Referring expressions: A tall man, cheese

Input: "The new math teacher is fat"
Referring expressions: The new math teacher

Input: "Giving 10% of your income to the Church will free a child's soul"
Referring expressions: Your income, church, child's soul, limbo, heaven
```

## Stage 3: Entity Relations

This stage determines relationships between entities mentioned in the claim and implication.

### Implementation

```python theme={null}
# From src/nl_to_fol.py:219-258
def get_entity_relations(self):
    claim_res = self.claim_ref_exp.split(",")
    implication_res = self.implication_ref_exp.split(",")
    
    for c_re in claim_res:
        for i_re in implication_res:
            if c_re.strip().lower() == i_re.strip().lower():
                self.equal_entities.append((c_re, i_re))
                continue
            
            # Use LLM to determine relationship
            with open("prompts/prompt_entity_relation.txt", encoding="ascii", errors="ignore") as f:
                prompt = f.read().format(c_re, i_re)
            result = self.get_llm_result(prompt)
            relationship = int(result)
            
            if relationship == 1:
                self.equal_entities.append((c_re, i_re))
            elif relationship == 2:
                self.subset_entities.append((c_re, i_re))
            elif relationship == 3:
                self.equal_entities.append((i_re, c_re))
```

### Relationship Types

<CardGroup cols={2}>
  <Card title="Equal Entities" icon="equals">
    Entities that refer to the same thing

    Examples:

    * "a tall man" ≈ "tall people"
    * "the teacher" ≈ "she"
  </Card>

  <Card title="Subset Relations" icon="circle-dot">
    One entity is a subset of another

    Examples:

    * "Harvard students" ⊂ "students"
    * "New York drivers" ⊂ "drivers"
  </Card>
</CardGroup>

<Tip>
  Entity relations are crucial for determining the correct quantifier scope in the final FOL formula.
</Tip>

## Stage 4: Entity Mapping

This stage assigns logical variables (a, b, c, ...) to entities.

### Implementation

```python theme={null}
# From src/nl_to_fol.py:260-280
def get_entity_mapping(self):
    current_char = 'a'
    
    # Map equal entities to the same variable
    for (s1, s2) in self.equal_entities:
        if s1 in self.entity_mappings:
            self.entity_mappings[s2] = self.entity_mappings[s1]
        elif s2 in self.entity_mappings:
            self.entity_mappings[s1] = self.entity_mappings[s2]
        else:
            self.entity_mappings[s1] = current_char
            self.entity_mappings[s2] = current_char
            current_char = chr(ord(current_char) + 1)
    
    # Map remaining entities
    for s in self.claim_ref_exp.split(','):
        if s not in self.entity_mappings:
            self.entity_mappings[s] = current_char
            current_char = chr(ord(current_char) + 1)
```

### Mapping Strategy

1. **Equal entities get the same variable** - preserves semantic equivalence
2. **Distinct entities get different variables** - maintains logical independence
3. **Variables assigned alphabetically** - starting from 'a'

**Example**:

```
Claim: "a tall man" → x
Implication: "tall people" → x (same entity, same variable)

Claim: "cheese" → y (different entity, different variable)
```

## Stage 5: Property Extraction

This stage extracts predicates that describe properties of entities and relationships between them.

### Implementation

```python theme={null}
# From src/nl_to_fol.py:105-131
def get_properties(self):
    with open("prompts/prompt_properties.txt", encoding="ascii", errors="ignore") as f:
        prompt = f.read()
    
    prompt_template = "Input {} " \
        "Referring Expressions: {} " \
        "Properties: ".format(self.claim, label_values(self.claim_ref_exp, self.entity_mappings))
    prompt1 = prompt + prompt_template
    self.claim_properties = first_non_empty_line(self.get_llm_result(prompt1))
    
    # Similar for implication properties...
    self.claim_properties, self.implication_properties = fix_inconsistent_arities(
        split_string_except_in_brackets(self.claim_properties, ','),
        split_string_except_in_brackets(self.implication_properties, ',')
    )
```

### Property Types

<Accordion title="Unary Properties (Single Argument)">
  Properties that describe a single entity:

  ```
  Input: "A tall man loves cheese"
  Properties: IsTall(a), LovesCheese(a)
  ```

  These become unary predicates in FOL.
</Accordion>

<Accordion title="Binary Relations (Two Arguments)">
  Properties that describe relationships between two entities:

  ```
  Input: "A man is touching another person"
  Properties: IsBald(a), IsTouching(a, b)
  ```

  These become binary predicates in FOL.
</Accordion>

<Accordion title="Complex Properties">
  Properties that may involve multiple predicates:

  ```
  Input: "Giving 10% of your income to the Church will free a child's soul"
  Properties: IsGiven(a,b), IsInLimbo(c), IsInHeaven(c)
  ```
</Accordion>

### Consistency Checking

The system ensures predicate arities are consistent using `fix_inconsistent_arities()`:

```python theme={null}
# From src/helpers.py:61-104
def fix_inconsistent_arities(clauses1, clauses2):
    predicates = {}
    
    # Extract predicates and their arities
    for clause in all_clauses:
        predicate = clause.split('(')[0]
        arity = len(clause.split(','))
        
        if predicate in predicates:
            if predicates[predicate] != arity:
                predicates[predicate] = min(predicates[predicate], arity)
        else:
            predicates[predicate] = arity
```

<Note>
  If the same predicate appears with different numbers of arguments, the system uses the minimum arity to maintain consistency.
</Note>

## Stage 6: FOL Generation

This stage converts properties into first-order logic formulas using logical connectives.

### Implementation

```python theme={null}
# From src/nl_to_fol.py:170-192
def get_fol(self):
    with open("prompts/prompt_fol.txt", encoding="ascii", errors="ignore") as f:
        prompt = f.read()
    
    prompt_template = " Input {} " \
        "Referring Expressions: {} " \
        "Properties: {} " \
        "Logical Form:".format(self.claim, label_values(self.claim_ref_exp, self.entity_mappings), 
                               self.claim_properties)
    prompt1 = prompt + prompt_template
    self.claim_lf = first_non_empty_line(self.get_llm_result(prompt1))
    
    # Similar for implication...
    self.claim_lf = remove_text_after_last_parenthesis(self.claim_lf)
    self.implication_lf = remove_text_after_last_parenthesis(self.implication_lf)
```

### Prompt Examples

The prompt teaches the LLM to combine properties with logical operators:

```
Example 1:
Input: "A tall man loves cheese"
Properties: IsTall(x), LovesCheese(x)
Logical Form: IsTall(x) & LovesCheese(x)

Example 2:
Input: "Smacking children stops bad behavior"
Properties: IsSmacked(x), HasBadBehavior(x)
Logical Form: IsSmacked(x) -> ~HasBadBehavior(x)
```

### Heuristics Applied

```python theme={null}
# From src/nl_to_fol.py:378-387
def apply_heuristics(self):
    self.claim_lf = self.claim_lf.replace('->','&')
    self.claim_lf = self.claim_lf.replace('&','and')
    self.claim_lf = self.claim_lf.replace('|','or')
    
    self.implication_lf = self.implication_lf.replace('->','&')
    self.implication_lf = self.implication_lf.replace('&','and')
    self.implication_lf = self.implication_lf.replace('|','or')
```

<Info>
  The system applies heuristics to normalize logical operators, replacing implications in claims with conjunctions and converting symbols to words.
</Info>

## Stage 7: Quantifier Application

The final stage adds quantifiers (exists/forall) based on entity relationships and constructs the complete FOL formula.

### Implementation

```python theme={null}
# From src/nl_to_fol.py:282-320
def get_final_lf(self):
    claim_symbols = extract_propositional_symbols(self.claim_lf)
    implication_symbols = extract_propositional_symbols(self.implication_lf)
    claim_lf = self.claim_lf
    implication_lf = self.implication_lf
    
    # Handle subset relationships
    for (subset, superset) in self.subset_entities:
        if map[subset] in claim_symbols and map[superset] in implication_symbols:
            if claim_lf.find("exists {} ".format(map[subset])) == -1:
                claim_lf = "exists {} ({})".format(map[subset], claim_lf)
            if implication_lf.find("forall {}".format(map[superset])) == -1:
                implication_lf = "forall {} ({})".format(map[superset], implication_lf)
    
    # Add property implications
    for (prop1, prop2) in self.property_implications:
        lf = "{} -> {}".format(prop1, prop2)
        lf_symbols = extract_propositional_symbols(lf)
        for symbol in lf_symbols:
            lf = "forall {} ".format(symbol) + '(' + lf + ')'
        claim_lf = claim_lf + " & (" + lf + ")"
    
    self.final_lf = "({}) -> ({})".format(claim_lf, implication_lf)
```

### Quantifier Rules

<CardGroup cols={2}>
  <Card title="Claims (Premises)" icon="circle-dot">
    Typically use **existential quantifiers** (exists)

    Represents specific observations:

    ```
    exists x (IsTall(x) and LovesCheese(x))
    ```
  </Card>

  <Card title="Implications (Conclusions)" icon="globe">
    Typically use **universal quantifiers** (forall)

    Represents general claims:

    ```
    forall y (IsTall(y) -> LovesCheese(y))
    ```
  </Card>
</CardGroup>

### Final Formula Structure

The complete formula follows the pattern:

```
(claim_with_quantifiers) -> (implication_with_quantifiers)
```

**Complete Example**:

```
Input: "I met a tall man who loved to eat cheese, now I believe all tall people like cheese"

Final FOL:
exists x (IsTall(x) and LovesCheese(x)) -> forall y (IsTall(y) -> LovesCheese(y))
```

<Tip>
  This formula reads: "If there exists a tall person who loves cheese, then all tall people love cheese" - which is clearly fallacious!
</Tip>

## Complete Pipeline Example

Let's trace a complete example through all stages:

<Accordion title="Full Pipeline Walkthrough">
  **Input**: "The two courses I took at UF were not very interesting. I don't think it's a good university."

  **Stage 1 - Claim & Implication**:

  * Claim: "Two courses at UF were not very interesting"
  * Implication: "UF is not a good university"

  **Stage 2 - Referring Expressions**:

  * Claim: "courses at UF"
  * Implication: "UF"

  **Stage 3 - Entity Relations**:

  * Subset: "courses at UF" ⊂ "UF courses"

  **Stage 4 - Entity Mapping**:

  * "courses at UF" → x
  * "UF" → y

  **Stage 5 - Properties**:

  * Claim: IsUFCourse(x), NotInteresting(x)
  * Implication: IsUF(y), NotGood(y)

  **Stage 6 - FOL Generation**:

  * Claim FOL: IsUFCourse(x) and NotInteresting(x)
  * Implication FOL: IsUF(y) and NotGood(y)

  **Stage 7 - Quantifiers**:

  * Final: `exists x (IsUFCourse(x) and NotInteresting(x)) -> forall y (IsUF(y) -> NotGood(y))`
</Accordion>

## Model Selection

The pipeline supports multiple LLM backends:

```python theme={null}
# From src/nl_to_fol.py:49-67
def get_llm_result(self, prompt, model_type=None):
    if model_type == None:
        model_type = self.model_type
    
    if model_type == 'llama':
        sequences = self.pipeline(prompt,
            do_sample=False,
            num_return_sequences=1,
            eos_token_id=self.tokenizer.eos_token_id
        )
        return sequences[0]["generated_text"].removeprefix(prompt)
    
    elif model_type == 'gpt':
        completion = client.chat.completions.create(
            model="gpt-4o",
            messages=[{"role": "user", "content": prompt}]
        )
        return completion.choices[0].message.content
```

<Note>
  The system can use:

  * **GPT-4**: For higher accuracy and better reasoning
  * **Llama models**: For local deployment and cost efficiency
</Note>

## Next Steps

<CardGroup cols={2}>
  <Card title="First-Order Logic" icon="function" href="/concepts/first-order-logic">
    Learn the formal logic notation used in the pipeline
  </Card>

  <Card title="SMT Solving" icon="gear" href="/concepts/smt-solving">
    Understand how the final FOL is verified
  </Card>

  <Card title="API Reference" icon="code" href="/api/nl2fol">
    Use the NL2FOL class in your code
  </Card>

  <Card title="Quick Start" icon="rocket" href="/quickstart">
    Try the pipeline yourself
  </Card>
</CardGroup>