# fol-tp

**Repository Path**: flyingsheeplp/fol-tp

## Basic Information

- **Project Name**: fol-tp
- **Description**: interactive theorem prover for first-order logic
- **Primary Language**: Unknown
- **License**: Not specified
- **Default Branch**: master
- **Homepage**: None
- **GVP Project**: No

## Statistics

- **Stars**: 0
- **Forks**: 0
- **Created**: 2024-06-10
- **Last Updated**: 2025-11-17

## Categories & Tags

**Categories**: Uncategorized

**Tags**: None

## README

# fol-tp

#### 介绍
这是一个交互式定义证明器（目前纯手动- -||) , 目的旨在学习逻辑系统与现代的定理证明器(如coq,isabella等)的核心原理，逻辑系统采用德国数学家/哲学家 Gerhard Gentzen 于1934年提出的LK系统(Sequent Calculus风格)，这是现代结构化证明的开始，该系统已被Gentzen证明是正确且完备的。

可以看出定理证明器的核心是非常小的，整体代码量也不到1000行，并还有优化空间，在保证这个最小核心正确性的基础上进行易用性扩展就会得到各类现代的定理证明器。

#### 软件架构

User <-> REPL -> Parser -> | Goal Manager | Logic Inferencer | 

REPL : 和用户的交互界面，负责解析用户指令以及输出结果
Parser : 解析命题，转化为结构化的内部表示
Goal Manager : 负责管理命题，包括原始命题以及转化的自命题
Logic Inferencer: 负责进行逻辑推理，简单理解也就是对Goal进行变化，产生新的待证明自命题，最后归一到公理上

#### 逻辑规则


#### 使用说明
启动fol-tp后，会出现命令提示符 FOL-TP> , 然后根据用户输入进行交互，一般流程为

1. 使用goal指令定义一个待证明目标
```
FOL-TP> goal A |- A
```
2. 反复使用逻辑规则对目标进行处理，直到没有待证明目标
```
FOL-TP> refl
no more goals
```
3. 使用qed指令结束证明，输出证明过程
```
FOL-TP> qed
--------------
Theorem A|-A
   refl
   qed
```
4. 如果目标无法证明，也可以用abort指令放弃

#### 例子1
```
证明0阶命题 ~ ((A->(B\/C)) -> (((B->~A) /\ ~C) -> ~A))

            FOL-TP>goal |- ((A->(B\/C)) -> (((B->~A) /\ ~C) -> ~A))
            ⊢(A→(B∨C))→(((B→(¬A))∧(¬C))→(¬A))
            FOL-TP>ir 0
            ---
            A→(B∨C)⊢((B→(¬A))∧(¬C))→(¬A)
            ---
            FOL-TP>ir 0
            ---
            A→(B∨C),(B→(¬A))∧(¬C)⊢¬A
            ---
            FOL-TP>il 0
            ---
            (B→(¬A))∧(¬C),B∨C⊢¬A
            (B→(¬A))∧(¬C)⊢¬A,A
            ---
            FOL-TP>al 0
            ---
            B∨C,B→(¬A),¬C⊢¬A
            (B→(¬A))∧(¬C)⊢¬A,A
            ---
            FOL-TP>il 1
            ---
            B∨C,¬C,¬A⊢¬A
            B∨C,¬C⊢¬A,B
            (B→(¬A))∧(¬C)⊢¬A,A
            ---
            FOL-TP>wl 0
            ---
            ¬C,¬A⊢¬A
            B∨C,¬C⊢¬A,B
            (B→(¬A))∧(¬C)⊢¬A,A
            ---
            FOL-TP>wl 0
            ---
            ¬A⊢¬A
            B∨C,¬C⊢¬A,B
            (B→(¬A))∧(¬C)⊢¬A,A
            ---
            FOL-TP>refl
            ---
            B∨C,¬C⊢¬A,B
            (B→(¬A))∧(¬C)⊢¬A,A
            ---
            FOL-TP>or 0
            not a RIGHT-OR formula
            FOL-TP>ol 0
            ---
            ¬C,C⊢¬A,B
            ¬C,B⊢¬A,B
            (B→(¬A))∧(¬C)⊢¬A,A
            ---
            FOL-TP>nl 0
            ---
            C⊢¬A,B,C
            ¬C,B⊢¬A,B
            (B→(¬A))∧(¬C)⊢¬A,A
            ---
            FOL-TP>wr 0
            ---
            C⊢B,C
            ¬C,B⊢¬A,B
            (B→(¬A))∧(¬C)⊢¬A,A
            ---
            FOL-TP>wr 0
            ---
            C⊢C
            ¬C,B⊢¬A,B
            (B→(¬A))∧(¬C)⊢¬A,A
            ---
            FOL-TP>refl
            ---
            ¬C,B⊢¬A,B
            (B→(¬A))∧(¬C)⊢¬A,A
            ---
            FOL-TP>wl 0
            ---
            B⊢¬A,B
            (B→(¬A))∧(¬C)⊢¬A,A
            ---
            FOL-TP>wr 0
            ---
            B⊢B
            (B→(¬A))∧(¬C)⊢¬A,A
            ---
            FOL-TP>refl
            ---
            (B→(¬A))∧(¬C)⊢¬A,A
            ---
            FOL-TP>nr 0
            ---
            (B→(¬A))∧(¬C),A⊢A
            ---
            FOL-TP>wl 0
            ---
            A⊢A
            ---
            FOL-TP>refl
            ---
            
            ---
            FOL-TP>qed
            ---------------------------------------------
            Theorem - ⊢(A→(B∨C))→(((B→(¬A))∧(¬C))→(¬A))
              apply rule - "RIGHT-IMPLY"
              apply rule - "RIGHT-IMPLY"
              apply rule - "LEFT-IMPLY"
              apply rule - "LEFT-AND"
              apply rule - "LEFT-IMPLY"
              apply rule - "LEFT-WEAKENING"
              apply rule - "LEFT-WEAKENING"
              refl
              apply rule - "LEFT-OR"
              apply rule - "LEFT-NEG"
              apply rule - "RIGHT-WEAKENING"
              apply rule - "RIGHT-WEAKENING"
              refl
              apply rule - "LEFT-WEAKENING"
              apply rule - "RIGHT-WEAKENING"
              refl
              apply rule - "RIGHT-NEG"
              apply rule - "LEFT-WEAKENING"
              refl
              qed
            ---------------------------------------------
            FOL-TP>
```

#### 例子2
```
证明带量词的命题 ~ ∃x.∀y.P(y,x)⊢∀x.∃y.P(x,y)

        FOL-TP>goal EXISTS x. (ALL y. P(y,x)) |- ALL x. (EXISTS y. P(x,y))
        ∃x.∀y.P(y,x)⊢∀x.∃y.P(x,y)
        FOL-TP>el 0
        ∀y.P(y[?x],?x)⊢∀x.∃y.P(x,y)
        FOL-TP>ll 0
        P(?y[?x],?x[?y])⊢∀x.∃y.P(x,y)
        FOL-TP>instl 0 ?y 0
        P(0[?x],?x)⊢∀x.∃y.P(x,y)
        FOL-TP>instl 0 ?x 1
        P(0,1)⊢∀x.∃y.P(x,y)
        FOL-TP>lr 0
        P(0,1)⊢∃y.P(?x,y[?x])
        FOL-TP>er 0
        P(0,1)⊢P(?x[?y],?y[?x])
        FOL-TP>instr 0 ?x 0
        P(0,1)⊢P(0[?y],?y)
        FOL-TP>instr 0 ?y 1
        P(0,1)⊢P(0,1)
        FOL-TP>refl
        
        FOL-TP>qed
        ---------------------------------------------
        Theorem - ∃x.∀y.P(y,x)⊢∀x.∃y.P(x,y)
          apply rule - "LEFT-EXISTS"
          apply rule - "LEFT-ALL"
          LEFT-INSTANTIATE - instantiate ?y with 0
          LEFT-INSTANTIATE - instantiate ?x with 1
          apply rule - "RIGHT-ALL"
          apply rule - "RIGHT-EXISTS"
          RIGHT-INSTANTIATE - instantiate ?x with 0
          RIGHT-INSTANTIATE - instantiate ?y with 1
          refl
          qed
        ---------------------------------------------
```