Propositional logic #
Find similar titles

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)

Summary
Example code (python)
참고자료
Incoming Links
1. Related Codes (Code 0)
Suggested Pages

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))

Propositional logic #
Find similar titles

Table of Contents

Summary #

Example code (python) #

참고자료 #

Incoming Links #

Related Codes (Code 0) #

Suggested Pages #