预备知识根据合式公式的真值表与主合取范式与主析取范式的关系来求。在命题逻辑中，合式公式的真值表的应用非常广泛。列合式公式真值表的步骤如下：找出合式公式中出现的所有命题变项。按照二进制的顺序给出命题公式的2n种赋值。对每个赋值按照合式公式的层次求出它的值。所有成真赋值的合取即为主合取范式，所有成假赋值的析取即为主析取范式熟悉真值表定义，并列出合式公式的真值表，并根据真值表的结果来判断公式的类型。源程序参考PropostionalLogicHeader头文件/**************************************************************************
* (C) Copyright
All Rights Reserved.
* DISCLAIMER: The authors and publisher shall not be liable in any event *
* for incidental or consequential damages in connection with, or arising *
* out of, the furnishing, performance, or use of these programs.
**************************************************************************/
/* File: PropostionalLogicHeader.h
*-------------------------------
* This interface exports a simple symboll table abstraction
#ifndef _PROPOSTIONALLOGICHEADER_H_
#define _PROPOSTIONALLOGICHEADER_H_
* Constants
*------------------
* LengthMaxLimit
- Length Max
value for the tables
#define LengthMaxLimit 100
/*Private function prototypes*/
* Function: negation
* Usage: negation(p);
*-------------------
* This funtion is an operation that takes a proposition p to another proposition &not p&,
* written ?p, which is interpreted intuitively as being true when p is false and false when p is true.
static int negation(const int p);
* Function: conjunction
* Usage: conjunction(p,q);
* ---------------------------------
* This function is an operation on two logical values, typically the values of two propositions, that
* produces a value of true if and only if both of its operands are true.The conjunctive identity is 1,
* which is to say that AND-ing an expression with 1 will never change the value of the expression. In
* keeping with the concept of vacuous truth, when conjunction is defined as an operator or function of
* arbitrary arity, the empty conjunction (AND-ing over an empty set of operands) is often defined as
* having the result 1.
static int conjunction(const int p,const int q);
* Function: disjunction
* Usage: disjunction(p,q);
*----------------------------------------
* The Function is the values of two propositions, that has a value of false if and only if both of its
* operands are false. More generally, a disjunction is a logical formula that can have one or more literals
* separated only by ORs. A single literal is often considered to be a degenerate disjunction.
* The disjunctive identity is false, which is to say that the or of an expression with false has the same
* value as the original expression. In keeping with the concept of vacuous truth, when disjunction is defined
* as an operator or function of arbitrary arity, the empty disjunction (OR-ing over an empty set of operands)
* is generally defined as false.
static int disjunction(const int p, const int q);
* Function: conditional
* Usage: conditional(p,q)
* ----------------------------------------
* The function is The material conditional is used to form statements of the form &p→q& (termed a conditional
* statement) which is read as &if p then q& and conventionally compared to the English construction &If...
* then...&. But unlike as the English construction may, the conditional statement &p→q& does not specify a
* causal relationship between p and q and is to be understood to mean &if p is true, then q is also true& such
* that the statement &p→q& is false only when p is true and q is false.[1] The material conditional is also to
* be distinguished from logical consequence.
static int conditional(const int p, const int q);
* Function:bicondtional
* Usage: bincontional(p,q)
* ----------------------------------------------
* The function is the logical connective of two statements asserting &p if and only if q&, where q is an
* antecedent and p is a consequent. This is often abbreviated p iff q. The operator is denoted using a
* doubleheaded arrow (), a prefixed E (Epq), an equality sign (=), an equivalence sign (≡), or EQV. It is
* logically equivalent to (p → q) ∧ (q → p), or the XNOR (exclusive nor) boolean operator. It is equivalent to
* &(not p or q) and (not q or p)&. It is also logically equivalent to &(p and q) or (not p and not q)&, meaning
* &both or neither&.
* The only difference from material conditional is the case when the hypothesis is false but the conclusion is
* true. In that case, in the conditional, the result is true, yet in the biconditional the result is false.
* In the conceptual interpretation, a = b means &All a 's are b 's and all b 's are a 's&; in other words, the
* sets a and b coincide: they are identical. This does not mean that the concepts have the same meaning.
* Examples: &triangle& and &trilateral&, &equiangular trilateral& and &equilateral triangle&. The antecedent is
* the subject and the consequent is the predicate of a universal affirmative proposition.
* In the propositional interpretation, a
b means that a impli in other words, that the
* propositions are equivalent, that is to say, either true or false at the same time. This does not mean that
* they have the same meaning. Example: &The triangle ABC has two equal sides&, and &The triangle ABC has two
* equal angles&. The antecedent is the premise or the cause and the consequent is the consequence. When an
* implication is translated by a hypothetical (or conditional) judgment the antecedent is called the hypothesis
* (or the condition) and the consequent is called the thesis.
static int biconditional(const int p, const int q);
* Function:compute
* Usage: compute(p,q ch)
* ----------------------------------
static int compute(const int p, const int q, const char ch);
* Function: is_proposition
* Usage: is_propositon(ch)
* ----------------------------------
static int is_proposition(const char ch);
* Function:is_LogicalConnectives
* Usage: is_LogicalConnectives(c)
* ----------------------------------
static int is_LogicalConnectives(const char c);
* Function:get_isp
* Usage: get_isp(ch)
* ----------------------------------
static int get_isp(const char ch);
* Function:get_icp
* Usage: get_icp(ch)
* ----------------------------------
static int get_icp(const char ch);
* Function:to_InersePolandT
* Usage: to_InersePolandT(*last_exp, *pre_exp)
* -------------------------------------------
static void to_InversePolandT(char *last_exp, const char *pre_exp);
* Function: add_blackets
* Usage: add_blackets(s)
* ----------------------------
static void add_blackets(char* s);
* Function: exp_resolve
* Usage: exp_resolve(*exp,length,(*re_exp)[LengMaxLimit],k)
* ----------------------------
static void exp_resolve(const char* exp, const int length, char (*re_exp)[LengthMaxLimit] , int k);
static void binary_inc(int* a, int length);
* Function: get_proposition
* Usage: get_proposition(*exp,length,*p)
* ------------------------------------------
* The propositions in these logics are more complex. First, terms must be defined. A term is (i) a variable or
* (ii) a function symbol applied to the number of terms required by the function symbol's arity. For example,
* if + is a binary function symbol and x, y, and z are variables, then x+(y+z) is a term, which might be written
* with the symbols in various orders. A proposition is (i) a predicate symbol applied to the number of terms
* required by its arity, (ii) an operator applied to the number of propositions required by its arity, or
* (iii) a quantifier applied to a proposition. For example, if = is a binary predicate symbol and ? is a
* quantifier, then ?x,y,z [(x = y) → (x+z = y+z)] is a proposition. This more complex structure of propositions
* allows these logics to make finer distinctions between inferences, i.e., to have greater expressive power.
* In this context, propositions are also called sentences, statements, statement forms, formulas, and well-formed
* formulas, though these terms are usually not synonymous within a single text. This definition treats propositions
* as syntactic objects, as opposed to semantic or mental objects. That is, propositions in this sense are meaningless,
* formal, abstract objects. They are assigned meaning and truth-values by mappings called interpretations and
* valuations, respectively.
static int get_proposition(const char* exp, const int length, char* p);
static void proposition_ass(const char* pre_exp, int length, char *p, int* v, int n, char* last_exp);
static int bin2dec(int* v, int n);
/* Public function prototyes*/
* Function:is_wellformed
* Usage:is_wellformed(s,length)
* -----------------------------------
* The formulas are inductively defined as follows:
Each propositional variable is, on its own, a formula.
If φ is a formula, then \lnotφ is a formula.
If φ and ψ are formulas, and o is any binary connective, then ( φ o ψ) is a formula.
* Here o could be (but is not limited to) the usual operators ∨, ∧, →, or .
* This definition can also be written as a formal grammar in Backus–Naur form, provided the set
* of variables is finite.
int is_wellformed(const char *s,const int length);
* Function: compute_wellformed
* Usage: compute_wellformed(exp,length)
* -------------------------------------------
int compute_wellformed(const char* exp, const int length);
* Function: truth_table
* Usage: truth_table(exp,length)
* ----------------------------------
* a truth table is composed of one column for each input variable (for example, A and B), and
* one final column for all of the possible results of the logical operation that the table is
* meant to represent (for example, A XOR B). Each row of the truth table therefore contains one
* possible configuration of the input variables (for instance, A=true B=false), and the result of
* the operation for those values. See the examples below for further clarification.
void truth_table(const char* exp, const int length);
int get_main_disjunction(const char* exp, char* resu);
int get_main_conjunction( char* exp, char* resu);
void help();
#endif // end of _PROPOSTIONALLOGICHEADER_H_PropostionalLogicSource源文件/**************************************************************************
* (C) Copyright
All Rights Reserved.
* DISCLAIMER: The authors and publisher shall not be liable in any event *
* for incidental or consequential damages in connection with, or arising *
* out of, the furnishing, performance, or use of these programs.
**************************************************************************/
#include &stdio.h&
#include &stdlib.h&
#include &ctype.h&
#include &string.h&
#include &math.h&
#include &PropostionalLogicHeader.h&
/*Private functions */
//Compute testing
static int compute(const int p, const int q, const char ch){
switch(ch){
return negation(q);
return disjunction(p, q);
return conjunction(p, q);
return conditional(p, q);
return biconditional(p, q);
return -1;
//Negation
static int negation(const int p){
return p == 0 ? 1 : 0;
//Conjunction
static int conjunction(const int p, const int q){
return (p != 0 && q != 0) ? 1 : 0;
//Disjunction
static int disjunction(const int p, const int q){
return (p == 0 && q == 0) ? 0 : 1;
//Conditional
static int conditional(const int p, const int q){
return (p != 0 && q == 0) ? 0 : 1;
//Biconditional
static int biconditional(const int p, const int q){
return ((p == 0 && q == 0) || (p != 0 && q != 0)) ? 1 : 0;
//Whether or not is Propostion?
static int is_proposition(const char ch){
return isalpha(ch) || isalnum(ch);
//Whether or not is Logical Connnectives?
static int is_LogicalConnectives(const char c){
switch(c){
//Stack Priority
static int get_isp(const char ch){
switch(ch){
return -1;
//Stack Priority
static int get_icp(const char ch){
switch(ch)
return -1;
//Inverse Poland Type
static void to_InversePolandT(char* last_exp, const char* pre_exp){
char sign_stack[LengthMaxLimit] = {'\0'};
int sp = -1;
int pp = 0;
int lp = 0;
sign_stack[++sp] = '#';
while(pre_exp[pp] != '\0'){
if(is_proposition(pre_exp[pp])) {
last_exp[lp++] = pre_exp[pp];
while(get_icp(pre_exp[pp]) & get_isp(sign_stack[sp])){
last_exp[lp++] = sign_stack[sp];
sign_stack[sp--] = '\0';
if(get_icp(pre_exp[pp]) == get_isp(sign_stack[sp]))
sign_stack[sp--] = '\0';
sign_stack[++sp] = pre_exp[pp];
while(sp != 0){
last_exp[lp++] = sign_stack[sp--];
static void add_blackets(char* s){
int len = strlen(s);
memcpy(s + 1, s, len);
s[0] = '(';
s[len + 1] = ')';
static void exp_resolve(const char* exp, const int length, char (*re_exp)[LengthMaxLimit] , int k){
char stack[LengthMaxLimit][LengthMaxLimit] = {&\0&};
char rpn_exp[LengthMaxLimit] = &\0&;
char tmp_exp[LengthMaxLimit] = &\0&;
int sp = -1;
int len = 0;
int i = 0;
int j = 0;
to_InversePolandT(rpn_exp, exp);
for(i = 0; i & i++){
if(j & k){
else if(rpn_exp[i] == '~'){
memset(tmp_exp, '\0', sizeof(char) * LengthMaxLimit);
strncpy(tmp_exp, &rpn_exp[i], sizeof(char));
strcpy(tmp_exp + strlen(tmp_exp), stack[sp]);
add_blackets(tmp_exp);
memset(stack[sp], '\0', sizeof(char) * LengthMaxLimit);
strcpy(stack[++sp], tmp_exp);
else if(is_LogicalConnectives(rpn_exp[i])){
memset(tmp_exp, '\0', sizeof(char) * LengthMaxLimit);
strcpy(tmp_exp, stack[sp-1]);
strncpy(tmp_exp + strlen(tmp_exp), &rpn_exp[i], 1);
strcpy(tmp_exp + strlen(tmp_exp), stack[sp]);
add_blackets(tmp_exp);
memset(stack[sp], '\0', sizeof(char) * LengthMaxLimit);
memset(stack[sp - 1], '\0', sizeof(char) *LengthMaxLimit);
strcpy(stack[++sp], tmp_exp);
else if(is_proposition(rpn_exp[i])){
strncpy(stack[++sp], &rpn_exp[i], 1);
strcpy(re_exp[k], tmp_exp);
static void binary_inc(int* a, int length){
int i = 0, c = 0;
a[length - 1] += 1;
for(i = length - 1; i & 0; i--) {
if(a[i] & 1){
a[i - 1] += 1;
static int get_proposition(const char* exp, const int length, char* p){
int i = 0;
int j = 0;
int k = 0;
int n = 0;
for(i = 0; i & i++){
if(is_proposition(exp[i])){
while(p[j] != '\0') {
if(exp[i] == p[j]){
if(k == 0){
p[j] = exp[i];
static void proposition_ass(const char* pre_exp, int length, char *p, int* v, int n, char* last_exp)
int j = 0, k = 0;
for(j = 0; j & j++) {
if(is_proposition(pre_exp[j])){
for(k = 0; k & k++){
if(pre_exp[j] == p[k])
last_exp[j] = v[k] + '0';
last_exp[j] = pre_exp[j];
//Binary to Dec
static int bin2dec(int* v, int n)
int num = 0, i = 0;
for(i = n - 1; i & -1; i--)
if(v[i] == 0)
num += (int)pow(2.0, n - i - 1);
/*Public functions */
// Compute for well formed formula Values
int compute_wellformed(const char* exp, const int length)
if(!is_wellformed(exp, length)){
printf(&The expression is not a well formed\n&);
return -1;
char last_exp[LengthMaxLimit] = {'\0'};
int stack[LengthMaxLimit] = {0};
int lp = 0, sp = -1, r,
for(i = 0; i & i++){
if(isalpha(exp[i])){
printf(&does not assigment&);
return -1;
to_InversePolandT(last_exp, exp);
while(last_exp[lp] != '\0')
if(isalnum(last_exp[lp])){
stack[++sp] = last_exp[lp] - '0';
else if(last_exp[lp] == '~'){
r = compute(0, stack[sp--], last_exp[lp]);
stack[++sp] =
else if(is_LogicalConnectives(last_exp[lp])){
r = compute(stack[sp-1], stack[sp], last_exp[lp]);
stack[++sp] =
return stack[sp];
//Whether or not is well-formed?
int is_wellformed(const char* s, const int length){
int l_bracket = 0;
int r_bracket = 0;
int i = 0;
if(length == 1 && is_proposition(s[i]))
while(i & length){
if(is_proposition(s[i])){
if(!is_LogicalConnectives(s[i + 1]) && s[i + 1] != ')' && s[i + 1] != '\0' || s[i + 1] == '~')
else if(is_LogicalConnectives(s[i])){
if(!is_proposition(s[i + 1]) && s[i + 1] != '~' && s[i + 1] != '(')
else if(s[i] == '(')
if(s[i + 1] != '~' && !is_proposition(s[i + 1]) && s[i + 1] != '(')
l_bracket++;
else if(s[i] == ')')
if(s[i + 1] != '\0' && !is_LogicalConnectives(s[i + 1]) && s[i + 1] != ')' || s[i + 1] == '~')
r_bracket++;
if(l_bracket == r_bracket)
//print truth table
void truth_table(const char* exp, const int length)
if(!is_wellformed(exp, length)) {
printf(&The expression is not a wff\n&);
int i, j, k, r, n = 0, m = 0;
char s[LengthMaxLimit] = &\0&;
char p[LengthMaxLimit] = &\0&;
char ss[LengthMaxLimit][LengthMaxLimit] = {'\0'};
n = get_proposition(exp, length, p);
m = (int)pow(2.0, n);
int* v = new int[m];
memset(v, 0, sizeof(int) * m);
memset(ss, '\0', sizeof(char) * LengthMaxLimit * LengthMaxLimit);
for(i = 0, k = 0; i & i++){
if(is_LogicalConnectives(exp[i])){
exp_resolve(exp, length, ss, k);
for(j = 0; j & j++)
printf(&%c
&, p[j]);//print propostional
for(j = 0; j & j++)
printf(&%s
&, ss[j]);
printf(&\n&);
for(i = 0; i & i++){
for(j = 0; j & j++)
printf(&%d
for(j = 0; j & j++){
memset(s, '\0', sizeof(char) * LengthMaxLimit);
proposition_ass(ss[j], strlen(ss[j]), p, v, n, s);
r = compute_wellformed(s, strlen(s));
printf(&%d
binary_inc(v, n);
printf(&\n&);
//Main Disjunction
int get_main_disjunction(const char* exp, char* resu)
int len = strlen(exp);
if(!is_wellformed(exp, len))
memset(resu, '\0', sizeof(char) * LengthMaxLimit);
char tmp_exp[LengthMaxLimit] = &\0&;
char p[LengthMaxLimit] = &\0&;
int i = 0, r = 0;
int n = get_proposition(exp, len, p);
int m = (int)pow(2.0, n);
int* v = new int[m];
memset(v, 0, sizeof(int) * m);
int r_index = 0;
for(i = 0; i & i++)
proposition_ass(exp, len, p, v, n, tmp_exp);
r = compute_wellformed(tmp_exp, strlen(tmp_exp));
//compute to well-fomred
if(r == 1)
if(r_index - 1 & -1 && resu[r_index - 1] != '\0')
resu[r_index++] = '+';
char strn[10] = &\0&, num = 0;
num = bin2dec(v, n);
resu[r_index++] = 'm';
_itoa(num, strn, 10);
memcpy(resu + r_index, strn, sizeof(char) * strlen(strn));
resu += strlen(strn); //以上几行为添加范式
binary_inc(v, n);
//Main conjunction
int get_main_conjunction( char* exp, char* resu)
int len = strlen(exp);
if(!is_wellformed(exp, len))
memset(resu, '\0', sizeof(char) *LengthMaxLimit);
char tmp_exp[LengthMaxLimit] = &\0&;
char p[LengthMaxLimit] = &\0&;
int i = 0, r = 0;
int n = get_proposition(exp, len, p);
int m = (int)pow(2.0, n);
int* v = new int[m];
memset(v, 0, sizeof(int) * m);
int r_index = 0;
for(i = 0; i & i++)
proposition_ass(exp, len, p, v, n, tmp_exp);
r = compute_wellformed(tmp_exp, strlen(tmp_exp));
if(r == 0)
if(r_index - 1 & -1 && resu[r_index - 1] != '\0')
resu[r_index++] = '*';
char strn[10] = &\0&, num = 0;
num = bin2dec(v, n);
resu[r_index++] = 'M';
_itoa(num, strn, 10);
memcpy(resu + r_index, strn, sizeof(char) * strlen(strn));
resu += strlen(strn);
binary_inc(v, n);
void& help(){
&& &printf(&*********************************************************&);
&& &printf(&\n*\t\t\t\t\t\t\t*&);
&& &printf(&\n*\t\t Welcome to Propostion Set\t\t*&);
&& &printf(&\n*\t\t\t\t\t\t\t*&);
&& &printf(&\n*\t Usage:\t\t\t\t\t\t*&);
&& &printf(&\n*\t\t'~': Negation\t\t\t\t*&);
&& &printf(&\n*\t\t'+': Disjunction\t\t\t\*&);
&& &printf(&\n*\t\t'*': Conjunction\t\t\t*&);
&& &printf(&\n*\t\t'&': Conditional\t\t\t*&);
&& &printf(&\n*\t\t'=': Biconditional\t\t\t*&);
&& &printf(&\n*\t\t'default': -1\t\t\t\t*&);&& &&& &
&& &printf(&\n*\t\t\t\t\t\t\t*&);
&& &printf(&\n*********************************************************&);
printf(&\n&);
}&Main源文件/**************************************************************************
* (C) Copyright
All Rights Reserved.
* DISCLAIMER: The authors and publisher shall not be liable in any event *
* for incidental or consequential damages in connection with, or arising *
* out of, the furnishing, performance, or use of these programs.
**************************************************************************/
#include &stdio.h&
#include &string.h&
#include &PropostionalLogicHeader.h&
/*main program */
int main( ){
char s[100];
int length, r = 0;
while(scanf(&%s&, s) && s[0] != '#'){
length = strlen(s);
printf(&expression is:
%s\n\n&, s);
//Whether or not is well-formed?
printf(&is_wellformed Formula?
%d\n\n&, is_wellformed(s, length));
printf(&compute_wellfomred is: &);
r = compute_wellformed(s, length);
if(r & -1)
printf(&%d&, r);
printf(&\n\n&);
printf(&Print True table\n&);
truth_table(s,length);
char dis_form[LengthMaxLimit];
get_main_disjunction(s, dis_form);
printf(&main disjunction normal form is: %s\n\n&, dis_form);
char con_form[LengthMaxLimit];
get_main_conjunction(s, con_form);
printf(&main conjunction normal form is: %s\n\n&, con_form);
}测试结果界面测试:p蕴含q,然后蕴含r测试: p析取q,然后蕴含r测试:p蕴含q,然后析取r关于更多讨论与交流，敬请关注本博客和新浪微博.
本文已收录于以下专栏：
相关文章推荐
int const MAX = 1e6;
short true_value[MAX]; //真值
short true...
利用真值表法求主析取范式及主析取范式的实现(C++)
功能:用户可输入合式公式（包含！&|以及圆括号），程序即可输出变元真值表及主合取范式及主析取范式
《离散数学》南京邮电大学学习期间，离散数学实...
实验目的和要求
编程实现用真值表法求取任意数量变量的合式公式的主析取范式和主合取范式。
能够列出任意合式公式的真值表并给出相应主析取和主合取范式。
编程实现用...
课本是高等教育出版社出版的《离散数学及其应用》。
程序会自动分析输入的表达式，并且列出真值表，最后打印出主析取范式和主合取范式，最多支持256 个变元。
主要用到的算法：中缀表达式转后缀表达式、后缀表...
这是我们学校离散数学的作业题目，我用JAVA写的，不废话，上代码：package lisanE
import java.io.BufferedR
import jav...
实现功能：输入命题公式的合式公式，求出公式的真值表，并输出该公式的主合取范式和主析取范式。
输入：命题公式的合式公式
输出：公式的主析取范式和主析取范式，输出形式为：“ mi ∨ Mi ∧ ...
离散数学上机实验，给定一个命题公式，求其主析取范式，主合取范式，能力有限，参考了我学长的一篇博客，并进行了许多优化。
本次离散数学实验，我学到了许多东西，也看了自己的不足之处
1).我深刻地体会到在...
本程序可以实现任意输入表达式，变元数最多可为3个，即可输出主析取式和主合取式。
规定符号：
[离散] 编程求命题公式真值表概述
真值表是离散数学中的一个重要概念，由真值表我们能求得任意命题公式的主析取范式和主合取范式。本文将用C语言编写一个求任意命题公式真值表的程序...
针对给定的包含任意个变量的真值表，编程实现用真值表法求取其所对应的主析取范式和主合取范式。
能够掌握通过真值表求取相应主析取和主合取范式的方法及原理。
他的最新文章
讲师：董岩
您举报文章：
举报原因：
原文地址：
原因补充：
(最多只允许输入30个字)