Logic gives AI a precise language for knowledge and a sound procedure for drawing conclusions from it. A knowledge base (KB) is a set of sentences; inference derives new sentences that are guaranteed true whenever the KB is. This is the formal backbone of rule engines, Prolog and Datalog, ontology reasoners, SAT and SMT solvers used in verification and scheduling, and the policy engines that increasingly sit next to LLM agents.
Part of Knowledge & Reasoning. For reasoning under uncertainty see Bayesian Networks and Fuzzy Logic.
A model is a possible world: an assignment of truth values (or, in first-order logic, a domain plus interpretations). KB ⊨ α (entailment) means α is true in every model where the KB is true. Inference (KB ⊢ α) is the syntactic procedure that tries to establish this. A procedure is sound if it derives only entailed sentences and complete if it can derive all of them. Most practical provers work by refutation: add ¬α to the KB and show that the result has no model.
Propositional logic has atomic symbols (Rain, WetGrass) combined with ¬ ∧ ∨ ⇒ ⇔. Every formula can be converted to conjunctive normal form (CNF): an AND of clauses, each an OR of literals. Deciding whether a CNF formula is satisfiable (SAT) is NP-complete, yet modern CDCL solvers (conflict-driven clause learning, descended from DPLL) routinely handle industrial instances with millions of clauses using unit propagation, clause learning, non-chronological backjumping, restarts and activity-based branching heuristics.
For restricted Horn clauses (at most one positive literal, i.e. rules of the form A ∧ B ⇒ C), forward and backward chaining are sound, complete and run in linear time. That is why rule engines and Datalog stick to Horn-like rules.
First-order logic (FOL) adds objects, predicates, functions and the quantifiers ∀ and ∃, so one sentence can cover infinitely many cases. Inference lifts propositional rules using unification: UNIFY(p, q) returns the most general substitution θ with pθ = qθ, or fails. Generalized modus ponens applies a rule whenever its premises unify with known facts. Prolog implements backward chaining with depth-first search over Horn clauses; Datalog restricts FOL further (no function symbols) so that bottom-up evaluation always terminates, which is why it is used in program analysis, access control and modern query engines.
FOL entailment is only semi-decidable: if KB ⊨ α, a complete prover will eventually say so, but if not it may run forever.
The resolution rule takes two clauses containing complementary literals and produces a clause with the rest: from (A ∨ B) and (¬B ∨ C) infer (A ∨ C). Resolution refutation is complete for CNF: KB entails α exactly when resolving clauses of KB ∧ ¬α can derive the empty clause. In FOL, resolution combined with unification is refutation-complete, and strategies such as unit preference, set-of-support and subsumption keep the clause set from exploding.
from itertools import combinations
def resolve(c1, c2):
out = []
for lit in c1:
neg = lit[1:] if lit.startswith("~") else "~" + lit
if neg in c2:
out.append(frozenset((c1 - {lit}) | (c2 - {neg})))
return out
def entails(kb_clauses, query_lit):
neg = query_lit[1:] if query_lit.startswith("~") else "~" + query_lit
clauses = set(map(frozenset, kb_clauses)) | {frozenset([neg])}
while True:
new = set()
for a, b in combinations(clauses, 2):
for r in resolve(a, b):
if not r:
return True # empty clause: contradiction
new.add(r)
if new <= clauses:
return False # nothing new: not entailed
clauses |= new
kb = [{"~Rain", "WetGrass"}, {"~Sprinkler", "WetGrass"}, {"Rain", "Sprinkler"}]
print(entails(kb, "WetGrass")) # True: either way the grass is wet
print(entails(kb, "Rain")) # False
# Real workloads: an SMT solver (pip install z3-solver)
from z3 import Bools, Solver, Implies, Or, Not, unsat
rain, spr, wet = Bools("rain sprinkler wet")
s = Solver()
s.add(Implies(rain, wet), Implies(spr, wet), Or(rain, spr), Not(wet))
print("entailed" if s.check() == unsat else "not entailed")
The toy prover is exponential; use it to understand the idea. Z3, CVC5, PySAT and Clingo (answer set programming) are what you reach for in practice, for example to verify configurations, check access-control policies, or solve scheduling problems also covered in Constraint Satisfaction.
| Formalism | Decidable? | Typical use |
|---|---|---|
| Horn clauses / Datalog | Yes, polynomial data complexity | Rule engines, program analysis, authorization |
| Propositional (SAT) | Yes, NP-complete | Hardware/software verification, planning, configuration |
| Description logics (OWL) | Yes for OWL DL, varying complexity | Ontologies, classification |
| SMT (SAT + theories) | Depends on theory | Program verification, symbolic execution |
| Full first-order logic | Semi-decidable | Theorem proving, mathematics |
The recurring design choice is to give up expressiveness to get guaranteed, fast answers. Classical logic is also monotonic: adding facts never removes conclusions. Defaults and exceptions need non-monotonic formalisms such as negation as failure (Prolog, answer set programming) or default logic.
A ⇒ B is true whenever A is false.Take three Horn rules — Rain ⇒ WetGrass, Sprinkler ⇒ WetGrass, WetGrass ∧ Cold ⇒ Ice — and the facts Rain and Cold.
Forward chaining is data-driven. Each rule keeps a count of unsatisfied premises; when a fact is added, every rule mentioning it decrements its count, and a rule whose count reaches zero adds its conclusion to the agenda. Here Rain fires the first rule (WetGrass), and WetGrass plus Cold fire the third (Ice). The Sprinkler rule never fires. The process stops at a fixpoint where nothing new can be derived; every atom is processed at most once, which gives the linear running time. This is how production-rule engines (Rete-based systems such as Drools or CLIPS) and bottom-up Datalog evaluation work, and it suits monitoring, where new facts stream in and you want every consequence.
Backward chaining is goal-driven. To prove Ice, find a rule concluding it and recursively prove its premises: WetGrass (try Rain: a fact, done) and Cold (a fact). It touches only rules relevant to the question, which suits diagnosis and question answering. Its weaknesses are repeated subgoals and infinite loops on recursive rules; Prolog's depth-first strategy is not complete for that reason, while tabled evaluation (memoizing subgoals, as in XSB) restores termination for Datalog-style programs.
Resolution and SAT solvers need clauses, so every propositional formula is first converted to CNF with four mechanical steps:
A ⇔ B becomes (A ⇒ B) ∧ (B ⇒ A).A ⇒ B becomes ¬A ∨ B.¬ appears only on atoms.∨ over ∧ until the formula is an AND of ORs.Example: ¬(P ∧ Q) ⇒ R becomes ¬¬(P ∧ Q) ∨ R, then (P ∧ Q) ∨ R, then (P ∨ R) ∧ (Q ∨ R). Distribution can blow formulas up exponentially, so real tools use the Tseitin transformation: introduce a fresh variable for each subformula and add clauses defining it. The result is only equisatisfiable rather than equivalent, but its size is linear, which is all a satisfiability check needs.
In first-order logic two more steps are needed: skolemization replaces each existential variable with a new function of the universally quantified variables in scope (∀x ∃y Loves(x, y) becomes ∀x Loves(x, F(x))), and the remaining universal quantifiers are dropped because all clause variables are implicitly universal. Variables are also renamed apart so that no two clauses share a variable name before unification.
| Setting | How logic is used |
|---|---|
| Hardware and software verification | Bounded model checking encodes "can the system reach a bad state in k steps" as SAT or SMT; symbolic execution asks an SMT solver for inputs that reach a branch. |
| Cloud access policies | Policies are translated to SMT formulas so a solver can prove properties such as "no statement makes this bucket public", or produce a counterexample request. |
| Package managers and configuration | Dependency resolution is NP-complete in general; several package managers encode version constraints for a SAT or ASP solver. |
| Knowledge graphs and ontologies | Description-logic reasoners classify OWL ontologies and check consistency; Datalog rules derive new edges in graph databases. |
| LLM agents | A language model translates a request into a formal query or constraints, a solver or rule engine computes the answer, and the result is checked before acting. The solver supplies guarantees the model cannot. |
The common thread is a division of labor: statistical models handle perception and messy language, while logic handles the parts where a wrong answer must be impossible rather than merely unlikely. See Rule-based Systems and Agents & Tool Use for the surrounding architecture.