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

# Quick Start

> Run your first logical fallacy detection using NL2FOL

## Overview

This guide walks you through running the complete NL2FOL pipeline: from translating natural language to first-order logic, converting to SMT format, and evaluating results.

## Basic Workflow

<Steps>
  <Step title="Convert Natural Language to First-Order Logic">
    Use `nl_to_fol.py` to process a dataset and generate logical formulas
  </Step>

  <Step title="Convert FOL to SMT and Run Solver">
    Use `fol_to_cvc.py` to convert formulas to SMT format and verify them
  </Step>

  <Step title="Evaluate Results">
    Use `get_metrics.py` to calculate accuracy, precision, recall, and F1 score
  </Step>
</Steps>

## Step 1: Natural Language to FOL

The main entry point is `nl_to_fol.py`, which processes datasets and generates first-order logic formulas.

### Command Syntax

```bash theme={null}
python3 src/nl_to_fol.py \
  --model_name <model_name> \
  --nli_model_name <nli_model_name> \
  --run_name <run_name> \
  --dataset <logic|logicclimate|nli|folio> \
  --length <number_of_samples>
```

### Example: Using GPT-4

```bash theme={null}
python3 src/nl_to_fol.py \
  --model_name gpt-4o \
  --nli_model_name roberta-large-mnli \
  --run_name my_first_run \
  --dataset logic \
  --length 10
```

<Note>
  GPT models (starting with "gpt-") use the OpenAI API. Ensure your OPENAI\_API\_KEY environment variable is set.
</Note>

### Example: Using Llama

```bash theme={null}
python3 src/nl_to_fol.py \
  --model_name meta-llama/Llama-2-7b-hf \
  --nli_model_name roberta-large-mnli \
  --run_name llama_run \
  --dataset logic \
  --length 10
```

### Available Datasets

<CodeGroup>
  ```bash Logic Dataset theme={null}
  # General logical fallacies (3,227 examples)
  python3 src/nl_to_fol.py \
    --model_name gpt-4o \
    --nli_model_name roberta-large-mnli \
    --run_name logic_test \
    --dataset logic \
    --length 50
  ```

  ```bash Climate Dataset theme={null}
  # Climate-related fallacies (1,415 examples)
  python3 src/nl_to_fol.py \
    --model_name gpt-4o \
    --nli_model_name roberta-large-mnli \
    --run_name climate_test \
    --dataset logicclimate \
    --length 50
  ```

  ```bash NLI Dataset theme={null}
  # Natural Language Inference examples (170K+)
  python3 src/nl_to_fol.py \
    --model_name gpt-4o \
    --nli_model_name roberta-large-mnli \
    --run_name nli_test \
    --dataset nli \
    --length 100
  ```

  ```bash FOLIO Dataset theme={null}
  # Formal logic inference
  python3 src/nl_to_fol.py \
    --model_name gpt-4o \
    --nli_model_name roberta-large-mnli \
    --run_name folio_test \
    --dataset folio \
    --length 20
  ```
</CodeGroup>

### Output

This generates a CSV file at `results/<run_name>.csv` with columns:

* **articles**: Original natural language text
* **Claim**: Extracted claim from the sentence
* **Implication**: Extracted implication
* **Referring Expressions - Claim/Implication**: Entity references
* **Property Implications**: Property relationships
* **Equal Entities**: Entities identified as equal
* **Subset Entities**: Subset relationships between entities
* **Claim Lfs**: Logical form for claim
* **Implication Lfs**: Logical form for implication
* **Logical Form**: Final combined formula (version 1)
* **Logical Form 2**: Final combined formula (version 2)
* **label**: Ground truth (0=fallacy, 1=valid)

## Step 2: FOL to SMT Verification

Convert the generated logical formulas to SMT format and verify them using CVC4/CVC5.

### Command Syntax

```bash theme={null}
python3 src/fol_to_cvc.py <run_name>
```

### Example

```bash theme={null}
python3 src/fol_to_cvc.py my_first_run
```

This will:

1. Read the FOL formulas from `results/my_first_run.csv`
2. Generate SMT-LIB files in `results/my_first_run_smt/`
3. Run CVC4 on each formula
4. Save results to `results/my_first_run_results.csv`

### SMT Results

The solver produces one of three results:

<CardGroup cols={3}>
  <Card title="Valid" icon="check">
    Formula is unsatisfiable (negation fails) - the argument is logically valid
  </Card>

  <Card title="LF" icon="x">
    Formula is satisfiable or unknown - the argument contains a logical fallacy
  </Card>

  <Card title="Empty" icon="question">
    Processing error occurred
  </Card>
</CardGroup>

<Note>
  The code uses "Logical Form 2" by default, which applies different quantifier scoping heuristics than "Logical Form".
</Note>

## Step 3: Evaluate Results

Calculate performance metrics on the results.

### Command Syntax

```bash theme={null}
python3 eval/get_metrics.py <results_csv_path>
```

### Example

```bash theme={null}
python3 eval/get_metrics.py results/my_first_run_results.csv
```

### Output Metrics

The script outputs:

```
(accuracy, precision, recall, f1_score)
```

Example output:

```python theme={null}
(0.85, 0.82, 0.88, 0.85)
```

This represents:

* **Accuracy**: 85% of predictions are correct
* **Precision**: 82% of predicted fallacies are actual fallacies
* **Recall**: 88% of actual fallacies are detected
* **F1 Score**: 85% harmonic mean of precision and recall

## Complete Example

Here's a complete end-to-end example:

```bash theme={null}
# Step 1: Generate FOL formulas from 20 examples
python3 src/nl_to_fol.py \
  --model_name gpt-4o \
  --nli_model_name roberta-large-mnli \
  --run_name quickstart_demo \
  --dataset logic \
  --length 20

# Step 2: Convert to SMT and verify
python3 src/fol_to_cvc.py quickstart_demo

# Step 3: Evaluate results
python3 eval/get_metrics.py results/quickstart_demo_results.csv
```

<Warning>
  Processing can take several minutes per example due to multiple LLM calls. Start with small dataset sizes (10-20 examples) for testing.
</Warning>

## Understanding the NL2FOL Class

The core logic is implemented in the `NL2FOL` class from `src/nl_to_fol.py:15`. Here's how it works:

### Initialization

```python theme={null}
from nl_to_fol import NL2FOL

nl2fol = NL2FOL(
    sentence="All birds can fly. Penguins are birds. Therefore, penguins can fly.",
    model_type='gpt',
    pipeline=None,
    tokenizer=None,
    nli_model=nli_model,
    nli_tokenizer=nli_tokenizer,
    debug=True
)
```

### Conversion Pipeline

The `convert_to_first_order_logic()` method executes these steps:

<Steps>
  <Step title="Extract Claim and Implication">
    Separates the premise (claim) from the conclusion (implication)

    ```python theme={null}
    nl2fol.extract_claim_and_implication()
    # claim: "All birds can fly. Penguins are birds."
    # implication: "Penguins can fly."
    ```
  </Step>

  <Step title="Get Referring Expressions">
    Identifies entities mentioned in the text

    ```python theme={null}
    nl2fol.get_referring_expressions()
    # claim_ref_exp: "birds, penguins"
    ```
  </Step>

  <Step title="Determine Entity Relations">
    Uses NLI to find relationships between entities

    ```python theme={null}
    nl2fol.get_entity_relations()
    # subset_entities: [("penguins", "birds")]
    ```
  </Step>

  <Step title="Map Entities to Variables">
    Creates logical variable mappings

    ```python theme={null}
    nl2fol.get_entity_mapping()
    # entity_mappings: {"birds": "a", "penguins": "b"}
    ```
  </Step>

  <Step title="Extract Properties">
    Identifies predicates and properties

    ```python theme={null}
    nl2fol.get_properties()
    # claim_properties: "canFly(a)"
    ```
  </Step>

  <Step title="Generate Logical Forms">
    Creates FOL formulas for claim and implication

    ```python theme={null}
    nl2fol.get_fol()
    # claim_lf: "canFly(a) and isPenguin(b)"
    # implication_lf: "canFly(b)"
    ```
  </Step>

  <Step title="Combine into Final Formula">
    Applies quantifiers and creates the final implication

    ```python theme={null}
    nl2fol.get_final_lf()
    # final_lf: "(exists a (canFly(a))) -> (forall b (canFly(b)))"
    ```
  </Step>
</Steps>

## Advanced Usage

### Custom Sentence Processing

You can process individual sentences programmatically:

```python theme={null}
import torch
from transformers import AutoModelForSequenceClassification, AutoTokenizer
from nl_to_fol import NL2FOL
from openai import OpenAI

# Initialize NLI model
nli_tokenizer = AutoTokenizer.from_pretrained("roberta-large-mnli")
nli_model = AutoModelForSequenceClassification.from_pretrained("roberta-large-mnli")

# Process a sentence
sentence = "All politicians are corrupt. John is a politician. Therefore, John is corrupt."

nl2fol = NL2FOL(
    sentence=sentence,
    model_type='gpt',
    pipeline=None,
    tokenizer=None,
    nli_model=nli_model,
    nli_tokenizer=nli_tokenizer,
    debug=True
)

final_lf, final_lf2 = nl2fol.convert_to_first_order_logic()
print(f"Logical Form: {final_lf}")
```

### Interpreting SMT Results

To understand why a formula was classified a certain way:

```bash theme={null}
python3 src/interpret_smt_results.py \
  results/my_run_smt/5_out.txt \
  results/my_run.csv
```

This provides detailed explanations of the SMT solver's reasoning.

## Troubleshooting

<AccordionGroup>
  <Accordion title="Rate limits with OpenAI API">
    Add delays between requests or reduce dataset size:

    ```bash theme={null}
    --length 5
    ```
  </Accordion>

  <Accordion title="GPU memory issues">
    Use smaller models or CPU inference:

    ```bash theme={null}
    export CUDA_VISIBLE_DEVICES=""
    ```
  </Accordion>

  <Accordion title="CVC4 timeouts">
    The code automatically enables finite model finding for "unknown" results. If still timing out, the formula may be too complex.
  </Accordion>

  <Accordion title="Empty results column">
    Check that:

    * CVC4/CVC5 binary exists and is executable
    * SMT files were generated in results/`<run_name>`\_smt/
    * FOL formulas are well-formed in the CSV
  </Accordion>
</AccordionGroup>

## Next Steps

<CardGroup cols={2}>
  <Card title="API Reference" icon="code" href="/api/nl2fol">
    Explore detailed API documentation
  </Card>

  <Card title="Examples" icon="lightbulb" href="/examples/basic-usage">
    View more complex usage examples
  </Card>
</CardGroup>