---
tags: teaching
---
## Natural Deduction Calculator Project

[项目文档](/1t_rO_u1RX687v1q8WDWOg)

### Subproject

[Combination of trees and decomposition of trees](/p8aXkZX9TdeQ_XJPkbijjA)

[形式证明方案设计](/xJIMi-FeTVKQao2foTAc8g)

### Resources

[Web 项目开发规范](https://www.kancloud.cn/chandler/css-code-guide/50867)

[Natural deduction proof editor and checker](https://proofs.openlogicproject.org/)

[Logic2010](https://logiclx.humnet.ucla.edu/)

[Concice Course for logic](http://solr.bccampus.ca:8001/bcc/file/17082e35-cf6d-43e1-a5be-7235b2cf8da0/1/A-Concise-Introduction-to-Logic-1490623862.pdf)

### Project Goal

A logic computing system that is able to verify easy deduction steps

### Object Type

Our basic core object is the expression tree. This is a tree with the following type of nodes

- Quantifier nodes: For example, Let, For all $\forall$, For some $\exists$.
- Global Operator nodes: For example $+,\times,\land,\lor$
- Local Operator nodes: a link to Quantifier nodes.

### Design
#### Representation for quantifiers

Quantifiers|Code base 16
-|-
let|0x000
$\forall$|0x001
$\exists$|0x002

#### Representation for global operators

- We must decide a code for quantifiers and code for $+,-,\times,\frac1x,\land,\lor,\lnot$

Parantesis|Code base 16
-|-
(|0x010
)|0x011

Logic Operators|Code base 16
-|-
$\lnot$|0x020
$\land$|0x021
$\lor$|0x022

Common compare operators|Code base 16
-|-
$=$|0x100
$<$|0x101
$>$|0x102

Common Binary Operators|Code base 16
-|-
$-$|0x200
$+$|0x201
$\frac{1}{a}$|0x202
$\times$|0x203

### Libraries
#### Set Theory
Common operators|Code base16
-|-
$\in$|0x10000

Common logic expressions|Code base 16
-|-
p(x): x is set|0x11000

#### Representation for local operaotrs

Local operator is a link to a quantifier nodes. It could be represent as **a non-zero integer**, indicating how many steps one need to take to associate the local operator to quantifier nodes. **I am thinking to represent it as negative numbers**

For example, here is the expression tree for "Let p Let q, p or q"

**Question** Design a criterion of text input to represent the expression tree

digraph hierarchy {

                nodesep=1.0 // increases the separation between nodes
                
                node [color=Red,fontname=Courier,shape=circle] //All nodes will this shape and colour
                edge [color=Blue] //All the lines look like this

Root -> "Let p"-> "Let q"-> or -> {p q}
                 // Put them on the same level
}

We would store it as a tree

digraph hierarchy {

                nodesep=1.0 // increases the separation between nodes
                
                node [color=Red,fontname=Courier,shape=circle] //All nodes will this shape and colour
                edge [color=Blue] //All the lines look like this

Root -> "0x00"-> "0x00 "-> "0x12" -> {-3 -2}
                 // Put them on the same level
}

Here we have all quantifier nodes, global operator nodes and local variable nodes. Here -3 means the local variable that declared by quantifier with the relative position of 3 steps above.

### Test

The definition of a function $f:X\longrightarrow Y$ has the limit
$$
\lim_{x\mapsto c}f(x)=L
$$

$\epsilon-\delta$

Language: Let $X$,$Y$ be two sets, $f$ is a map $f:X\rightarrow Y$. We call
$$
\lim_{x\mapsto c}f(x)=L
$$
if for any $\epsilon>0$, there exists $\delta>0$, such that forany $x'\in X$, we have $|x'-x|<\delta\implies |f(x)-L|<\epsilon$

digraph hierarchy {

                nodesep=1.0 // increases the separation between nodes
                
                node [color=Red,fontname=Courier,shape=circle] //All nodes will this shape and colour
                edge [color=Blue] //All the lines look like this

"Let X"->"is set"

"Let Y"->" is set"

"forall t"->"in X"


"Let f"->"forall t"->"in Y"->" f "->" t" 

"Let c"->" in X"

"Let L"->" in Y"

"forany eps"->" >0"

"forsome del"->" >0 "

"forany x"->" in X  "

Root ->"Let X"->"Let Y"-> "Let f"->"Let c"->"Let L"->"forany eps"->"forsome del"->"forany x"->"=>" -> {"<" ," <"}


"<"->{"|.|" del}

" <"->{"|.| " eps}

"|.|"-> "-" -> {x c}

"|.| "-> " -" -> {f L}

f->" x "
}