从“G·德尔Escher Bach”，Douglas Hofstadter玩正式系统
FormalSystems的Python项目详细描述
这是一个python实现的douglas hofstadter形式系统，来自他的书gódel，escher，bach：一个永恒的金色辫子（通常是geb）。
实际上，您可以使用非常简单的语法定义自己的形式系统，接近自由文本。 本书中的miu、pg、fg和ndp形式系统的示例在目录definitions中实现。
一个主要的python脚本为您提供了使用正式系统的可能性，包括：
- 公理模式支持（迭代，决策过程）
- 定理逐步生成（使用不同算法）
- 定理推导
正式系统定义
示例
miu系统的定义可以是：
axioms:-MIrules:-x is .*, xI => xIU-x is .*, Mx => Mxx-x is .*, y is .*, xIIIy => xUy-x y .* , xUUy => xy
底层语法是yaml（参见raw格式）。您可以使用一个模式定义一个或多个公理，或者甚至无限数量的公理，如在^ {EM1}$PG
axioms:-x is -+, xp-gx-rules:-x y z are -+, xpygz => xpy-gz-
语法
公理定义应该像这样格式化（^ {Tt1} $这是可选的）：
[def_1, [def_2, ...]] expr
其中：
- def_i是通配符的可选定义，使用正则表达式，例如：
- “*”可以是任何内容，包括空字符串
- “-+”是由“-” 组成的字符串
如果不同的通配符具有相同的定义，则使用char [is] regexp或char1 char2 [are] regexp编写定义。请注意，通配符定义只能使用one character。
定理产生的规则格式如下：
[def_1, [def_2, ...]] cond_1 [and cond_2 [and ...]]=> th_1 [and th_2 [and ...]]
其中：
- def_i与以前相同
- cond_i是一个必需的定理，以便产生新的定理（如果有几个条件，则用和分隔）
- th_i是一个具有规则的产生定理
安装
安装时使用：
$ python setup.py install --user
脚本应该放在~/.local/bin中，确保此路径位于$PATH：
$ exportPATH=$PATH:~/.local/bin
测试
如果安装成功，请使用以下命令运行测试：
$ cd tests
$ python test_formalsystems.py -v
主脚本
安装之后，应该将主脚本FormalSystemsMain.py部署在$PATH指向的位置，名为FormalSystems。 如果不是这样，则可以直接执行脚本，前提是正确安装了依赖项（只要pyyaml和lepl）。
主脚本的用法在--help参数中有完整的文档记录。
如果公理的数量有限，你可以一步一步地生成定理。$ FormalSystems definitions/MIU.yaml --iteration 3 > Finite number of axioms, using step algorithm STEP 1: MI P (1) x is .*, xI=> xIU for MI gives MIU P (2) x is .*, Mx=> Mxx for MI gives MII . (3) x is .*, y is .*, xIIIy=> xUy for MI . (4) x y .* , xUUy=> xy for MI STEP 2: MIU/MII P (1) x is .*, xI=> xIU for MII gives MIIU . (1) x is .*, xI=> xIU for MIU P (2) x is .*, Mx=> Mxx for MII gives MIIII P (2) x is .*, Mx=> Mxx for MIU gives MIUIU . (3) x is .*, y is .*, xIIIy=> xUy for MII . (3) x is .*, y is .*, xIIIy=> xUy for MIU . (4) x y .* , xUUy=> xy for MII . (4) x y .* , xUUy=> xy for MIU STEP 3: MIIU/MIIII/MIUIU
或使用公理被抛出的桶，如果公理数是无限的，则迭代地计算定理：
$ FormalSystems definitions/pg.yaml --iteration 4 > Infinite number of axioms, using bucket algorithm [Adding -p-g-- to bucket]=== BUCKET 1: -p-g-- P (1) x y z are -+, xpygz=> xpy-gz- for -p-g-- gives -p--g--- [Adding --p-g--- to bucket]=== BUCKET 2: -p--g---/--p-g--- P (1) x y z are -+, xpygz=> xpy-gz- for -p--g--- gives -p---g---- P (1) x y z are -+, xpygz=> xpy-gz- for --p-g--- gives --p--g---- [Adding ---p-g---- to bucket]=== BUCKET 3: -p---g----/--p--g----/---p-g---- P (1) x y z are -+, xpygz=> xpy-gz- for -p---g---- gives -p----g----- P (1) x y z are -+, xpygz=> xpy-gz- for ---p-g---- gives ---p--g----- P (1) x y z are -+, xpygz=> xpy-gz- for --p--g---- gives --p---g----- [Adding ----p-g----- to bucket]=== BUCKET 4: -p----g-----/---p--g-----/--p---g-----/----p-g-----
也可以使用选项来显示定理推导：
$ FormalSystems definitions/NDP.yaml --quiet --derivation P----- > Infinite number of axioms, using bucket algorithm > Rule with several parents, using recursivity=== BUCKET 1: --NDP- === BUCKET 2: --NDP---/-SD--/P-- === BUCKET 3: --NDP-----/---SD--/---NDP-- === BUCKET 4: --NDP-------/---NDP-----/-----SD--/P---/---NDP- === BUCKET 5: --NDP---------/---NDP--------/---NDP----/-------SD--/-----SD---/-SD---/----NDP--- === BUCKET 6: ---NDP-----------/----NDP-------/---NDP-------/--NDP-----------/---------SD--/----NDP- === BUCKET 7: ----NDP-----------/----NDP-----/---NDP----------/---NDP--------------/--NDP-------------/-----------SD--/-------SD---/-SD----/----NDP-- === BUCKET 8: ----NDP---------/----NDP---------------/---NDP-------------/---NDP-----------------/--NDP---------------/----NDP------/-------------SD--/-------SD----/-----SD----/-----------SD---/-----NDP- === BUCKET 9: --NDP-----------------/-----NDP------/----NDP-------------/---NDP--------------------/---NDP----------------/----NDP----------/----NDP-------------------/---------------SD--/-SD-----/-------------SD---/-----------SD----/P-----/-----NDP-- === Theorem P----- found, derivation: [1] Axiom gives --NDP- [2](1) x y are -+, xNDPy=> xNDPxy for --NDP- gives --NDP--- [3] Axiom gives ---NDP-- [3](1) x y are -+, xNDPy=> xNDPxy for --NDP--- gives --NDP----- [4] Axiom gives ----NDP- [4](1) x y are -+, xNDPy=> xNDPxy for ---NDP-- gives ---NDP----- [4](2) z is -+, --NDPz => zSD-- for --NDP----- gives -----SD-- [5](1) x y are -+, xNDPy=> xNDPxy for ----NDP- gives ----NDP----- [5](3) x z are -+, zSDx and x-NDPz => zSDx- for -----SD-- and ---NDP----- gives -----SD--- [6](3) x z are -+, zSDx and x-NDPz => zSDx- for -----SD--- and ----NDP----- gives -----SD---- [7](4) z is -+, z-SDz => Pz- for -----SD---- gives P-----
python api
一些测试使用doctests：
>>>fromformalsystems.formalsystemsimportFormalSystem,Theorem
MIU正式系统：
>>>fs=FormalSystem()>>>fs.read_formal_system('./definitions/MIU.yaml')>>>r=fs.apply_rules_step(fs.iterate_over_schema(),step=4,verbose=False)STEP1:MISTEP2:MIU/MIISTEP3:MIIU/MIIII/MIUIUSTEP4:MIIIIU/MIIIIIIII/MIIUIIU/MIUIUIUIU/MIU/MUI>>>print[str(a)forainfs.iterate_over_schema()]['MI']
PG正式系统：
>>>fs=FormalSystem()>>>fs.read_formal_system('./definitions/pg.yaml')>>>r=fs.apply_rules_bucket_till(fs.iterate_over_schema(),max_turns=4,verbose=False)===BUCKET1:-p-g--===BUCKET2:-p--g---/--p-g---===BUCKET3:-p---g----/--p--g----/---p-g----===BUCKET4:-p----g-----/---p--g-----/--p---g-----/----p-g----->>>r=fs.apply_rules_bucket_till(fs.iterate_over_schema(),min_len=9,verbose=False)===BUCKET1:-p-g--===BUCKET2:-p--g---/--p-g---===BUCKET3:-p---g----/--p--g----/---p-g----
ndp正式系统：
>>>fs=FormalSystem()>>>fs.read_formal_system('./definitions/NDP.yaml')>>>r=fs.apply_rules_bucket_till(fs.iterate_over_schema(),max_turns=2,full=True,verbose=False)===BUCKET1:--NDP-===BUCKET2:--NDP---/-SD--/P--
成功推导：
>>>fs=FormalSystem()>>>fs.read_formal_system('./definitions/NDP.yaml')>>>r=fs.derivation_asc(fs.iterate_over_schema(),Theorem('P-----'),full=True,max_turns=10)<BLANKLINE>...===TheoremP-----found,derivation:...
派生失败：
>>>fs=FormalSystem()>>>fs.read_formal_system('./definitions/MIU.yaml')>>>r=fs.derivation_step(fs.iterate_over_schema(),Theorem('MIUIU'),step=5)<BLANKLINE>...===TheoremMIUIUfound,derivation:...>>>r=fs.derivation_step(fs.iterate_over_schema(),Theorem('MU'),step=5)<BLANKLINE>...===TheoremMUnotfound
欢迎加入QQ群-->： 979659372
