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

# Natural Language to First-Order Logic

> Learn how to translate natural language arguments to first-order logic formulas

## Overview

The `nl_to_fol.py` script converts natural language arguments into first-order logic (FOL) formulas. This is the first and most critical step in the NL2FOL pipeline for detecting logical fallacies.

## How It Works

The translation process follows a multi-stage pipeline:

<Steps>
  <Step title="Claim and Implication Extraction">
    The system identifies the claim and implication components of the argument using LLM prompts.
  </Step>

  <Step title="Referring Expression Identification">
    Extracts referring expressions (entities) from both the claim and implication.
  </Step>

  <Step title="Entity Relationship Detection">
    Determines relationships between entities (equal, subset, or unrelated) using NLI models or LLM reasoning.
  </Step>

  <Step title="Entity Mapping">
    Maps entities to logical variables (a, b, c, etc.) for formal representation.
  </Step>

  <Step title="Property Extraction">
    Identifies properties and predicates associated with each entity.
  </Step>

  <Step title="FOL Formula Generation">
    Generates first-order logic formulas for claim and implication with proper quantifiers.
  </Step>

  <Step title="Final Formula Assembly">
    Combines claim and implication into a final formula of the form: (Claim) → (Implication)
  </Step>
</Steps>

## Command Usage

### Basic Command

```bash theme={null}
python3 src/nl_to_fol.py \
  --model_name <your_model_name> \
  --nli_model_name <your_nli_model_name> \
  --run_name <run_name> \
  --dataset <logic or logicclimate> \
  --length <number_of_datapoints>
```

### Parameters

<ParamField path="model_name" type="string" required>
  The LLM model to use for translation. Supports:

  * HuggingFace model paths (e.g., `meta-llama/Llama-2-7b-hf`)
  * OpenAI models (e.g., `gpt-4o`) - prefix with 'gpt' to use GPT mode
</ParamField>

<ParamField path="nli_model_name" type="string">
  The Natural Language Inference model for entity relationship detection.
  Example: `microsoft/deberta-v2-xlarge-mnli`
</ParamField>

<ParamField path="run_name" type="string" required>
  Name for this run. Output will be saved to `results/<run_name>.csv`
</ParamField>

<ParamField path="dataset" type="string" required>
  Dataset to use for testing. Options:

  * `logic` - Standard logical fallacy dataset
  * `logicclimate` - Climate-specific logical fallacy dataset
  * `folio` - FOLIO dataset for evaluation
  * `nli` - NLI-based dataset
</ParamField>

<ParamField path="length" type="integer" required>
  Number of datapoints to sample from the dataset for processing.
</ParamField>

## Example Usage

<CodeGroup>
  ```bash LLaMA Model theme={null}
  python3 src/nl_to_fol.py \
    --model_name meta-llama/Llama-2-13b-hf \
    --nli_model_name microsoft/deberta-v2-xlarge-mnli \
    --run_name llama_experiment_1 \
    --dataset logic \
    --length 100
  ```

  ```bash GPT-4 Model theme={null}
  python3 src/nl_to_fol.py \
    --model_name gpt-4o \
    --nli_model_name microsoft/deberta-v2-xlarge-mnli \
    --run_name gpt4_experiment_1 \
    --dataset logicclimate \
    --length 50
  ```
</CodeGroup>

## Output Format

The script generates a CSV file in `results/<run_name>.csv` with the following columns:

| Column                                | Description                                                 |
| ------------------------------------- | ----------------------------------------------------------- |
| `articles`                            | Original natural language text                              |
| `label`                               | Ground truth label (0=fallacy, 1=valid)                     |
| `Claim`                               | Extracted claim statement                                   |
| `Implication`                         | Extracted implication statement                             |
| `Referring Expressions - Claim`       | Entities in the claim                                       |
| `Referring Expressions - Implication` | Entities in the implication                                 |
| `Property Implications`               | Relationships between properties                            |
| `Equal Entities`                      | Entities determined to be equal                             |
| `Subset Entities`                     | Subset relationships between entities                       |
| `Claim Lfs`                           | Logical form of the claim                                   |
| `Implication Lfs`                     | Logical form of the implication                             |
| `Logical Form`                        | Final FOL formula (version 1)                               |
| `Logical Form 2`                      | Final FOL formula (version 2, with existential quantifiers) |

## Implementation Details

### NL2FOL Class

The core translation logic is implemented in the `NL2FOL` class:

```python theme={null}
nl2fol = NL2FOL(
    sentence=text,
    model_type='gpt',  # or 'llama'
    pipeline=pipeline,
    tokenizer=tokenizer,
    nli_model=nli_model,
    nli_tokenizer=nli_tokenizer,
    debug=True
)

final_lf1, final_lf2 = nl2fol.convert_to_first_order_logic()
```

### Debug Mode

The script runs with `debug=True` by default, printing intermediate results:

* Extracted claim and implication
* Referring expressions
* Entity relationships
* Property assignments
* Intermediate logical forms

<Note>
  Processing time varies based on:

  * Model size and type (LLaMA models require GPU)
  * Dataset length
  * Complexity of arguments

  Expect \~30-60 seconds per datapoint for LLM-based processing.
</Note>

## GPU Requirements

<Warning>
  LLaMA models require GPU acceleration. The script automatically detects CUDA availability and displays GPU information at startup.

  Minimum recommended: 16GB GPU memory for 7B models, 24GB+ for 13B models.
</Warning>

## Quantifier Strategies

The system generates two versions of the logical form:

**Logical Form 1**: Uses heuristics for quantifier assignment based on entity relationships

* Subset entities: subset gets `exists`, superset gets `forall`
* Property implications: universally quantified

**Logical Form 2**: More conservative approach

* All entity variables get existential quantifiers
* Property implications remain universally quantified

<Tip>
  Logical Form 2 is typically used for SMT solving as it provides better satisfiability checking results.
</Tip>

## Prompt Engineering

The system uses specialized prompts located in `prompts/`:

* `prompt_nl_to_ci.txt` - Claim/implication extraction
* `prompt_referring_expressions.txt` - Entity identification
* `prompt_entity_relation.txt` - Entity relationship detection
* `prompt_properties.txt` - Property extraction
* `prompt_fol.txt` - FOL formula generation

## Troubleshooting

### Common Issues

**CUDA Out of Memory**

* Reduce model size or batch processing
* Use model quantization or CPU offloading

**Empty Results**

* Check that prompts directory exists in working directory
* Verify model has necessary permissions and access

**NLI Model Errors**

* Ensure NLI model is compatible (sequence classification models)
* Check tokenizer compatibility

## Next Steps

After generating FOL formulas:

1. Convert to SMT format using `fol_to_cvc.py`
2. Run SMT solver for satisfiability checking
3. Interpret results and evaluate performance

See [FOL to SMT Conversion](/usage/fol-to-smt) for the next step in the pipeline.