Skip to main content

​
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.
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.

​
Architecture

​
Stage 1: Claim and Implication Extraction

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

​
Implementation

# 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."
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

​
Example Transformations

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”
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”

​
Stage 2: Referring Expressions

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

​
Implementation

# 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:

Noun Phrases

“a tall man” “the new teacher” “all students”

Pronouns

“he”, “she”, “it” “they”, “them” “this”, “that”

Proper Names

“Harvard” “Michael Vick” “New York”

​
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

# 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

Equal Entities

Entities that refer to the same thingExamples:
  • “a tall man” ≈ “tall people”
  • “the teacher” ≈ “she”

Subset Relations

One entity is a subset of anotherExamples:
  • “Harvard students” ⊂ “students”
  • “New York drivers” ⊂ “drivers”
Entity relations are crucial for determining the correct quantifier scope in the final FOL formula.

​
Stage 4: Entity Mapping

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

​
Implementation

# 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

# 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

Properties that describe a single entity:
Input: "A tall man loves cheese"
Properties: IsTall(a), LovesCheese(a)
These become unary predicates in FOL.
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.
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)

​
Consistency Checking

The system ensures predicate arities are consistent using fix_inconsistent_arities(): 
# 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
If the same predicate appears with different numbers of arguments, the system uses the minimum arity to maintain consistency.

​
Stage 6: FOL Generation

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

​
Implementation

# 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

# 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')
The system applies heuristics to normalize logical operators, replacing implications in claims with conjunctions and converting symbols to words.

​
Stage 7: Quantifier Application

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

​
Implementation

# 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

Claims (Premises)

Typically use existential quantifiers (exists)Represents specific observations:
exists x (IsTall(x) and LovesCheese(x))

Implications (Conclusions)

Typically use universal quantifiers (forall)Represents general claims:
forall y (IsTall(y) -> LovesCheese(y))

​
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))
This formula reads: “If there exists a tall person who loves cheese, then all tall people love cheese” - which is clearly fallacious!

​
Complete Pipeline Example

Let’s trace a complete example through all stages:
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))

​
Model Selection

The pipeline supports multiple LLM backends: 
# 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
The system can use:
  • GPT-4: For higher accuracy and better reasoning
  • Llama models: For local deployment and cost efficiency

​
Next Steps

First-Order Logic

Learn the formal logic notation used in the pipeline

SMT Solving

Understand how the final FOL is verified

API Reference

Use the NL2FOL class in your code

Quick Start

Try the pipeline yourself

Build docs developers (and LLMs) love

Get started for freeTalk to us