Proof Assistant

This project is written in OCaml as part of a Functional Programming course. It serves as a Proof Assistant, supporting logical reasoning and theorem proving in first-order logic. The project is modular, allowing for different theories to be implemented and used in conjunction with the core Logic Module.

Features

• Representation of Formulas
• Representation of Theorems
• Operations for Deduction Rules
• Extensible Theory Framework
• Unit Tests with Alcotest
• Interactive Testing with UTop

Logic Module

The Logic Module provides tools for representing and reasoning about first-order logic formulas and theorems. It supports:

Representation of Terms and Formulas

Terms and formulas are defined as follows:

type term =
  | Var of string
  | Sym of string * term list

type formula =
| Bot                       (* Bottom ⊥ *)
| Imp of formula * formula  (* Implication φ → ψ *)
| Rel of sym * term list    (* Relation symbol r(t1,...,tn) *)
| All of var * formula      (* Universal quantifier (∀x. φ) *)

Logical Deduction Rules

The following deduction rules are implemented:

1. By Assumption

Constructs a theorem where the formula is both the assumption and the consequence:

val by_assumption : formula -> theorem

-------(Ax)
{f} ⊢ f

2. Implication Introduction (→I)

Derives an implication $f \to \phi$ by removing $f$ from the assumptions:

val imp_i : formula -> theorem -> theorem

       thm
      Γ ⊢ φ
---------------(→I)
Γ \ {f} ⊢ f → φ

3. Implication Elimination (→E)

Applies modus ponens to derive $\psi$ from $\phi \to \psi$ and $\phi$:

val imp_e : theorem -> theorem -> theorem

thm1      thm2
Γ ⊢ φ → ψ    Δ ⊢ φ
------------------(→E)
Γ ∪ Δ ⊢ ψ

4. Bottom Elimination (⊥E)

Derives any formula $f$ from a contradiction:

val bot_e : formula -> theorem -> theorem

   thm
  Γ ⊢ ⊥
  -----(⊥E)
  Γ ⊢ f

5. Universal Quantifier Introduction (∀I)

Introduces a universal quantifier $\forall x.,φ$ by removing the free variable $y$ from the assumptions:

val forall_i : var -> theorem -> theorem

       thm
      Γ ⊢ φ
------------------(∀I)
Γ ⊢ ∀x. φ   (provided x ∉ fv(Γ))

6. Universal Quantifier Elimination (∀E)

Eliminates a universal quantifier $\forall x.,φ$ by instantiating $x$ with a term $t$:

val forall_e : term -> theorem -> theorem

        thm
      Γ ⊢ ∀x. φ
-----------------(∀E)
     Γ ⊢ φ{x→t}

7. Renaming Free Variables

Renames a free variable $x$ in the assumptions and conclusion to a new variable $y$, provided $y$ does not appear free:

val rename_free : var -> var -> theorem -> theorem

        thm
     Γ ⊢ φ   y ∉ (fv(Γ) ∪ fv(φ))
---------------------------(RenFree)
 Γ{x → y} ⊢ φ{x → y}

8. Renaming Bound Variables

Renames a bound variable in the conclusion by providing a formula that is $\alpha$-equivalent to the old conclusion:

val rename_bound : formula -> theorem -> theorem

     thm1
    Γ ⊢ ψ
----------------(RenBound)
   Γ ⊢ φ
    thm2

---

Peano Arithmetic as an Example Theory

The Logic Module is parameterized by a Theory Module, allowing different axiomatic systems to be defined. Peano Arithmetic is implemented as an example of such a theory.

Representation of Peano Arithmetic Axioms

The Peano Axioms are defined as follows:

type axiom =
  | EqRefl                      (* ∀x. x = x *)
  | EqElim of var * formula     (* ∀y.∀z. y = z ⇒ φ{x → y} ⇒ φ{x → z} *)
  | PlusZ                       (* ∀n. 0 + n = n *)
  | PlusS                       (* ∀n.∀m. S(n) + m = S(n + m) *)
  | Induction of var * formula  (* Induction principle *)

These axioms allow for the proof of fundamental properties such as:

1. Identity of Addition: $\forall n. n + 0 = n$
2. Successor Property: $\forall n. \forall m. n + S(m) = S(n + m)$
3. Commutativity of Addition: $\forall n. \forall m. n + m = m + n$

Each of these can be formally proven using the inference rules of the Logic Module.

---

Installation and Running

1. Make sure you have OCaml (>= 4.12) and Dune (>= 3.7) installed.
2. Install Alcotest:

   opam install alcotest

3. Build the project:

   dune build

4. Run all tests:

   dune test

5. Optionally, run an interactive session:

   dune utop src

   Then load the printers and modules.

---

Example Usage

To try it interactively in UTop, run:

dune utop src

and then:

#use "example/install_pp_utop.ml";;

This sets up pretty-printers and imports the necessary modules.

A small usage example is provided in example/use_example.ml. It shows how to:

1. Open the Proof_assistant.Logic and Proof_assistant.Peano modules.
2. Construct variables and formulas using fresh_var, Rel, Sym, etc.
3. Build proofs using rules like axiom, by_assumption, imp_i, imp_e, forall_i, etc.
4. Inspect the final theorem or formula using the built-in pretty printers.

---

GitHub Repository

A GitHub repository containing this project is available here: Proof Assistant on GitHub

---