f i p：python中的逻辑框架
FLi的Python项目详细描述
flip是用python编写的逻辑框架。逻辑框架是 用于定义逻辑和编写定理等应用程序的库 证明人。一个flip应用程序是一个用于输入和 以自然演绎的方式编辑校样。这是一些来自 检查器，由python验证脚本生成：
Kaye ex. 9.12, ~Ax.P(x) |- Ex.~P(x) (0) Comment ~Ax.P(x) (1) Given |~Ex.~P(x) (2) Assumption ||Let x be arbitrary (3) New variable for subproof |||~P(x) (4) Assumption |||Ex.~P(x) (5) E-Introduction (4) |||F (6) Contradiction (5) (2) ||~~P(x) (7) Reductio Ad Absurdum (4) (6) ||P(x) (8) Not-Elimination (7) |Ax.P(x) (9) A-Introduction (3) (8) |F (10) Contradiction (9) (1) ~~Ex.~P(x) (11) Reductio Ad Absurdum (2) (10) Ex.~P(x) (12) Not-Elimination (11)
检查器可以使用不同的逻辑；flip有几个逻辑。你 可以通过编写一个逻辑来添加另一个逻辑，或者添加公理和派生规则。 python中的模块。python既是对象语言又是 元语言。公式、推理规则和整个证明都是python 表达。prover命令是python函数。Python 解释器本身是校对程序的唯一用户界面 申请。（使用 检查器。）
flip是作为一个python编程练习进行的。不是的 旨在与诸如hol等工业强度定理证明者竞争， 也没有像Jape这样设计精良的教育专家。 也就是说，检查者很有能力处理示例和 大学计算机逻辑或 数学，如凯、胡特、瑞安和博纳特。
欢迎加入QQ群-->： 979659372
