C++实现王浩算法：逆推与转换示例

// WangHao.cpp: 定义控制台应用程序的入口点。
//

#include "stdafx.h"
#include<iostream>
#include<string>
using namespace std;
bool right_arrow(const string& g);
void transfer_darrow(string &g,int cos);
int rcenter_arrow(const string &g,int aos);
bool left_arrow(const string& g);
int lcenter_arrow(const string& g, int aos);

int main()
{
cout << "王浩算法推理规则如下：" << endl;
cout << "\t规则一：\t若a,b=>x,y,则a,~x,b=>y;\n";
cout << "\t规则二：\t若a,x=>b,y,则a=>b,~x,y;\n";
cout << "\t规则三：\t若a,~x,b=>y且a,y,b=>y,则a,(x->y),b=>y;\n";
cout << "\t规则四：\t若a=>b,~x,y,Y,则a=>b,(x->y),Y;\n";
cout << "请输入公式行（由命题符号、&、|、~、->、<->、圆括号组成）：\n";
string gongshi;
getline(cin, gongshi);
cout << gongshi << endl;
string sjt = "=>";
gongshi.insert(0, sjt);
cout << "将其放在相继式后面：" << gongshi << endl;     
while (right_arrow(gongshi)) {
string  sjt2 = "=>";
int aos = gongshi.find(sjt2);

int i = 0;
for (i = aos + 2; i < gongshi.size(); i++)
if (gongshi[i] == '-')
if (gongshi[i + 1] == '>'&&gongshi[i - 1] == '<') {
transfer_darrow(gongshi, i);          
cout << "消掉“双箭头”：" << gongshi << endl;
}                                                                                   //将双箭头转化成单箭头；
for (int i = aos + 2; i < gongshi.size(); i++)
if (gongshi[i] == '|')
gongshi.replace(i, 1, ",");
int bos = rcenter_arrow(gongshi,aos);
if (bos == 100) {
break;
cerr << "有错误发生了" << endl;
system("pause");
EXIT_FAILURE;
}          //找到中心单箭头;
gongshi.insert(aos + 2, "~");
gongshi.replace(bos + 1, 2, ",");
cout << "由规则四，需证明如下：" << gongshi << endl;          //去除核心单箭头,并将“或”符号转化成逗号；
int count = 0;
int pos[10] = { 100,100,100,100,100,100,100,100,100,100 };
for (int i = aos + 2; i < gongshi.size(); i++)
if (gongshi[i] == ',')
pos[count++] = i;
count++;
string term[10] = { "Fail","Fail","Fail","Fail","Fail", "Fail", "Fail", "Fail", "Fail", "Fail" };
for (int i = 0; i < count; i++) {
if (i == 0)
term[i] = gongshi.substr(aos + 2, pos[i] - aos - 2);