命题逻辑系统的自动推理.rar

【实例简介】
本程序用归结反演策略实现了命题逻辑系统的自动推理 归结方法的基本算法很简单，每次从子句集中选择两个可进行归结的子句，求它们的归结式，如果归结式为NIL，则算法结束，结论得证。如果归结式不为空，则将该归结式加入到子句集中，继续以上过程。
【实例截图】
【核心代码】
Autologic.rar
└── Autologic
└── Autologic
├── back
│   ├── 1 系统总体介绍.doc
│   ├── 5 字符映射和逆波兰变换.doc
│   ├── 6 逻辑蕴含.doc
│   ├── 7 逻辑求逆的消去处理.doc
│   ├── 9 归结反演.doc
│   └── SNAG-0000.jpg
├── Debug
│   ├── vc60.idb
│   └── vc60.pdb
├── Debug_Build
│   ├── Project1my.#00
│   ├── Project1my.obj
│   ├── Project1my.pch
│   ├── Stack1.obj
│   ├── Unit1my.obj
│   ├── Unit2my.obj
│   └── Unit3my.obj
├── Project1my.bpr
├── Project1my.cbproj
├── Project1my.cbproj.local
├── Project1my.cpp
├── Project1my.dsp
├── Project1my.dsw
├── project1my.exe
├── Project1my.map
├── Project1my.ncb
├── Project1my.obj
├── Project1my.opt
├── Project1my.plg
├── Project1my.res
├── Project1my.tds
├── Release_Build
│   ├── Project1my.#00
│   ├── Project1my.obj
│   ├── Project1my.pch
│   ├── Stack1.obj
│   ├── Unit1my.obj
│   ├── Unit2my.obj
│   └── Unit3my.obj
├── Stack1.cpp
├── Stack1.h
├── Stack1.obj
├── Train
│   ├── 1.txt
│   ├── test10.txt
│   ├── test1.txt
│   ├── test2.txt
│   ├── test3.txt
│   ├── test4.txt
│   ├── test5.txt
│   ├── test6.txt
│   ├── test7.txt
│   ├── test8.txt
│   └── test9.txt
├── Unit1my.cpp
├── Unit1my.ddp
├── Unit1my.dfm
├── Unit1my.h
├── Unit1my.obj
├── Unit2my.cpp
├── Unit2my.ddp
├── Unit2my.dfm
├── Unit2my.h
├── Unit2my.obj
├── Unit3my.cpp
├── Unit3my.ddp
├── Unit3my.dfm
├── Unit3my.h
└── Unit3my.obj

7 directories, 65 files