Soundness and Completeness
The set of inference rules R is said to be sound, iff Δ ⊢R P implies Δ ⊨ P is set of wffs and P is an wff.
R is said to be complete, iff Δ ⊨ P is such that there exist a. proof of P from Δ using set of inference rules R.
If inference rules, are sound and complete, we can find whether one sentence (wff) follows from Δ. It is done by searching for a proof. Here no need to use truth table.
If inference rules are sound, we can find proof of P from Δ. Here logically follows from Δ.
If inference rules are Complete, we can confirm that P follows from Δ by searching proof using complete search procedure.
NP-hard problem states that it is need to determine whether a P logically follows Δ or can be proved from Δ.
The PSAT Problem
The propositional satisfiability (PSAT) problem is to find a model for a formula which comprises the conjunction of all the wffs in Δ. We have to find out an interpretation which should be satisfiable by all the. wffs of Δ.
A clause is formed by disjunction of literals. A conjunctive normal form (CNF) which is the conjunction of clauses is called formula. It is easy to solve the PSAT problem when it is represented using CNF formulas. The problems such as circuit synthesis, circuit diagnosis and planning, constraint satisfaction are converted to CNF formulas for solution as CNF PSAT problems.
The procedure to solve CNF PSAT problem involves assigning True and False to atoms in the formula, in all of the ways systematically. The interpretation for which all of the clauses have value true is selected. The drawback of this procedure is, we need to check all 2n different assignments (where n is number of atoms). If n value is large, the procedure takes exponential time.
In KSAT problem, we need to find a model for formula which is conjunction of clauses,. the longest of which contains exactly K literals. 2SAT and 3SAT problems are special cases for PSAT problem.
Unlike PSAT problem, GSAT is non-exhaustive and greedy. The procedure to solve GSAT problem is similar to hill climbing search. The procedure start by assigning a random True/False values for all atoms in the formula. We. note down the number of clauses having true value. Next assign another set of True/False values to atoms and note down the number of clauses having true value. The value of the atom which giving largest increase is changed. The process continues upto fixed number of changes.
Other Important Topics
Language Distinctions
An artificial agent uses propositional calculus to describe its world. The agent should not be confused between formal and informal languages used in propositional calculus.
Example: Consider a wff {P, P ⊃ R} ⊢R
Here the symbol ⊢ is not from language of propositional calculus and symbol ⊃ is used in language of propositional calculus. The agent should not be confuse in identifying these symbols.
Metatheorems
The propositional calculus has several theorems which are proved by chaining certain rules of inference. But metatheorems are theorems about the propositional calculus. The most important theorems of metatheorems are,
1) The deduction theorem
2) Reductio ad absurdum
1) Deduction:
If {∝1, ∝2,....∝n}⊨ ∝, vice versa. , then (∝1 ^ ∝2,^....^ ∝n) ⊃ ∝ is valid, and vice versa
2) Reductio ad absurdum:
If there is no interpretation that satisfies all wffs of Δ then Δ ⊨ ∝
Associative Laws
1) If conjunction ^ is associative, then
(∝1 ^ ∝2 ) ^ ∝3 = ∝1 ^ (∝2 ^ ∝3)
Here ∝1, ∝2 , ∝3 are called conjuncts.
2) If disjunction v is associative, then
(∝1 ∨ ∝2 ) ∨ ∝3 = ∝1 ∨ (∝2 ∨ ∝3)
Here ∝1, ∝2 , ∝3 are called disjuncts.
Distributive Laws
∝1 ^ (∝2 ∨ ∝3) = (∝1 ^ ∝2 ) ∨ (∝1 ^ ∝3)
∝1 ∨ (∝2 ^ ∝3) = (∝1 ∨ ∝2 ) ^ (∝1 ∨ ∝3)