命题演算公式是指由逻辑变量组成的公式 （其值为TRUE或FALSE）和逻辑运算符∧（and）、∧（or）和 Ø （NOT）根据某些规则（诸如蕴涵之类的运算可以使用∧，∧ 以及表示）。公式运算的顺序是，∧，∧和括号 （）可以更改优先级。给定一个命题演算公式和每个公式的值 变量，则需要设计一个程序来计算公式的真值。 【基本要求】 利用python语言完成程序，使用二叉树来计算公式的真值。 首先，使用堆栈将公式的中缀形式更改为后缀形式。 其次，根据后缀形式，从 叶节点。最后，按后序遍历二叉树，并找到 每个子树。也就是说，每次到达一个节点时，其子树的值已经 计算当到达根节点时，获得公式的真值。最终需要的是完成python代码

以下是基于二叉树的命题演算公式计算的Python代码实现：

class Node:
    def __init__(self, value):
        self.left = None
        self.right = None
        self.value = value

def isOperator(c):
    if (c == 'AND' or c == 'OR' or c == 'NOT'):
        return True
    else:
        return False

def constructTree(postfix):
    stack = []
    
    for char in postfix:
        if not isOperator(char):
            node = Node(char)
            stack.append(node)
        else:
            node = Node(char)
            if char == 'NOT':
                node.right = stack.pop()
            else:
                node.right = stack.pop()
                node.left = stack.pop()
            stack.append(node)
            
    return stack.pop()

def evaluate(root, values):
    if root is None:
        return False
    
    if root.left is None and root.right is None:
        return values[root.value]
    
    leftValue = evaluate(root.left, values)
    rightValue = evaluate(root.right, values)
    
    if root.value == 'AND':
        return leftValue and rightValue
    elif root.value == 'OR':
        return leftValue or rightValue
    elif root.value == 'NOT':
        return not rightValue
    
def postfixConversion(infix):
    postfix = []
    stack = []
    
    priorities = {'AND': 2, 'OR': 1, 'NOT': 3}
    
    for char in infix:
        if not isOperator(char):
            postfix.append(char)
        else:
            while len(stack) != 0 and priorities[char] < priorities[stack[-1]]:
                postfix.append(stack.pop())
            stack.append(char)
    
    while len(stack) != 0:
        postfix.append(stack.pop())
        
    return postfix

infix = input("Enter the propositional formula: ")
postfix = postfixConversion(infix)
root = constructTree(postfix)

values = {}
for char in infix:
    if not isOperator(char) and char not in values:
        value = input("Enter the value of " + char + ": ")
        values[char] = value.lower() == 'true'

print("The value of the propositional formula is: ", evaluate(root, values))

这个程序首先将中缀表达式转换为后缀表达式，然后使用后缀表达式构造二叉树。接下来，程序计算每个变量的值，并将其存储在一个字典中。最后，程序计算整个命题演算公式的值，并输出结果。