通过编写一个C语言程序，让计算机给出命题公式的真值表，并在此基础上进行命题公式类型的判定、求命题公式的主范式等。

实现这个功能需要对命题逻辑的相关知识有一定的了解。下面是一个简单的实现过程，仅供参考。

1. 首先需要定义命题公式的语法，可以使用巴克斯范式或EBNF等形式定义。例如，可以定义命题变量为大写字母，命题连接词为小写字母，命题公式可以用以下EBNF表示：

<prop> ::= <var> | '(' <prop> <conn> <prop> ')'
<var> ::= 'A' | 'B' | 'C' | ...
<conn> ::= '&' | '|' | '->' | '<->'

其中，`<prop>`表示命题公式，`<var>`表示命题变量，`<conn>`表示命题连接词，`|`表示或，`&`表示与，`->`表示蕴含，`<->`表示等价。

2. 然后需要编写一个函数，将命题公式转换为真值表。可以使用递归方式实现，对每个命题变量进行赋值，计算命题公式的真值。例如，下面是一个简单的伪代码实现：

function truth_table(prop):
    var_list = get_variables(prop)  # 获取命题变量列表
    table = []  # 真值表
    for values in binary_combinations(len(var_list)):
        row = []
        for i in range(len(var_list)):
            set_variable_value(var_list[i], values[i])  # 设置变量值
        row.append(eval_prop(prop))  # 计算命题公式真值
        table.append(row)
    return table

其中，`get_variables(prop)`用于获取命题公式中的所有变量，`binary_combinations(n)`用于生成n位二进制数的所有组合，`set_variable_value(var, value)`用于设置变量的值，`eval_prop(prop)`用于计算命题公式的真值。

3. 接下来可以编写一个函数，判断命题公式的类型。可能的类型包括：永真式、永假式、可满足式、重言式、矛盾式等。例如，下面是一个简单的伪代码实现：

function prop_type(prop):
    table = truth_table(prop)  # 获取真值表
    all_true = True
    all_false = True
    some_true = False
    some_false = False
    for row in table:
        if row[0]:
            all_false = False
            some_true = True
        else:
            all_true = False
            some_false = True
    if all_true:
        return 'Tautology'
    elif all_false:
        return 'Contradiction'
    elif some_true and some_false:
        return 'Contingency'
    elif some_true:
        return 'Satisfiable'
    else:
        return 'Unsatisfiable'

其中，`truth_table(prop)`用于获取命题公式的真值表，`all_true`、`all_false`、`some_true`、`some_false`用于判断真值表的情况，`Tautology`表示永真式，`Contradiction`表示永假式，`Contingency`表示可满足式，`Satisfiable`表示重言式，`Unsatisfiable`表示矛盾式。

4. 最后可以编写一个函数，求出命题公式的主范式。主范式是由所有使命题公式为真的赋值组成的析取范式或合取范式。例如，下面是一个简单的伪代码实现：

function main_formula(prop):
    table = truth_table(prop)  # 获取真值表
    var_list = get_variables(prop)  # 获取变量列表
    minterms = set()
    maxterms = set()
    for i in range(len(table)):
        if table[i][0]:
            minterm = []
            maxterm = []
            for j in range(len(var_list)):
                if binary_combinations(len(var_list))[i][j] == '0':
                    minterm.append(var_list[j] + '\'')
                    maxterm.append(var_list[j])
                else:
                    minterm.append(var_list[j])
                    maxterm.append(var_list[j] + '\'')
            minterms.add(''.join(minterm))
            maxterms.add(''.join(maxterm))
    return '∨'.join(minterms) + '\n' + '∧'.join(maxterms)

其中，`truth_table(prop)`用于获取命题公式的真值表，`get_variables(prop)`用于获取命题公式中的所有变量，`minterms`、`maxterms`用于保存主析取范式和主合取范式，`binary_combinations(len(var_list))[i]`用于获取真值表中的第i行赋值组合，`∨`表示析取，`∧`表示合取。

以上代码仅为伪代码，实际实现需要根据具体语言进行调整。