First-Order Logic (FOL)

The aria.fol module provides Miniprover, an automated theorem prover for first-order logic. This is a pedagogical implementation that is guaranteed to find proofs for all provable formulae (though it may loop forever for some unprovable ones, per Gödel’s Entscheidungsproblem).

Directory Structure

``` fol/ └── miniprover/

├── __init__.py (0 lines - empty) ├── language.py (517 lines) ├── prover.py (525 lines) ├── main.py (526 lines) └── README.md (95 lines) └── __pycache__/ (compiled Python files)

```

Module Purpose

Miniprover is an educational first-order logic theorem prover using sequent calculus. It serves as:

  1. Pedagogical tool for teaching proof search strategies

  2. Reference implementation for building efficient FOL provers

  3. Research foundation for experimenting with inference rules

Note: This is intentionally slow for practical use - it’s designed for correctness and educational value, not performance.

Key Components

### 1. Language Definitions (language.py - 517 lines)

Defines the complete FOL language with support for unification and substitution.

Terms:

  • Variable: FOL variables with name and instantiation time tracking - Tracks when variables were created for temporal reasoning

  • Function: Represents function applications with recursive term structure - Example: f(g(x), h(f(a), b)

  • UnificationTerm: Metavariables used during unification - Supports occurs-check to prevent infinite unification

Formulae:

  • Predicate: Atomic formulas with name and term arguments - Example: P(x), R(f(x), y)

  • Not: Logical negation (¬φ)

  • And/Or: Logical conjunction and disjunction

  • Implies: Logical implication (φ → ψ)

  • ForAll/ThereExists: Universal and existential quantification

Common Methods (across all classes):

  • freeVariables(): Extract all free variables

  • freeUnificationTerms(): Extract all unification metavariables

  • replace(old, new): Substitute terms/variables

  • occurs(term): Occurs-check for unification safety

  • setInstantiationTime(time): Track when terms were created

### 2. Theorem Prover (prover.py - 525 lines)

Implements complete sequent calculus with unification-based proof search.

Unification Engine:

  • unify(term_a, term_b): Solves single unification equations - Uses occurs-check to prevent infinite loops - Returns unification substitution or failure

  • unify_list(pairs): Solves multiple unification equations simultaneously - More efficient than pairwise solving

Sequent Calculus:

  • Sequent class: Represents sequents (Γ ⊢ Δ) - Left side (Γ): Set of formulae assumed true - Right side (Δ): Set of formulae to be proven - Sibling tracking: Manages parallel proof branches - Depth information: Tracks proof depth for ordering

Proof Search:

  • proveSequent(sequent): Main proof search algorithm - Breadth-first expansion of sequents - Formula ordering: Expands by creation time (depth-first within each sequent) - Inference rules: Complete set of left and right rules for all connectives - Parallel branch handling: Manages sibling sequents for unification across branches

Key Inference Rules Implemented:

  • Left rules (for Γ): - Not-left: If ¬φ ∈ Γ, add φ to Γ and move ¬φ to Δ - And-left: If φ∧ψ ∈ Γ, create two branches (φ) and (ψ) - Or-left: If φ∨ψ ∈ Γ, add both to Γ - Implies-left: If φ→ψ ∈ Γ, add ψ to Γ, move φ to Δ - ForAll-left: If ∀x.φ ∈ Γ, instantiate with fresh term

  • Right rules (for Δ): - Not-right: Move ¬φ to Γ, add φ to Δ - And-right: If φ∧ψ ∈ Δ, add both to Δ - Or-right: If φ∨ψ ∈ Δ, create two branches - Implies-right: If φ→ψ ∈ Δ, move φ to Γ, add ψ to Δ - ThereExists-right: If ∃x.φ ∈ Δ, instantiate with fresh term

Proof Strategy:

  • Formula selection: Expands formulas in order of creation time - Within sequent: depth-first (most recent first)

  • Universal quantification: Skolem-style unification terms - Introduces unification metavariables for instantiations

  • Existential quantification: Fresh variable instantiation - Ensures no variable capture during substitution

### 3. Command-Line Interface (main.py - 526 lines)

Interactive theorem prover REPL with formula management.

Lexer/Parser:

  • lex(inp): Tokenizes input strings into tokens - Handles identifiers, operators, quantifiers, parentheses - Supports whitespace and comments

  • parse(tokens): Recursive descent parser - Operator precedence: quantifiers > implication > disjunction > conjunction > not > atoms - Type checking: Validates well-formedness of formulae - Error messages: Clear feedback on parse errors

Syntax Support:

  • Variables: x, y, z (lowercase identifiers)

  • Functions: f(term, ...)

  • Predicates: P(term) (uppercase identifiers)

  • Logical operators: not, and, or, implies

  • Quantifiers: forall x. P, exists x. P

Interactive Session:

  • Formula input and proof verification

  • Axiom management: add, list, remove axioms

  • Lemma management: prove lemmas, add them, list, remove - Tracks dependencies between lemmas

  • Reset functionality: Clear session state

Session Commands:

### 4. Documentation (README.md - 95 lines)

Comprehensive guide including:

  • Purpose and limitations - Pedagogical tool: Intentionally slow - Completeness: Guaranteed to find proofs for provable formulae - Gödel limitation: May loop forever on unprovable formulae - Logic: Implements intuitionistic sequent calculus (not classical)

  • Syntax reference: Complete grammar with examples

  • Interactive session example: Demonstrates proof steps with sequent numbering

  • Axiom and lemma usage: Examples of building knowledge bases

Algorithms Implemented

  1. Unification Algorithm: First-order unification with occurs-check - Time-based instantiation constraints - Handles substitution composition

  2. Sequent Calculus: Complete set of inference rules - Left rules (for assumptions in Γ) - Right rules (for goals in Δ) - Proper handling of quantifiers

  3. Proof Search: Breadth-first exploration - Parallel branch management - Unification for closing branches - Skolemization for universal quantification - Fresh variable generation for existential quantification

  4. Formula Ordering: Depth-first within sequent, breadth-first globally

Usage Examples

### Python API

from aria.fol.miniprover.language import *
from aria.fol.miniprover.prover import proveFormula

# Define axioms and prove formulae
axioms = {
    ForAll(Variable('x'), Predicate('P', [Variable('x')])),
    ForAll(Variable('y'), Predicate('Q', [Variable('y')]))
}

formula = Implies(
    And(Predicate('P', [Variable('a')]),
    Predicate('Q', [Variable('a')]))
)

result = proveFormula(axioms, formula)
# Returns sequent or None if no proof found

### Interactive CLI

python -m aria.fol.miniprover.main

# Interactive session:
# Input: forall x. P(x)
# Prover: Added to axioms: [1]
# Input: P(a)
# Prover: ✓ Provable
#
# Input: implies (P(a)) (Q(a))
# Prover: ✓ Provable (1 steps)

Key Features

  1. Complete: Guaranteed to find proofs for all provable formulae

  2. Educational: Shows detailed proof steps with sequent numbering

  3. Unification-based: Handles equality and substitution automatically

  4. Axiom System: Supports custom axioms and lemma management - Dependency tracking for lemmas

  5. Interactive REPL: Rich command-line interface for experimentation

Strengths:

  • Clear separation between language definitions, prover logic, and CLI

  • Well-documented with comprehensive README

  • Proper error handling and user feedback

  • Comprehensive proof search with parallel branch handling

Limitations (as stated in documentation):

  • Performance: Too slow for practical use (pedagogical tool only)

  • Termination: May loop forever on unprovable formulae (Entscheidungsproblem)

  • Logic: Implements intuitionistic sequent calculus (not classical logic)

  • No practical applications: Intended for teaching and research, not production use

Size Statistics

  • Total Python lines: ~1,568

  • language.py: 517 lines

  • prover.py: 525 lines

  • main.py: 526 lines

  • README.md: 95 lines

Testing

While no explicit test files were found in the analysis, the module includes:

  • Manual testing through interactive sessions

  • Formula validation via type checking

  • Example proofs demonstrating various inference patterns

Use Cases

  1. Teaching first-order logic proof strategies

  2. Understanding sequent calculus mechanics

  3. Experimenting with axiom systems and lemma development

  4. Reference implementation for building efficient provers

  5. Research in automated deduction systems

Notable Design Decisions

  • Intuitionistic over classical: Matches pedagogical use case

  • Breadth-first search: Ensures completeness (won’t miss shorter proofs)

  • Creation time ordering: Reproduces typical textbook proofs

  • Unification terms: Implements Skolemization naturally