Propositional logic (also called propositional calculus, sentential calculus, or sentential logic, 명제 논리) is the branch of mathematical logic concerned with the study of propositions (whether they are true or false) and formed by other propositions with the use of logical connectives, and how their value depends on the truth value of their components. (http://en.wikipedia.org/wiki/Propositional_calculus)

# Table of Contents

# Summary #

**Proposition** - a sentence that can be either true or false

- x is grater than y
- Noam wrote this letter

**Formulas** - grammar of well-formed propositional formulas

- Formula := prop | (! Formula) | (Formula o Formula)

**Assignments** - A truth-values assignment

**Model** of a formula

- If the value of the formula X holds 1 for the assignment A, then the assignment A is called model for formula X.
- That means, all assignments for which the formula X is true are models of it.

**Satisfiable formulas**

- If there exist at least one model of a formula then the formula is called satisfiable.
- The value of the formula is true for at least one assignment. If plays no rule how many models the formula has.

**Valid formulas**

- A formula is called valid (or tautology) if all assignments are models of this formula.
- The value of the formula is true for all assignments. If a tautology is part of a more complex formula then you could replace it by the value 1.

**Inference rules**

- Logical inference is used to create new sentences that logically follow from a given set of sentences (KB)
- Deriving conclusions from premises
- Premises - An assumption that something is true

**Rules for Inference**

**Entailment: KB |= Q**

- Q is entailed by KB (a set of premises or assumptions) if and only if there is no logically possible model in which Q is false while all the premises in KB are true
- Q is entailed by KB if and only if the conclustion is true in every logically possible model in which all the premises in KB are true.

**Derivation: KB |- Q**

- We can derive Q from KB if ther is a proof consisting of a sequence of valid inference steps starting from the premises in KB and resulting in Q

**Soundness: If KB |- Q then KB |= Q**

- IF Q is derived fro ma set of sentences KB using a given set of rules of inference, then Q is entailed by KB.
- Hence, inference produces only real entailments, or any sentence that follows deductively from the premises is valid.

**Completness: If KB |= Q then KB |- Q**

- If Q is entailed by a set of sentences KB, then Q can be derived from KB using the rules of inference.
- Hence, inference produces all entailments, or all valid sentences can be proved from the premises.

# Example code (python) #

```
#!python
# connectives
and_ = lambda p, q: p and q
or_ = lambda p, q: p or q
not_ = lambda p: not p
implies_ = lambda p, q: 0 if (p and p != q) else 1
equivalent_ = lambda p, q: implies_(p, q) and implies_(q, p)
assignments = {
'A': (0, 0),
'B': (0, 1),
'C': (1, 0),
'D': (1, 1),
}
satisfiable_formula = lambda f: any(
f(*assignment) for assignment in assignments.values())
valid_formula = lambda f: all(
f(*assignment) for assignment in assignments.values())
def check(f1, f2):
for name, (p, q) in assignments.items():
for r in (0, 1):
if f1(p, q, r) != f2(p, q, r):
return False
return True
# {p ⇒ q ∨ r} |= (p ⇒ r)
check(lambda p, q, r: implies_(p, and_(q, r)),
lambda p, q, r: implies_(p, r))
# {p ⇒ r} |= (p ⇒ q ∨ r)
check(lambda p, q, r: implies_(p, r),
lambda p, q, r: implies_(p, or_(q, r)))
# {q ⇒ r} |= (p ⇒ q ∨ r)
check(lambda p, q, r: implies_(q, r),
lambda p, q, r: implies_(p, or_(q, r)))
# {p ⇒ q ∨ r, p ⇒ r} |= (q ⇒ r)
check(lambda p, q, r: implies_(p, or_(q, r)),
lambda p, q, r: implies_(q, r))
# {p ⇒ q ∨ r, q ⇒ r} |= (p ⇒ r)
check(lambda p, q, r: implies_(p, or_(q, r)),
lambda p, q, r: implies_(p, r))
```

# 참고자료 #

- SymPy's logic: SymPy에 관련 심볼릭 계산 기능이 내장됨
- Propositional logic for Python 3

# Incoming Links #

## Related Codes (Code 0) #

# Suggested Pages #

- 0.025 LaTeX
- 0.025 Calculs
- 0.025 Python
- 0.025 PeerJ Computer Science
- 0.025 Computer algebra system
- 0.025
- 0.025 January 2
- 0.025
- 0.013 mrjob
- 0.013 Salsa
- More suggestions...