def ResolutionProp(KB):
    steps = []
    k = 1
    clause_dict = {}  # 记录子句及其编号--同时加入新增语句
    clause_labels = {}  # 记录子句内元素的编号
    
    # 初始化子句编号,同时将子句集列举出来
    for clause in KB:
        clause_dict[clause] = k
        steps.append(f"{k} {clause}")
        if len(clause) > 1: #有多个元素的子句编号a,b...
            clause_labels[clause] = {ele: chr(97 + i) for i, ele in enumerate(clause)} 
        k += 1
    
    clauses = list(KB)
    processed_KB = set()  # 记录已经归结过的子句--保证不会重复归结
    new_KB = set(clauses)  # 初始子句集--需要进行更新
    
    while new_KB:
        current_clauses = list(new_KB)  # 当前需要归结的新子句--上一轮生成的语句
        new_KB.clear() 
        
            
        
        for i in range(len(current_clauses)):
            for j in range(len(clauses)):  # 之前的子句 + 新生成的子句
                if current_clauses[i] == clauses[j]:  # 避免自身归结
                    continue
                if current_clauses[i] in processed_KB : # 这里是防止出现重复归结
                    continue
                if clauses[j] in processed_KB :
                    continue
                
                res, resolved_literals = resolve(current_clauses[i], clauses[j])
                if res is not None:
                    clause1_id = str(clause_dict[current_clauses[i]])
                    clause2_id = str(clause_dict[clauses[j]])
                    
                    # 处理字句编号
                    if len(current_clauses[i]) > 1 and resolved_literals[0] in clause_labels[current_clauses[i]]:
                        clause1_id += clause_labels[current_clauses[i]][resolved_literals[0]]
                    if len(clauses[j]) > 1 and resolved_literals[1] in clause_labels[clauses[j]]:
                        clause2_id += clause_labels[clauses[j]][resolved_literals[1]]
                    #在这里把已经归结的加入
                    processed_KB.add(current_clauses[i])
                    processed_KB.add(clauses[j])
                    
                    if res == ():#空子句
                        steps.append(f"{k} R[{clause1_id},{clause2_id}] = ()")
                        return steps
                    
                    if res not in clause_dict:
                        clause_dict[res] = k
                        if len(res) > 1:
                            clause_labels[res] = {lit: chr(97 + i) for i, lit in enumerate(res)}
                        new_KB.add(res)
                        clauses.append(res)
                        steps.append(f"{k} R[{clause1_id},{clause2_id}] = {res}")
                        k += 1
        
            
        #clauses.extend(current_clauses)  # 将新子句加入原始子句集中

    
    return steps

def resolve(clause1, clause2):
    for literal in clause1:
        complement = f"~{literal}" if literal[0] != '~' else literal[1:]
        if complement in clause2:
            # 新的子句应该去除字面量和互补字面量
            new_clause = tuple(sorted(set(clause1).union(set(clause2)) - {literal, complement}))
            
            # 如果新子句为空，返回空子句
            if not new_clause:
                return (), (literal, complement)
            return new_clause, (literal, complement)
    return None, None

def main():
    KB = {
        ('FirstGrade',), 
        ('~FirstGrade', 'Child'), 
        ('~Child',)
    }
    KB1={
        ('a',),
        ('b',)
    }
    KB2 = {
        ('A',), 
        ('~A', 'B'), 
        ('~B',)
    }
    KB3 = {
        ('P', 'Q'), 
        ('~P', 'R'), 
        ('~Q', 'R'), 
        ('~R',)
    }
    KB4 = {
        ('A', 'B'), 
        ('~A', 'C'), 
        ('~B', 'D'), 
        ('~C', '~D')
    }
    steps = ResolutionProp(KB)
    for step in steps:
        print(step)

#其实这部分可以直接使用find()来查找第一个左括号，再使用切片
i=0
for i in range(len(literal1)):
    if literal1[i]!='(':
        i+=1
    else:
        break

# 去掉P(),然后使用split以逗号划分项
lit1=literal1[i+1:-1].split(',')
lit2=literal2[i+1:-1].split(',')

#不等长无法合并--特殊情况
if len(lit1)!=len(lit2):
    return None

#遍历两个集合
   for i in range(len(lit1)):
       if lit1[i]==lit2[i]:
           continue
       
       if lit1[i] != lit2[i]:
           # 查看字符串里是否存在变量？如果都是变量无法合一--单独一个变量，不是项
           v1=Check_Var(lit1[i])
           v2=Check_Var(lit2[i])
           #全都含有变量，无法合一
           if v1 and v2:
              return None 
           elif v1 is True and v2 is False:
               if v1 in res:
                   #如果v1在res中已经进行了项的替换，不能再替换成其他的
                   return None 
               #v1是变量，v2是项
               res[lit1[i]]=lit2[i]
               for j in range(i+1,len(lit1)):
                   lit1[j]=lit1[j].replace(lit1[i],lit2[i])
                   lit2[j]=lit2[j].replace(lit1[i],lit2[i])
           elif v2 is True and v1 is False:
               if v2 in res:
                   #如果v1在res中已经进行了项的替换，不能再替换成其他的
                   return None 
               #v1是变量，v2是项
               res[lit2[i]]=lit1[i]
               for j in range(i+1,len(lit1)):
                   lit1[j]=lit1[j].replace(lit2[i],lit1[i])
                   lit2[j]=lit2[j].replace(lit2[i],lit1[i])
           else:
               #单独判断--可能存在嵌套的函数项
               if '(' in lit1[i] and '(' in lit2[i]:
                   sub_res=MGU(lit1[i],lit2[i])
                   if sub_res is None:
                       return None
                   else: 
                       res.update(sub_res)
               else:   
                   return None 

def main():
    # literal1='P(f(zz))'
    # literal2='P(f(f(u)))'
    # literal1='P(xx,a)'
    # literal2='P(b,yy)'
    # literal1='P(zz,xx)'
    # literal2='P(a,f(zz))'
    literal1='P(a,xx,f(g(yy)))'
    literal2='P(zz,f(zz),f(uu))'
    res=MGU(literal1,literal2)
    if res is not None:
        for key,value in res.items():
            print(key,":",value)
    else:
        print("NO MGU found")
        

def ResolutionFOL(KB):
    steps = []
    k = 1
    clause_dict = {}  # 记录子句及其编号--同时加入新增语句
    clause_labels = {}  # 记录子句内元素的编号
    
    # 初始化子句编号,同时将子句集列举出来
    for clause in KB:
        clause_dict[clause] = k
        clause_str = format_clause(clause)
        steps.append(f"{k} {clause_str}")
        
        if len(clause) > 1:#有多个元素的子句编号a,b...
            clause_labels[clause] = {}
            for i, literal in enumerate(clause):
                clause_labels[clause][literal] = chr(97 + i)  
        k += 1
    
    original_size = k - 1  # 记录原始子句集的大小
    #原始子句集
    clauses = list(KB)
    # 记录已经归结过的子句--保证不会重复归结（但问题是一阶逻辑是可以多次为量词赋值的，所有我们记录的不是归结过的单个子句，而是子句对）
    processed = set()   
   
    while True:
        new_resolvents = []
        
        for i in range(len(clauses)):
            for j in range(i + 1, len(clauses)):
                if clauses[i] == clauses[j]:  # 避免自身归结
                    continue
                c1 = clauses[i]
                c2 = clauses[j]
                
                if (c1, c2) in processed:
                    continue
                #这里加入子句对
                processed.add((c1, c2))
                processed.add((c2, c1))
                
                resolvents = resolve(c1, c2)
                
                for resolvent_info in resolvents:
                    #由于输出需要含有合一替换，所以resolve函数有一些变化
                    resolvent, lit1, lit2, mgu = resolvent_info
                    
                    # 编号
                    clause1_id = str(clause_dict[c1])
                    clause2_id = str(clause_dict[c2])
                    
                    # 处理元素的编号
                    if len(c1) > 1 and lit1 in clause_labels.get(c1, {}):
                        clause1_id += clause_labels[c1][lit1]
                    
                    if len(c2) > 1 and lit2 in clause_labels.get(c2, {}):
                        clause2_id += clause_labels[c2][lit2]
                    
                    #MGU调用
                    mgu_str = format_mgu(mgu)
                    
                    # 查看是否产生了空集
                    if resolvent == ():
                        steps.append(f"{k} R[{clause1_id},{clause2_id}]{mgu_str} = ()")
                        # 找到空子句，简化归结过程
                        simplified_steps = Simplify(steps, original_size)
                        return simplified_steps
                    
                    # 将新的子句加入子句集
                    if resolvent not in clause_dict:
                        clause_dict[resolvent] = k
                        
                        # 编号
                        if len(resolvent) > 1:
                            clause_labels[resolvent] = {}
                            for idx, lit in enumerate(resolvent):
                                clause_labels[resolvent][lit] = chr(97 + idx)
                        
                        resolvent_str = format_clause(resolvent)
                        steps.append(f"{k} R[{clause1_id},{clause2_id}]{mgu_str} = {resolvent_str}")
                        new_resolvents.append(resolvent)
                        k += 1
        
        #不产生新子句，返回结果
        if not new_resolvents:
            return steps
        
        # 扩展旧子句集
        clauses.extend(new_resolvents)

def extract_parents(step):
    #从归结步骤中提取父子句编号
    if "R[" not in step:
        return None, None
    
    # 提取R[]内的内容
    relation_part = step[step.index("R[") + 2:step.index("]")]
    parents = relation_part.split(',')
    
    # 提取数字部分
    parent1 = int(''.join(c for c in parents[0] if c.isdigit()))
    parent2 = int(''.join(c for c in parents[1] if c.isdigit()))
    
    # 提取字母后缀
    parent1_suffix = ''.join(c for c in parents[0] if c.isalpha())
    parent2_suffix = ''.join(c for c in parents[1] if c.isalpha())
    
    return parent1, parent2, parent1_suffix, parent2_suffix

def get_step_number(step): #获取编号
    return int(step.split(' ')[0])

def Simplify(steps, original_size): #简化归结过程--把又臭又长的过程删减成有用的过程
    base_process = steps[0:original_size]  # 初始子句集
    useful_steps = []  # 有用子句集
    
    # 创建编号到索引的映射
    number_to_index = {}
    for i, step in enumerate(steps):
        number = get_step_number(step)
        number_to_index[number] = i
    
    # 从空子句开始，队列中存放需要处理的子句编号
    number = [get_step_number(steps[-1])]  # 空子句的编号
    processed = set()  # 已处理的子句编号
    
    while number:
        number0 = number.pop(0)  # 提取队列首元素
        if number0 in processed:  # 避免处理已处理的子句
            continue
            
        processed.add(number0)
        step_index = number_to_index[number0]
        step = steps[step_index]
        
        if step_index >= original_size:  # 非原始子句才加入useful_steps
            useful_steps.append(step)
            
        # 获取父子句编号
        parent_info = extract_parents(step)
        if parent_info[0] is not None:
            num1, num2 = parent_info[0], parent_info[1]
            
            # 如果不是初始子句，加入队列
            if num1 > original_size and num1 not in processed:
                number.append(num1)
            if num2 > original_size and num2 not in processed:
                number.append(num2)
    
    # 结果需要反转--回溯
    useful_steps.reverse()
    
    # 得到新的归结过程：原始子句 + 有用子句
    final_steps = base_process + useful_steps
    
    # 创建新旧编号的映射
    old_to_new = {}
    for i, step in enumerate(final_steps):
        old_num = get_step_number(step)
        new_num = i + 1
        old_to_new[old_num] = new_num
    
    # 将归结过程重新编号
    for i in range(original_size, len(final_steps)):
        step = final_steps[i]
        parent_info = extract_parents(step)
        
        if parent_info[0] is not None:
            old_num1, old_num2 = parent_info[0], parent_info[1]
            suffix1, suffix2 = parent_info[2], parent_info[3]
            
            # 获取新编号
            new_num1 = old_to_new[old_num1]
            new_num2 = old_to_new[old_num2]
            
            # 构造新的引用字符串
            old_ref = f"R[{old_num1}{suffix1},{old_num2}{suffix2}]"
            new_ref = f"R[{new_num1}{suffix1},{new_num2}{suffix2}]"
            
            # 替换引用
            final_steps[i] = final_steps[i].replace(old_ref, new_ref)
        
        # 更新步骤编号
        old_step_num = get_step_number(final_steps[i])
        new_step_num = i + 1
        if old_step_num != new_step_num:
            final_steps[i] = str(new_step_num) + final_steps[i][len(str(old_step_num)):]
    
    return final_steps