Propositional logic, also known as sentential logic or zeroth-order logic, is a formal system in which the basic units are whole propositions that are either true or false, combined using logical connectives such as conjunction, disjunction, negation, implication, and biconditional. It studies the truth-functional behaviour of compound statements and provides the foundation on which richer logics, including predicate logic, are built. Its decidability and clear semantics make it central to circuit design, satisfiability solving, and automated reasoning.
Overview
- Atomic propositions are assigned truth values, and connectives define how the truth of compounds depends on their parts.
- Truth tables give a complete, mechanical method for evaluating any propositional formula.
- The satisfiability problem (SAT) — deciding whether an assignment makes a formula true — is the canonical NP-complete problem.
- Normal forms such as conjunctive and disjunctive normal form provide canonical representations for reasoning and solving.
Key aspects
- Connectives — conjunction, disjunction, negation, implication, and biconditional define truth-functional composition.
- Truth tables — exhaustive enumeration of truth values establishes validity, satisfiability, and entailment.
- Decidability — propositional validity is decidable, unlike full first-order logic.
- Normal forms — CNF and DNF support resolution and DPLL-style search.
- Entailment and proof — natural deduction and resolution derive consequences from premises.
Applications
- Digital circuit design and Boolean function minimisation.
- SAT and SMT solvers for verification, planning, and configuration.
- Rule evaluation in business logic and policy engines.
- Teaching the foundations of formal reasoning and proof.