forseti 0.8.1

安装

$ pip install forseti

$ git clone git@github.com:MasterOdin/forseti.git
$ python setup.py install

用法

forseti带有命题演算公式的内部表示（原子、非、与、或、蕴涵和等价）。它可以从中任何公式的函数表示生成。内部上，它将所有内容都作为公式对象持有，可以接受适当的公式（符号只能保存一个字符串）。

示例

from forseti import parser
from forseti.predicate import Atomic, And
assert parser.parse("and(a, b)") == And(Atomic('a'), Atomic('b'))

此外，它还包含一个内置的证明器，可以验证命题演算论证

from forseti.prover import Prover
prover = Prover()
prover.add_formula("if(A,and(B,C))")
prover.add_formula("iff(C,B)")
prover.add_formula("not(C)")
prover.add_goal("not(A)")
assert_true(prover.run_prover())

路线图

1. 一阶逻辑证明器

2. 优化

用法

这些项目在其核心使用forseti

1. 真值表

目标

使用forseti实现以下程序/应用程序

1. 自动定理证明器（在forseti核心中完成）

2. 实现Davis-Putnam算法

3. 真值树

4. Slate / Fitch