逻辑系统的可靠性和完备性

Whether everything that can be proven with a given inference system is indeed valid (in this case the system is called sound), and whether there exists a proof of validity using the inference system for every valid formula (in this case it is called complete).

基本定义

赋值

Definition 1.1 (assignment). Given a formula φ, an assignment of φ from a domain $D$ is a function mapping φ’s variables to elements of $D$. An assignment to φ is full if all of φ’s variables are assigned, and partial otherwise.

可满足性

Definition 1.2 (satisfiability, validity and contradiction). A formula is satisfiable if there exists an assignment of its variables under which the formula evaluates to true. A formula is a contradiction if it is not satisfiable. A formula is valid (also called a tautology) if it evaluates to true under all assignments.

What does it mean that a formula “evaluates to true” under an assignment? To evaluate a formula, one needs a definition of the semantics of the various functions and predicates in the formula. In propositional logic, for example, the semantics of the propositional connectives is given by truth tables, as presented above. Indeed, given an assignment of all variables in a propositional formula, a truth table can be used for checking whether it satisfies a given formula, or, in other words, whether the given formula evaluates to true under this assignment.

Example. The propositional formula: $A ∧ B$
is satisfiable because there exists an assignment, namely {A → true, B → true}, which makes the formula evaluate to true.

$\alpha \models \phi, \models \phi$

Given a formula φ and an assignment α of its variables, we write α \models φ to denote that α satisfies φ. If a formula φ is valid (and hence, all assignments satisfy it), we write $\models φ$

判断问题

Definition (the decision problem for formulas). The decision problem for a given formula φ is to determine whether φ is valid (under all assignments).

判定过程的可靠性

Definition (soundness of a procedure). A procedure for the decision problem is sound if when it returns “Valid”, the input formula is valid.

判定过程的完备性

**Definition (completeness of a procedure).**A procedure for the decision problem is complete if

• it always terminates, and
• it returns “Valid” when the input formula is valid.

判定过程

Definition (decision procedure). A procedure is called a decision procedure for theory $T$ if it is sound and complete with respect to every formula of $T$.

判定性 decidability

Definition (decidability of a theory). A theory is decidable if and only if there is a decision procedure for it.

公式的基本定义

NNF 范式

Definition (negation normal form (NNF)). A formula is in negation normal form (NNF) if negation is allowed only over atoms, and ∧,∨,¬ are the only allowed Boolean connectives.

For example, ¬(x1 ∨ x2) is not an NNF formula, because the negation is applied to a subformula which is not an atom.

literal

Definition (literal). A literal is either an atom or its negation. We say that a literal is negative if it is a negated atom, and positive otherwise. For example, in the propositional-logic formula
$(a ∨ ¬b) ∧ ¬c$
the set of literals is \{a, ¬b, ¬c\},

Definition (state of a literal under an assignment). A positive literal is satisfied if its atom is assigned true. Similarly, a negative literal is satisfied if its atom is assigned false.

Definition (pure literal). A literal is called pure in a formula φ, if all occurrences of its variable have the same sign.

DNF 范式

Definition 1.16 (disjunctive normal form (DNF)). A formula is in dis- junctive normal form if it is a disjunction of conjunctions of literals, i.e., a formula of the form
$\lor_i(\land_j lij)$
where $lij$ is the $j$-th literal in the $i$-th term (a term is a conjunction of literals). For example:
$(a∧c∧¬b) ∨ (¬a∧d) ∨ (b∧¬c∧¬d) ∨…$

CNF范式

Definition (conjunctive normal form (CNF)). A formula is in conjunctive normal form if it is a conjunction of disjunctions of literals, i.e., it has the form
$\land_i(\lor_j lij)$
where $lij$ is the $j$-th literal in the $i$-th clause (a clause is a disjunction of literals).