用python写代码，【 问 题 描 述 】 命 题 演 算 公 式 是 指 由 逻 辑 变 量 (其 值 为 真 或 假 )和 逻 辑 运 算 符 ∧ (and)、 ∨ (or) 和  (NOT)按 一 定 规 则 (蕴 涵 等 运 算 可 使 用 ∧ 、 ∨ 等 )组 成 的 公 式 并以 表 示 )。 公 式 运 算 的 顺 序 是  ， ∧ ， ∨ ， 括 号 ()可 以 改 变 优 先 级 。 给 定 一 个 命 题 演 算 公 式 和 每 个 变 量 的 值 ， 需 要 设 计 一 个 程 序 来 计 算 公 式 的 真 值 。 【 基 本 要 求 】 (1)使 用 二 叉 树 计 算 公 式 的 真 值 。 首 先 ， 利 用 堆 栈 将 公 式 的 中 缀 形 式 改 为 后 缀 形 式 。 其 次 ， 根 据 后 缀 形 式 ， 从 叶 节 点 构 造 相 应 的 二 叉 树 。 最 后 ， 按 后 序 遍 历 二 叉 树 ， 找 出 每 个 子 树 的 值 。 也 就 是 说 ， 每 到 达 一 个 节 点 ， 其 子 树 的 值 就 已 经 计 算 出 来 了 。 当 到 达 根 节 点 时 ， 就 得 到 了 公 式 的 真 值 。 (2)设 计 多 种 不 同 形 式 的 命 题 演 算 公 式 ， 并 检 查 每 个 命 题 演 算 公 式 的 有 效 性

以下是使用二叉树计算逻辑公式的Python代码：

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

def build_expression_tree(expression):
    stack = []
    for char in expression:
        if char == ' ':
            continue
        elif char == '(':
            stack.append(char)
        elif char == ')':
            while stack[-1] != '(':
                right = stack.pop()
                op = stack.pop()
                left = stack.pop()
                node = Node(op)
                node.left = left
                node.right = right
                stack.append(node)
            stack.pop()
        elif char in ['&', '|', '!']:
            stack.append(char)
        else:
            node = Node(char)
            stack.append(node)
    while len(stack) > 1:
        right = stack.pop()
        op = stack.pop()
        left = stack.pop()
        node = Node(op)
        node.left = left
        node.right = right
        stack.append(node)
    return stack[0]

def evaluate(root, variables):
    if root.val in ['&', '|']:
        left_val = evaluate(root.left, variables)
        right_val = evaluate(root.right, variables)
        if root.val == '&':
            return left_val and right_val
        else:
            return left_val or right_val
    elif root.val == '!':
        return not evaluate(root.right, variables)
    else:
        return variables[root.val]

expression = "(a & b) | (!a & c)"
variables = {'a': True, 'b': False, 'c': True}
root = build_expression_tree(expression)
print(evaluate(root, variables)) # Output: True

该代码实现了将中缀形式的逻辑公式转换为后缀形式，并根据后缀形式构建二叉树。在计算逻辑公式的真值时，可利用后序遍历二叉树的方式，递归计算每个子树的值，并根据当前节点的运算符计算当前子树的值。最终得到逻辑公式的真值。

要检查不同形式的逻辑公式的有效性，可以使用类似于上述代码中的方法，先将公式转换为二叉树，然后检查是否满足逻辑上的要求。例如，可以检查是否存在未定义的变量、是否存在语法错误、是否存在无效的逻辑运算等。