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

# Introduction

> NL2FOL translates natural language to first-order logic for detecting logical fallacies using LLMs and SMT solvers

## Overview

NL2FOL is an AI/ML research project that automatically translates natural language arguments into first-order logic (FOL) formulas to detect logical fallacies. The system leverages Large Language Models (LLMs) combined with Satisfiability Modulo Theories (SMT) solvers to formally verify the validity of logical arguments.

## How It Works

The NL2FOL pipeline consists of three main stages:

<Steps>
  <Step title="Natural Language to First-Order Logic">
    The system uses LLMs to extract claims, implications, referring expressions, and properties from natural language sentences, then converts them into formal first-order logic formulas.
  </Step>

  <Step title="FOL to SMT Conversion">
    First-order logic formulas are converted into SMT-LIB format and processed using CVC4/CVC5 solvers to check satisfiability.
  </Step>

  <Step title="Result Interpretation">
    The SMT solver results are interpreted to classify arguments as logically valid or fallacious based on whether the negated formula is unsatisfiable.
  </Step>
</Steps>

## Key Features

<CardGroup cols={2}>
  <Card title="Multi-LLM Support" icon="brain">
    Works with both open-source models (Llama) and commercial APIs (GPT-4)
  </Card>

  <Card title="Entity Grounding" icon="link">
    Identifies relationships between entities using Natural Language Inference (NLI) models
  </Card>

  <Card title="Property Extraction" icon="tags">
    Automatically extracts properties and their implications from natural language
  </Card>

  <Card title="Formal Verification" icon="check-circle">
    Uses SMT solvers for rigorous logical validation
  </Card>
</CardGroup>

## Datasets

The project includes multiple curated datasets for logical fallacy detection:

* **Logic Dataset**: 3,227 general logical fallacies from educational sources
* **LogicClimate Dataset**: 1,415 climate-related logical fallacies
* **NLI Datasets**: Over 170,000 entailment and fallacy examples
* **FOLIO Dataset**: Formal logic inference examples

<Note>
  Each dataset contains labeled examples distinguishing valid logical arguments (label=1) from fallacious ones (label=0).
</Note>

## Research Context

This work bridges natural language understanding and formal logic verification, enabling automated detection of reasoning errors in arguments. The approach is particularly useful for:

* Fact-checking and misinformation detection
* Educational tools for teaching logical reasoning
* Automated argument quality assessment
* Research in logical fallacy classification

## Citation

For academic use, please cite the original paper:

```text theme={null}
NL2FOL: Translating Natural Language to First Order Logic for Logical Fallacy Detection
ArXiv: https://arxiv.org/abs/2405.02318
```

## Next Steps

<CardGroup cols={2}>
  <Card title="Installation" icon="download" href="/installation">
    Set up the NL2FOL environment and dependencies
  </Card>

  <Card title="Quick Start" icon="rocket" href="/quickstart">
    Run your first logical fallacy detection
  </Card>
</CardGroup>