NL2FOL

Core class for converting natural language to first-order logic

Overview

The NL2FOL class is the primary interface for translating natural language sentences into first-order logic (FOL) expressions. It orchestrates the entire translation pipeline, from claim extraction to logical formula generation.

Class Definition

class NL2FOL:
    def __init__(self, sentence, model_type, pipeline, tokenizer, nli_model, nli_tokenizer, debug=False, direct=False)

Parameters

sentence · str · required

The natural language sentence to convert to first-order logic

model_type · str · required

Type of language model to use. Supported values: 'llama' or 'gpt'

pipeline · transformers.Pipeline

HuggingFace text generation pipeline (required for LLaMA models, None for GPT)

tokenizer · transformers.Tokenizer

Tokenizer for the generation model (required for LLaMA models, None for GPT)

nli_model · transformers.PreTrainedModel · required

Natural Language Inference model for entity relationship detection

nli_tokenizer · transformers.Tokenizer · required

Tokenizer for the NLI model

debug · bool · default: "False"

Enable debug output to print intermediate results

direct · bool · default: "False"

Use direct FOL conversion (experimental)

Instance Attributes

After initialization and conversion, the following attributes are populated:

claim · str

Extracted claim from the input sentence

implication · str

Extracted implication from the input sentence

claim_ref_exp · str

Referring expressions identified in the claim

implication_ref_exp · str

Referring expressions identified in the implication

equal_entities · list

List of tuples containing entities that are semantically equal

subset_entities · list

List of tuples where first entity is a subset of the second

entity_mappings · dict

Mapping from entity names to logical variables (a, b, c, …)

claim_properties · str

Properties extracted from the claim

implication_properties · str

Properties extracted from the implication

property_implications · list

List of tuples representing property-level implications

claim_lf · str

Logical form of the claim

implication_lf · str

Logical form of the implication

final_lf · str

Final first-order logic formula (claim → implication)

final_lf2 · str

Alternative final formula with different quantifier handling

Methods

convert_to_first_order_logic

def convert_to_first_order_logic()

Main method to execute the complete NL to FOL conversion pipeline.

Returns: tuple[str, str] - A tuple containing (final_lf, final_lf2)

Pipeline Steps:

1. Extract claim and implication
2. Get referring expressions
3. Determine entity relations
4. Create entity mappings
5. Extract properties
6. Generate logical forms
7. Apply heuristics
8. Generate final formulas

Example

from transformers import AutoModelForSequenceClassification, AutoTokenizer
import transformers

# Initialize models
tokenizer = AutoTokenizer.from_pretrained("meta-llama/Llama-2-7b-hf")
pipeline = transformers.pipeline(
    "text-generation",
    model="meta-llama/Llama-2-7b-hf",
    torch_dtype=torch.float16,
    device_map="auto"
)
nli_tokenizer = AutoTokenizer.from_pretrained("microsoft/deberta-v3-base")
nli_model = AutoModelForSequenceClassification.from_pretrained("microsoft/deberta-v3-base")

# Create NL2FOL instance
sentence = "All cats are mammals, therefore my pet is a mammal."
nl2fol = NL2FOL(
    sentence=sentence,
    model_type='llama',
    pipeline=pipeline,
    tokenizer=tokenizer,
    nli_model=nli_model,
    nli_tokenizer=nli_tokenizer,
    debug=True
)

# Convert to FOL
final_lf, final_lf2 = nl2fol.convert_to_first_order_logic()
print(f"Formula 1: {final_lf}")
print(f"Formula 2: {final_lf2}")

extract_claim_and_implication

def extract_claim_and_implication()

Extracts the claim and implication components from the input sentence using an LLM.

Side Effects: Populates self.claim and self.implication attributes

get_referring_expressions

def get_referring_expressions()

Identifies referring expressions (entities) in both claim and implication.

Side Effects: Populates self.claim_ref_exp and self.implication_ref_exp

get_entity_relations

def get_entity_relations()

Determines relationships between entities (equality, subset) across claim and implication.

Side Effects: Populates self.equal_entities and self.subset_entities

get_entity_mapping

def get_entity_mapping()

Creates a mapping from entity strings to logical variables (a, b, c, …).

Side Effects: Populates self.entity_mappings dictionary

get_properties

def get_properties()

Extracts properties associated with the referring expressions.

Side Effects: Populates self.claim_properties and self.implication_properties

get_properties_relations

def get_properties_relations()

Determines entailment relationships between properties using NLI.

Side Effects: Populates self.property_implications

check_entailment

def check_entailment(clause1, clause2)

Checks if clause1 entails clause2 using GPT-based prompting.

Parameters:

• clause1 (str): First clause
• clause2 (str): Second clause

Returns: bool - True if entailment exists, False otherwise

get_fol

def get_fol()

Generates first-order logic representations for claim and implication.

Side Effects: Populates self.claim_lf and self.implication_lf

get_direct_fol

def get_direct_fol()

Generates FOL directly from the sentence without intermediate steps (experimental).

apply_heuristics

def apply_heuristics()

Applies post-processing heuristics to normalize logical operators:

• Replaces -> with &
• Normalizes & to and
• Normalizes | to or

get_final_lf

def get_final_lf()

Generates the final logical formula with proper quantifiers based on entity relationships.

Side Effects: Populates self.final_lf

get_final_lf2

def get_final_lf2()

Generates an alternative final formula with existential quantifiers for all symbols.

Side Effects: Populates self.final_lf2

get_llm_result

def get_llm_result(prompt, model_type=None)

Internal method to get LLM responses based on configured model type.

Parameters:

• prompt (str): Input prompt for the LLM
• model_type (str, optional): Override default model type

Returns: str - LLM response text

get_nli_prob

def get_nli_prob(premise, hypothesis)

Calculates NLI entailment probability for a premise-hypothesis pair.

Parameters:

• premise (str): Premise text
• hypothesis (str): Hypothesis text

Returns: float - Probability of entailment (0-100)

get_nli_prob_list

def get_nli_prob_list(premise, hypothesis_list)

Calculates NLI probabilities for multiple hypotheses.

Parameters:

• premise (str): Premise text
• hypothesis_list (list[str]): List of hypothesis texts

Returns: list[float] - List of entailment probabilities

Utility Functions

setup_dataset

def setup_dataset(fallacy_set='logic', length=100)

Sets up evaluation datasets for fallacy detection.

Parameters:

• fallacy_set (str): Dataset type - 'logic', 'logicclimate', 'nli', or 'folio'
• length (int): Number of samples to load

Returns: pandas.DataFrame - Dataset with articles and label columns

The setup_dataset function is typically used in evaluation scripts to prepare test data for batch processing.

Example Usage

GPT-4 Backend

from nl_to_fol import NL2FOL
from transformers import AutoModelForSequenceClassification, AutoTokenizer

# Initialize NLI model
nli_tokenizer = AutoTokenizer.from_pretrained("microsoft/deberta-v3-base")
nli_model = AutoModelForSequenceClassification.from_pretrained("microsoft/deberta-v3-base")

# Create NL2FOL instance with GPT
sentence = "If all birds can fly, then penguins can fly."
nl2fol = NL2FOL(
    sentence=sentence,
    model_type='gpt',
    pipeline=None,
    tokenizer=None,
    nli_model=nli_model,
    nli_tokenizer=nli_tokenizer,
    debug=True
)

# Convert and access results
final_lf, final_lf2 = nl2fol.convert_to_first_order_logic()

print("Claim:", nl2fol.claim)
print("Implication:", nl2fol.implication)
print("Entity Mappings:", nl2fol.entity_mappings)
print("Final Formula:", final_lf)

import pandas as pd
from nl_to_fol import NL2FOL, setup_dataset

# Load dataset
df = setup_dataset(fallacy_set='logic', length=50)

results = []
for idx, row in df.iterrows():
    nl2fol = NL2FOL(
        row['articles'],
        model_type='gpt',
        pipeline=None,
        tokenizer=None,
        nli_model=nli_model,
        nli_tokenizer=nli_tokenizer,
        debug=False
    )
    lf1, lf2 = nl2fol.convert_to_first_order_logic()
    results.append({
        'sentence': row['articles'],
        'formula': lf1,
        'formula2': lf2
    })

results_df = pd.DataFrame(results)

See Also

• CVCGenerator - Generate SMT solver input from FOL formulas
• SMTResults - Interpret solver results
• Helper Functions - Utility functions for string processing