Modified readme

README.md

@@ -11,6 +11,8 @@
 * [课程目录](#课程目录)
 * [管理与投稿](#管理与投稿)
     * [投稿方式](#投稿方式)
+        * [Fork](#fork)
+        * [更新内容并PR](#更新内容并pr)
     * [投稿建议](#投稿建议)
     * [管理工作](#管理工作)
     * [管理要求](#管理要求)
@@ -121,6 +123,7 @@
 
 ## 投稿方式
 
+### Fork
 * 发给管理员帮忙上传
 
 * 用网页或者[桌面版](https://desktop.github.com/)直接操作，fork and pull request, 
@@ -146,8 +149,16 @@ echo "公选课/人工智障"  >> .git/info/sparse-checkout  #这里工作目录
 #只需记住的是 加入的目录应该在远程仓库存在，否则报错“error: Sparse checkout leaves no entry on the working directory”
 
 git pull origin master
+git remote add upstream [email protected]:mbinary/USTC-CS-Courses-Resource.git 
+```
+### 更新内容并PR
+>建议: 如果没有较大的改动, 或者在改动之前,可以删除掉以前 fork 的仓库 重新 fork
+* [使用网页操作](https://blog.csdn.net/huutu/article/details/51018317)
+* 命令行
+```shell
+git fetch upstream/master
+git merge upstream/master
 ```
-
 
 ## 投稿建议
 * 由于 github 上不能直接上传大于 100mb 的文件，所以就不要上传太大的文件。可以存在云盘，然后将云盘链接发在这里。

大二下/数理逻辑/students/mbinary/README.md

@@ -0,0 +1,43 @@
+>写的一个简单的脚本实现 在 L 下的公式证明, 有兴趣的同学可以看看, 算是抛砖引玉吧
+
+# system-L
+
+## Descripton
+it's a formal logic deduction based on system-L
+### symbols
+`~` , `->`  (in the script, i use > to repr it)
+### rules
+The basic three axioms:
+* L1: `p->(q->p)`
+* L2: `(p->(q->r)) -> ((p->q)->(p->r))`
+* L3: `~q->~p -> (p->q)`
+
+### deduction
+{p,p->q} |- q
+
+you can read the professional [book](src/mathematical-logic.pdf)
+or click [here](https://en.wikipedia.org/wiki/Mathematical_logic) to see more details 
+
+## Idea
+To prove one proposition:
+* Firstly, I use deduction theorem(演绎定理) to de-level the formula and finally get a prop varible or a prop in form of `~(...)`. let's  mark it as p or ~p
+* Next, I create a set `garma` and fill it with  some generated  formulas using the three axioms(公理),some theorem and conclusions.
+* Then, I search p or ~p in `garma, or further, using modus ponent(MP) to deduct  p or ~p.
+* Finally, if using mp can't prove it, I will use `Proof by contradiction`(反证法) to prove it.
+
+## Requirement
+python modules
+* sympy
+
+## Visual
+
+![](src/sys-L.png)
+
+## To do
+* 将证明过程对象化,便于处理,打印(英文版,中文版),
+* 其他连接词的转换
+* 处理简单的, 有一定模式的自然语言, 形成命题推理
+
+## Contact
+* mail: [email protected]
+* QQ  : 414313516