English
Logic is the discipline of making the rules of valid reasoning precise. An argument is valid when its conclusion follows necessarily from its premises, and logic provides the formal systems in which “follows necessarily” has an exact definition rather than an intuitive one. A formal proof is a sequence of steps, each licensed by an explicit inference rule, leading from premises to conclusion — a certificate of validity that can be checked mechanically without requiring insight or judgment. The machinery that makes proof checking mechanical is the same machinery that underlies type systems, program verification, query evaluation, and automated reasoning. Logic did not become important to computer science by accident: computation and formal reasoning are, at a deep level, the same activity viewed from different angles.
The subject divides naturally into three overlapping traditions. Proof theory studies the structure of proofs themselves — what inference rules are, how they compose, what transformations preserve validity. Model theory studies the structures that logical sentences describe — what it means for a sentence to be true in a structure, and what the relationship is between syntactic provability and semantic truth. Computational logic studies the algorithmic properties of logical systems — which formulas are decidable, what resources decision procedures require, and how logical reasoning can be automated. Each tradition produces its own results, and serious work in any CS application of logic typically draws from all three.
Logic sits at the base of the Theory Axis. Type theory (§3.5) is logic with computational content: the Curry-Howard correspondence establishes that types are propositions and programs are proofs. Formal methods (§3.6) apply logical systems to specify and verify software and hardware. Programming language semantics (§3.4) uses logical frameworks to define what programs mean. Category theory (§3.7) provides an alternative foundation that subsumes logic as a special case. Understanding logic first is not strictly required to use these tools, but it is required to understand why they work.
Prerequisites: Discrete mathematics and proof (§2.2) — induction, proof techniques, and familiarity with formal argument. Theory of computation (§3.2) can be read in parallel; the two subjects illuminate each other.
How Formal Reasoning Became a Branch of Computer Science
Logic is ancient, but mathematical logic — the treatment of reasoning as a mathematical object that can be studied with the same rigor as geometry or arithmetic — is not. Aristotle’s syllogistic, the dominant logical framework for two millennia, specified valid argument patterns in natural language without attempting to formalize what “valid” meant or to derive completeness results. The modern discipline begins with Gottlob Frege’s Begriffsschrift in 1879, which introduced a formal notation for predicate logic — quantifiers, variables, a complete set of inference rules — and used it to attempt the rigorous derivation of arithmetic from purely logical axioms. Frege’s project failed: Bertrand Russell showed in 1901 that the comprehension principle Frege used to form sets led to a contradiction (the set of all sets that do not contain themselves). But the failure was more productive than most successes. It precipitated a foundational crisis in mathematics that drove a generation of mathematicians and logicians to examine the assumptions underlying formal reasoning with unprecedented precision.
The response took two forms. David Hilbert’s formalist program proposed to resolve the crisis by axiomatizing all of mathematics in a formal system and proving, within that system, that the axioms were consistent. If the formal system could prove its own consistency, no hidden contradiction could emerge to undermine the structure. Hilbert believed this was achievable; he spent the 1910s and 1920s developing proof theory — the mathematical study of formal proofs — as the foundation for the program. Alongside Hilbert, Bertrand Russell and Alfred North Whitehead were constructing Principia Mathematica (1910–1913), an attempt to derive all of mathematics from a carefully restricted set theory that avoided Russell’s paradox.
Both programs were interrupted by Kurt Gödel’s incompleteness theorems in 1931. The first theorem showed that any consistent formal system powerful enough to express basic arithmetic contains statements that are true but unprovable within the system. The second showed that such a system cannot prove its own consistency. Hilbert’s program was not merely incomplete — it was impossible in principle. The theorems established something that had not been suspected: the limits of formal systems are not contingent on our cleverness but are structural features of sufficiently powerful formal reasoning. Gödel also proved the completeness theorem for first-order logic in 1929, showing that every valid first-order sentence has a proof — but the incompleteness results revealed that completeness has precise limits when systems are strong enough to describe arithmetic.
The connection to computation arrived through Alonzo Church and Alan Turing in 1936. Church had been developing lambda calculus as a formal model of computation; Turing independently invented Turing machines. Both were attempting to make precise what it meant for a function to be “effectively computable” — definable by a procedure that a human could in principle execute. The convergence of their approaches produced the Church-Turing thesis: the two models define the same class of functions, and this class captures computational effectiveness in general. The immediate application was to Hilbert’s Entscheidungsproblem — the question of whether there is a mechanical procedure for deciding whether any given first-order sentence is valid. Church and Turing proved independently that no such procedure exists: first-order logic is undecidable. The proof technique was diagonalization, the same technique Cantor had used to show that the real numbers are uncountable and that Gödel had used in the incompleteness theorems. The connection between logic and computation was not metaphorical but structural: undecidability in logic and non-computability in computation are the same phenomenon described in different languages.
The post-war decades brought the computational perspective into the center of logic research. John Robinson’s resolution principle in 1965 gave the first practical automated theorem-proving algorithm for first-order logic, reducing proof search to systematic application of a single inference rule. The insight was that refutation — deriving a contradiction from the negation of the claim — could be mechanized more efficiently than direct proof. Resolution became the basis of logic programming: Prolog, designed by Alain Colmerauer and implemented by him with Robert Kowalski’s theoretical input in the early 1970s, allowed programs to be written as logical axioms and executed by theorem proving. A Prolog program is a set of Horn clauses — implications of the form “if A and B and C then D” — and running the program is resolving queries against the clause database. Prolog never achieved the commercial dominance its advocates expected, but it demonstrated that logic and programming were not merely analogous but literally the same activity from different perspectives.
The development that most directly shaped contemporary CS was SAT solving. Boolean satisfiability — deciding whether a propositional formula can be made true by some assignment of truth values to variables — is the prototypical NP-complete problem: Cook’s 1971 proof established NP-completeness precisely by showing that every problem in NP reduces to SAT in polynomial time. The apparent practical consequence was that SAT was intractable in general. But the DPLL algorithm (Davis, Putnam, Logemann, Loveland, 1962) had already shown that SAT could be solved efficiently in practice for many instances, and through the 1990s and 2000s, industrial-strength SAT solvers improved to the point where formulas with millions of variables — corresponding to full hardware circuits — became solvable routinely. Conflict-Driven Clause Learning (CDCL), developed through the late 1990s, is the core algorithmic advance: when the solver reaches a contradiction, it analyzes the conflict, learns a new clause that prevents revisiting the same dead end, and backtracks non-chronologically. Modern SAT solvers (MiniSat, CryptoMiniSat, Kissat) run the DPLL search with CDCL and sophisticated heuristics for variable ordering; they have transformed formal verification from a research curiosity into an industrial tool.
SMT (Satisfiability Modulo Theories) solvers extended SAT to richer logical languages by integrating propositional SAT solving with decision procedures for specific theories — linear arithmetic, arrays, bit vectors, uninterpreted functions. Z3 (de Moura and Björner, Microsoft Research, 2008) and CVC5 became the workhorses of program verification: when a verifier reduces the correctness of a program to a logical formula in a combination of theories, an SMT solver determines whether the formula is satisfiable. The combination of SAT and SMT techniques has made automated logical reasoning practical at a scale that would have seemed implausible two decades ago.
The most recent development is the integration of neural and symbolic reasoning. Language models have demonstrated surprising capability in informal mathematical reasoning; formal proof assistants have accumulated large libraries of machine-checked proofs; and the intersection is active research: using language models to suggest proof steps (Lean Copilot, Hypertree Proof Search), training models on formal proof corpora, and attempting to close the gap between the informal mathematical reasoning that appears in papers and the formal reasoning that proof assistants require. Whether this integration will produce systems capable of genuine mathematical discovery or only pattern-matching over formal notation is an open question — but the question is live, and progress has been faster than expected.
Three Problems That Organize the Field
Expressiveness and Its Costs
The central design decision for any logical system is what it can express, because expressiveness determines both what the system is useful for and what its computational properties are. The tradeoff is stark: more expressive systems can describe more situations, but their decision problems are typically harder or entirely undecidable.
Propositional logic is the simplest case. A propositional formula is built from atomic variables and the connectives ∧, ∨, ¬, →. Every formula has a truth value — true or false — under any assignment of true/false to its variables, and satisfiability asks whether any assignment makes the formula true. Satisfiability is decidable (just enumerate assignments) and is NP-complete (no known algorithm is better than exponential in the worst case). Despite its simplicity, propositional logic encodes an enormous range of problems: hardware circuit satisfiability, bounded model checking of hardware and software, planning, scheduling, and cryptanalysis all reduce to SAT. The practical utility of propositional logic is enormous precisely because the NP-completeness that seemed to make it hard turned out to be compatible with efficient solving for the instances that arise in practice.
First-order logic adds variables ranging over a domain, quantifiers ∀ and ∃, predicate symbols, and function symbols. This extension makes it possible to express most working mathematics: the axioms of arithmetic, the axioms of groups, the relational properties used in database queries. First-order logic is complete — every valid sentence has a proof — and sound — everything provable is valid. But it is undecidable: no algorithm can determine whether an arbitrary first-order sentence is valid. This is not an accident but a theorem with a specific proof: the halting problem reduces to validity of first-order sentences, so any algorithm for validity would solve the halting problem. The undecidability is the price of expressiveness.
Fragments of first-order logic recover decidability. The universal-existential fragment (Bernays-Schönfinkel-Ramsey class) is decidable. The two-variable fragment is decidable. Monadic first-order logic is decidable. Database query evaluation — the problem of determining whether a first-order query is satisfied by a finite structure — is decidable and, for restricted query classes, efficiently so. Description logics are decidable fragments specifically designed for knowledge representation, with decision procedures ranging from polynomial to double-exponential time depending on the expressiveness of the fragment.
Modal logic extends propositional logic with operators □ (“necessarily”) and ◇ (“possibly”), interpreted over possible-worlds semantics: □φ is true at a world w if φ is true at all worlds accessible from w. Different accessibility relations produce different modal logics — the major systems (K, T, S4, S5) correspond to different constraints on accessibility. Temporal logics (LTL, CTL, CTL*) restrict modal operators to temporal meanings — “always in the future,” “eventually,” “until” — and are the primary logical framework for specifying and verifying concurrent systems. Model checking, the algorithmic problem of determining whether a finite-state system satisfies a temporal logic specification, is decidable and in practice efficient: Clarke, Emerson, and Sifakis received the Turing Award in 2007 for their foundational contributions. The key insight is that for finite-state systems and temporal specifications in appropriate fragments, the model checking problem has polynomial-time algorithms — making automated verification of real systems practical.
Higher-order logic allows quantification over predicates and functions themselves. Second-order logic, which allows quantification over predicates (but not over functions of predicates), is far more expressive than first-order: it can characterize the natural numbers categorically (up to isomorphism), define transitive closure, and express many properties that first-order logic cannot. But this expressiveness comes with the cost of incompleteness: no sound and complete proof system exists for second-order logic. Higher-order logic — the basis of proof assistants like HOL Light, HOL4, and Isabelle — is used in practice by restricting to a well-behaved type-theoretic version that sacrifices some expressive power to gain decidability of type-checking.
Proof Theory: What Proofs Are and What They Reveal
Proof theory studies proofs as mathematical objects — sequences of syntactic manipulations governed by inference rules — rather than as informal arguments. The discipline originates with Gentzen’s introduction of natural deduction and the sequent calculus in 1935, both of which formalize the structure of mathematical proofs in ways that enable their analysis.
The sequent calculus represents proof states as sequents Γ ⊢ Δ, meaning “from assumptions Γ, conclude some formula in Δ.” Inference rules manipulate sequents. Gentzen’s cut elimination theorem — the central result of proof theory — says that any proof using the cut rule (which allows using an intermediate conclusion) can be transformed into a cut-free proof. The theorem has two consequences. Syntactically, it shows that every proof can be normalized to one with a particular structure (the subformula property: every formula in the proof is a subformula of the conclusion or assumptions). Semantically, it implies consistency: if we can prove both φ and ¬φ, cut elimination gives a proof of any formula, which is impossible in a cut-free proof of a reasonable logic. Cut elimination is also a computational procedure: cuts correspond to function calls, and eliminating cuts corresponds to reducing function calls to their definitions — the first example of the correspondence between proof transformations and computation that the Curry-Howard isomorphism makes precise.
Natural deduction, Gentzen’s other proof system, represents proofs in a style that matches informal mathematical reasoning more closely. Each connective has introduction rules (for proving it) and elimination rules (for using it). The harmony between introduction and elimination rules — roughly, that eliminating a formula you just introduced returns you to where you started — is the proof-theoretic expression of the meaning of each connective. This harmony is the foundation of the Curry-Howard correspondence: in the simply typed lambda calculus, introduction rules correspond to function abstraction, elimination rules correspond to function application, and proof normalization corresponds to beta reduction.
Substructural logics arise when the structural rules of the sequent calculus — weakening (unused assumptions can be discarded), contraction (assumptions can be duplicated), and exchange (the order of assumptions is irrelevant) — are restricted or modified. Linear logic, introduced by Jean-Yves Girard in 1987, eliminates weakening and contraction, requiring every assumption to be used exactly once. This makes linear logic a logic of resources: formulas represent resources that are consumed when used. The distinction between classical logic’s “A implies B” and linear logic’s “A implies B (consuming A)” is the distinction between using a fact and using a physical resource. Linear logic has found applications in type systems (Rust’s ownership types are informal linear types), in concurrent programming (session types for communication protocols model the two-channel nature of linear negation), and in database updates (where treating updates as resource consumption prevents aliasing errors).
The Relationship Between Logic and Computation
The Curry-Howard correspondence — also called the propositions-as-types correspondence — is the central insight connecting logic and computation. In its basic form: propositions are types, proofs are programs, and proof normalization is computation. The correspondence is not an analogy but an identity: the same formal systems, described in different vocabularies.
In the simply typed lambda calculus, the typing judgment Γ ⊢ t : τ says that term t has type τ under context Γ. Under Curry-Howard, this is the same as the logical judgment that proposition τ is provable from assumptions Γ, with t as the proof. Abstraction (λx.t) corresponds to implication introduction; application (t u) corresponds to modus ponens. The reduction of λ-expressions (beta reduction) corresponds to cut elimination. Normalization of terms corresponds to normalization of proofs.
The correspondence extends to richer logics and type systems. System F (Girard, Reynolds, independently 1970s) corresponds to second-order propositional logic. Dependent type theory (Martin-Löf, 1972 onward) corresponds to intuitionistic first-order logic. The Calculus of Constructions (Coquand and Huet, 1988) corresponds to the higher-order intuitionistic logic, and is the basis of the Coq proof assistant. The extended Curry-Howard correspondence makes proof assistants programming languages and programming languages proof systems: writing a program in Agda is writing a constructive proof, and verifying a theorem in Lean is writing a certified program.
Computational complexity has logical characterizations that run parallel to Curry-Howard. First-order logic over ordered structures with a successor function characterizes exactly the problems computable in nondeterministic linear time. Horn clause logic characterizes P. The polynomial hierarchy has logical characterizations through the alternation of first-order quantifiers over finite structures. This descriptive complexity program (Fagin, Immerman, and others) shows that complexity classes, usually defined computationally, have purely logical definitions — a different kind of connection between logic and computation, one about the resources that reasoning requires.
What Studying This Changes
Logic in computer science produces several capacities that no other single subject provides.
The first is the ability to read formal systems as objects of study. Type systems, programming language semantics, database query languages, protocol specifications, hardware designs — all are formal systems, and a practitioner trained in logic can analyze them using standard logical tools: asking about their expressiveness, their decision problems, their completeness and soundness, their metatheoretic properties. This is a transferable analytical capability that applies whenever a new formal notation is encountered.
The second is precision in reasoning. Logic teaches, by extended practice, what it means for an argument to be valid: what makes each step legitimate, where hidden assumptions are, when an apparently intuitive inference is actually invalid. This precision is professionally useful in a field that produces formal artifacts — proofs, specifications, type systems, protocols — whose correctness depends on the validity of the reasoning that produced them.
The third is the concrete knowledge of what formal reasoning cannot do. The undecidability of first-order logic, Gödel’s incompleteness theorems, Rice’s theorem for program properties — these are not merely philosophical curiosities but practical constraints. A practitioner who understands them knows when they are searching for something that provably does not exist, and can redirect effort toward what is achievable.
The fourth is access to the tools. SAT solvers, SMT solvers, model checkers, and proof assistants are among the most powerful tools for ensuring correctness in software and hardware. Using them well requires understanding the logical systems they implement: what theories an SMT solver supports and why their combination is decidable, what class of specifications a model checker can handle, what proof obligations a dependent type system generates. The tools are more usable, and their failures more diagnosable, when the logical foundations are understood.
Resources
Books and Texts
The standard CS-oriented entry is Huth and Ryan’s Logic in Computer Science: Modelling and Reasoning about Systems (2nd ed., 2004). It covers propositional logic, first-order logic, model checking, modal and temporal logics, and binary decision diagrams — all oriented toward CS applications rather than toward mathematical logic as an end in itself. The model checking chapters are particularly good: they develop the theory and practice of temporal logic model checking with more care than most texts. For most learners coming to logic from CS, Huth-Ryan is the right starting point and a text to return to throughout the rest of the Theory Axis.
For the mathematical foundations — completeness, compactness, Löwenheim-Skolem, the model theory of first-order logic — Enderton’s A Mathematical Introduction to Logic (2nd ed., 2001) is the standard rigorous treatment. It is more demanding than Huth-Ryan and presupposes mathematical sophistication, but its proofs are careful and complete, and it is the right text for learners who want to understand why the theorems hold rather than just what they say. Van Dalen’s Logic and Structure (5th ed., 2013) covers similar material with more attention to the connections between logic and computation and is a natural companion.
forall x: Calgary (free, Open Logic Project) is a gentler open introduction to formal logic, with truth-functional logic, first-order logic with identity, natural deduction, soundness, and some modal logic. It is not as CS-oriented as Huth-Ryan, but it is useful for readers who need more practice translating informal reasoning into formal syntax and proof before moving to model checking, SMT, or proof assistants. Peter Smith’s Logic: A Study Guide (free at logicmatters.net) is not itself a textbook but an unusually useful route map through logic resources; it belongs as a reference for self-learners planning a longer path.
For proof theory specifically — natural deduction, sequent calculi, Gentzen’s cut elimination theorem, the structural analysis of proofs — Troelstra and Schwichtenberg’s Basic Proof Theory (2nd ed., 2000) is the canonical reference. It is demanding and requires fluency with first-order logic and lambda calculus, but it is the foundation for understanding type theory and proof assistants at depth. Negri and von Plato’s Structural Proof Theory (2001) is a more accessible companion.
For modal and temporal logic, Blackburn, de Rijke, and Venema’s Modal Logic (2001) is the comprehensive contemporary treatment of modal logic from a computational perspective. The book develops possible-worlds semantics, correspondence theory, and the algorithmic properties of modal systems with unusual depth. Demri, Goranko, and Lange’s Temporal Logics in Computer Science (2016) covers temporal logic specifically, including LTL, CTL, CTL*, and their model checking algorithms.
For automated reasoning and SAT/SMT, Bradley and Manna’s The Calculus of Computation (2007) is the most accessible rigorous treatment of the decision procedures underlying SAT and SMT solving. It covers propositional logic, equality with uninterpreted functions, arithmetic, arrays, and the combination of theories (Nelson-Oppen). Kroening and Strichman’s Decision Procedures: An Algorithmic Point of View (2nd ed., 2016) covers similar material with more algorithmic detail. For SAT solving specifically, the Handbook of Satisfiability (Biere et al., 2nd ed., 2021) is the comprehensive reference.
For learners who want the philosophical and historical context alongside the technical content, Smullyan’s puzzle books — What Is the Name of This Book? and Forever Undecided — develop logical concepts through problems and riddles in a way that reveals aspects of the material that standard texts do not. Hofstadter’s Gödel, Escher, Bach (1979) examines the connections between logic, computation, music, and art through an extended dialogue; it is heterodox but formative for many practitioners. Franzén’s Gödel’s Theorem: An Incomplete Guide to Its Use and Abuse (2005) is the essential corrective for anyone who wants to understand what the incompleteness theorems actually establish — and what they do not.
| Book | Role | Type |
|---|---|---|
| Huth & Ryan, Logic in Computer Science (2nd ed.) | Standard CS-oriented entry | Entry |
| Enderton, A Mathematical Introduction to Logic (2nd ed.) | Mathematical foundations; completeness | Depth |
| van Dalen, Logic and Structure (5th ed.) | Alternative mathematical entry | Entry |
| forall x: Calgary (free) | Gentle open formal logic entry | Auxiliary |
| Smith, Logic: A Study Guide (free) | Self-study route map through logic | Reference |
| Troelstra & Schwichtenberg, Basic Proof Theory (2nd ed.) | Proof theory canonical reference | Reference |
| Blackburn, de Rijke & Venema, Modal Logic | Modal logic comprehensive treatment | Depth |
| Demri, Goranko & Lange, Temporal Logics in Computer Science | Temporal logic for CS | Depth |
| Bradley & Manna, The Calculus of Computation | Decision procedures; SAT/SMT foundations | Depth |
| Kroening & Strichman, Decision Procedures (2nd ed.) | SAT/SMT algorithmic treatment | Depth |
| Biere et al., Handbook of Satisfiability (2nd ed.) | SAT comprehensive reference | Reference |
| Smullyan, What Is the Name of This Book? | Logical puzzles; heterodox entry | Auxiliary |
| Hofstadter, Gödel, Escher, Bach | Cross-disciplinary context | Auxiliary |
| Franzén, Gödel’s Theorem: An Incomplete Guide | Incompleteness theorems correctly | Auxiliary |
Courses and Lectures
Stanford’s CS 157 (Computational Logic, materials available online) covers propositional and first-order logic with automated reasoning, including SAT solving and resolution. Genesereth’s treatment connects logic to AI applications more directly than most formal logic courses.
MIT 6.045/18.404 (Theory of Computation, free on MIT OCW) covers computability and complexity with substantial logical content. The overlap with §3.2 is significant, and studying both subjects in parallel produces better understanding of each than studying them sequentially.
The Lean 4 tutorials (Mathematics in Lean, Theorem Proving in Lean 4, free at leanprover-community.github.io) provide hands-on experience with formal proof that textbook study cannot replicate. Working through even the early tutorials makes the connection between proof theory and computation concrete in a way that abstract description cannot. Similarly for Coq (Software Foundations, Pierce et al., free at softwarefoundations.cis.upenn.edu) — the first volume introduces Coq while simultaneously teaching logic and programming language theory through it.
OPLSS (Oregon Programming Languages Summer School, free lectures on YouTube) covers topics at the intersection of logic and programming languages annually. The archived lectures by Frank Pfenning on proof theory and type theory are particularly worth watching.
| Course | Platform | Type |
|---|---|---|
| Stanford CS 157 Computational Logic (free) | Stanford / course site | Entry |
| MIT 6.045 / 18.404 Theory of Computation (free) | MIT OCW | Entry |
| Theorem Proving in Lean 4 (free) | leanprover-community.github.io | Practice |
| Software Foundations Vol. 1 in Coq (free) | softwarefoundations.cis.upenn.edu | Practice |
| OPLSS lectures — Pfenning on proof theory (free) | YouTube / OPLSS site | Depth |
Practice, Tools, and Current Sources
Working with a SAT solver directly is the most effective way to develop intuition for the expressiveness-tractability tradeoff. MiniSat is small enough to read the source code and understand the CDCL algorithm. Z3 (available via Python API as z3-solver) is the most widely used SMT solver and can be used interactively through its Python bindings — encoding problems as SMT formulas and querying Z3 for satisfiability or counterexamples takes hours to learn and produces immediate results for verification problems. cvc5 is the other important modern SMT solver to try after Z3; comparing the same examples across solvers teaches what belongs to SMT-LIB and what belongs to a particular solver’s interface. SAT/SMT by Example (free online) is a practical bridge from textbook decision procedures to executable solver encodings.
The TPTP World is the standard problem library and infrastructure for automated theorem proving. It is not a beginner tutorial, but it is the right reference once a reader wants to see how first-order theorem provers are evaluated, how benchmark problems are represented, and how automated reasoning research organizes shared test cases.
The Stanford Encyclopedia of Philosophy entries on classical logic, model theory, proof theory, modal logic, linear logic, and Gödel’s incompleteness theorems are consistently high-quality and provide orienting context that textbooks often assume.
Model checking tools — Alloy (Jackson, MIT) for relational logic, SPIN for temporal logic of concurrent systems, NuSMV for CTL/LTL model checking — make formal specification and automated verification accessible. Alloy in particular has an unusually shallow learning curve: Jackson’s Software Abstractions (2nd ed.) teaches the tool and the underlying logic simultaneously, and the Alloy Analyzer provides immediate feedback on specifications.
| Resource | Platform | Type |
|---|---|---|
| Z3 Python API (free) | pip install z3-solver | Practice |
| cvc5 SMT solver (free) | cvc5.github.io | Practice |
| MiniSat source (free) | GitHub | Practice |
| SAT/SMT by Example (free) | smt.st | Practice |
| TPTP World (free) | tptp.org | Reference |
| Alloy Analyzer + Software Abstractions (free) | alloytools.org | Practice |
| Stanford Encyclopedia of Philosophy — logic entries (free) | plato.stanford.edu | Reference |
| SPIN model checker (free) | spinroot.com | Practice |
Traps
| Trap | Why it misleads | Better response |
|---|---|---|
| Treating propositional logic as trivial preparation | Propositional logic is the entry point, but practitioners who rush through it miss substantial depth: the NP-completeness of SAT, CDCL solving, the connections to circuit complexity, the proof systems for propositional logic, and the role of propositional encoding in formal verification. A practitioner with only superficial propositional logic cannot understand how modern SAT solvers work or why they are so powerful. | Take propositional logic seriously as a subject in its own right. Implement the DPLL algorithm from scratch. Read the original Cook and Karp papers. Understand why the NP-completeness that seemed to make SAT intractable turned out to be compatible with practical solving. |
| Treating first-order logic as universal | First-order logic is the workhorse of mathematical logic and covers most of mathematics, but it cannot express transitive closure, quantify over predicates, or directly state temporal properties. Many CS applications require logics beyond first-order, and a practitioner who knows only first-order logic will reach for it inappropriately. | Study at least one major non-first-order logic: temporal logic if working with concurrent systems, modal logic for knowledge representation or protocol specification, higher-order logic if working with proof assistants. The habit of asking “what logic is appropriate for this problem?” is the goal. |
| Confusing model theory with proof theory | The model-theoretic perspective (what structures satisfy a formula) and the proof-theoretic perspective (what can be derived from axioms using inference rules) are complementary but distinct. The completeness theorem is the connection between them, and understanding it requires holding both perspectives simultaneously. Learners who know only one perspective encounter significant gaps when they engage with the other. | Study both Huth-Ryan (proof-theoretic emphasis) and Enderton or van Dalen (model-theoretic emphasis). Read and understand the statement and proof of the completeness theorem — the statement is model-theoretic, the proof is constructive and proof-theoretic. |
| Misappropriating Gödel | The incompleteness theorems are among the most frequently misunderstood results in mathematics. They do not say that “truth transcends proof,” that “human reason exceeds formal systems,” or that “mathematics is fundamentally incomplete.” They say that specific formal systems satisfying specific conditions have specific limitations. The philosophical conclusions that popular accounts draw from them go far beyond what the theorems establish. | Read Franzén’s Gödel’s Theorem: An Incomplete Guide to Its Use and Abuse alongside any treatment of the incompleteness theorems. Know the precise statements: which systems, which conditions, which conclusions follow and which do not. |
| Learning logic without using the tools | Logic is one of the subjects where the gap between knowing the theory and using the tools is largest. A practitioner who has read Huth-Ryan but has never encoded a specification in a model checker, never used Z3 to discharge a verification condition, and never written a proof in Lean has not connected the theory to practice in the way that produces real competence. | Work through at least one tool in each category: a SAT/SMT solver (Z3), a model checker (Alloy or SPIN), and a proof assistant (Lean or Coq). The Software Foundations series provides a structured path through Coq; Jackson’s Software Abstractions provides a structured path through Alloy. |
| Skipping linear logic as too abstract | Linear logic looks like a theoretical curiosity until you encounter Rust’s borrow checker, session types for communication protocols, or effect systems for resource management — all of which are informal implementations of linear logic ideas. The subject is more practically relevant than its reputation suggests and will become more so as type systems continue incorporating linear and substructural ideas. | Read at least an introductory treatment of linear logic — Girard’s original 1987 paper is short and readable, or Troelstra’s Lectures on Linear Logic. Then read about Rust’s ownership and borrowing from a type-theoretic perspective to see linear logic in production. |
中文
逻辑是使有效推理规则变得精确的学科。当一个论证的结论必然从其前提推出时，这个论证就是有效的；逻辑提供形式系统，使“必然推出”拥有精确定义，而不是只停留在直觉层面。形式证明是一串步骤，每一步都由明确的推理规则授权，从前提通向结论——它是一张有效性证书，可以被机械检查，而不需要洞见或判断。使证明检查能够机械化的机制，也正是类型系统、程序验证、查询求值和自动推理背后的机制。逻辑之所以对计算机科学重要，并不是偶然的：计算与形式推理在深层上是同一种活动，只是从不同角度观看。
这个主题自然分为三个相互重叠的传统。证明论研究证明本身的结构——推理规则是什么，它们如何组合，哪些变换能够保持有效性。模型论研究逻辑句子所描述的结构——一个句子在一个结构中为真意味着什么，以及句法可证性与语义真理之间是什么关系。计算逻辑研究逻辑系统的算法性质——哪些公式是可判定的，判定过程需要什么资源，以及逻辑推理如何被自动化。每个传统都会产生自己的结果；而计算机科学中任何严肃的逻辑应用，通常都会同时借用这三者。
逻辑位于理论轴的基础处。类型论（§3.5）是带有计算内容的逻辑：Curry-Howard 对应建立了类型就是命题、程序就是证明。形式化方法（§3.6）把逻辑系统用于规定和验证软件与硬件。编程语言语义（§3.4）使用逻辑框架定义程序意味着什么。范畴论（§3.7）提供另一种基础，并把逻辑作为特殊情形纳入其中。先理解逻辑，并不是使用这些工具的严格前提；但如果要理解它们为什么有效，逻辑就是必要的。
前置知识：离散数学与证明（§2.2）——归纳、证明技术，以及对形式论证的熟悉。计算理论（§3.2）可以并行阅读；这两个主题会彼此照亮。
形式推理如何成为计算机科学的一支
逻辑很古老，但数理逻辑——把推理视为一种可以像几何或算术那样被严格研究的数学对象——并不古老。亚里士多德的三段论在两千年中一直是主导逻辑框架；它用自然语言规定有效论证模式，却没有试图形式化“有效”是什么意思，也没有推导完备性结果。现代学科始于 Gottlob Frege 1879 年的 Begriffsschrift。这部作品引入了谓词逻辑的形式记号——量词、变量、一套完整推理规则——并试图用它从纯逻辑公理严格推导算术。Frege 的项目失败了：Bertrand Russell 在 1901 年指出，Frege 用来构造集合的概括原则会导致矛盾，也就是所有不包含自身的集合所组成的集合。可是，这次失败比大多数成功更有生产力。它引发了数学基础危机，推动一代数学家和逻辑学家以前所未有的精确性审视形式推理背后的假设。
回应采取了两种形式。David Hilbert 的形式主义纲领提出，通过把全部数学公理化为一个形式系统，并在该系统内部证明这些公理一致，来解决这场危机。如果形式系统能够证明自身一致，就不会有隐藏矛盾出现并破坏整个结构。Hilbert 相信这是可以做到的；他在 1910 年代和 1920 年代发展证明论——对形式证明的数学研究——作为该纲领的基础。与此同时，Bertrand Russell 和 Alfred North Whitehead 正在构造 Principia Mathematica（1910–1913），试图从一套经过严格限制、能够避免 Russell 悖论的集合论中推导全部数学。
这两个纲领都被 Kurt Gödel 1931 年的不完备性定理打断。第一定理表明，任何足够表达基本算术的一致形式系统，都包含在该系统内部为真但不可证明的命题。第二定理表明，这样的系统无法证明自身一致。Hilbert 的纲领不只是没有完成——它在原则上不可能完成。这些定理确立了一件此前未被怀疑的事情：形式系统的极限并不取决于我们是否足够聪明，而是足够强大的形式推理所具有的结构性特征。Gödel 还在 1929 年证明了一阶逻辑的完备性定理，表明每个有效的一阶句子都有证明；但不完备性结果揭示出，当系统强到足以描述算术时，完备性具有精确边界。
与计算的连接来自 1936 年的 Alonzo Church 和 Alan Turing。Church 一直在发展 λ 演算，作为计算的形式模型；Turing 则独立发明了图灵机。二者都试图精确说明一个函数“有效可计算”是什么意思——也就是可以由人原则上执行的一套程序来定义。两种方法的汇合产生了 Church-Turing 论题：这两个模型定义了同一类函数，而这类函数捕捉了一般意义上的计算有效性。直接应用对象是 Hilbert 的 Entscheidungsproblem，即是否存在一种机械过程，可以判断任意给定一阶句子是否有效。Church 和 Turing 独立证明了这种过程不存在：一阶逻辑是不可判定的。证明技术是对角线法，也就是 Cantor 用来证明实数不可数、Gödel 用于不完备性定理的同一种技术。逻辑与计算之间的联系不是隐喻性的，而是结构性的：逻辑中的不可判定性和计算中的不可计算性，是同一现象在不同语言中的描述。
战后几十年，计算视角进入逻辑研究中心。John Robinson 1965 年提出的归结原则，给出了一阶逻辑中第一个实用的自动定理证明算法，把证明搜索化约为系统应用一条推理规则。其洞见在于，反证——从主张的否定推出矛盾——比直接证明更容易机械化。归结成为逻辑编程的基础：Prolog 由 Alain Colmerauer 设计，并在 1970 年代初由他结合 Robert Kowalski 的理论输入实现，允许程序被写成逻辑公理，并通过定理证明来执行。一个 Prolog 程序是一组 Horn 子句——形式为“如果 A 且 B 且 C，则 D”的蕴含式——运行程序就是用查询对这个子句数据库进行归结。Prolog 从未达到其支持者预期的商业支配地位，但它证明了逻辑与编程不只是相似，而是从不同视角看时同一种活动。
最直接塑造当代计算机科学的发展，是 SAT 求解。布尔可满足性——判断一个命题公式是否存在某种变量真值赋值，使其为真——是原型性的 NP 完全问题：Cook 1971 年的证明，正是通过表明 NP 中每个问题都能在多项式时间内归约到 SAT，从而确立了 NP 完全性。表面上的实践后果是，SAT 一般情况下不可处理。但 DPLL 算法（Davis、Putnam、Logemann、Loveland，1962）早已表明，许多 SAT 实例在实践中可以高效求解。到了 1990 年代和 2000 年代，工业级 SAT 求解器已经进步到可以常规求解包含数百万变量的公式，而这些公式对应完整硬件电路。冲突驱动子句学习（Conflict-Driven Clause Learning，CDCL）是在 1990 年代末发展出的核心算法进展：当求解器遇到矛盾时，它会分析冲突，学习一个新子句，以避免再次走进同一个死胡同，并进行非时间顺序回溯。现代 SAT 求解器（MiniSat、CryptoMiniSat、Kissat）在 DPLL 搜索上加入 CDCL 和复杂变量排序启发式；它们已经把形式验证从研究趣味转变为工业工具。
SMT（Satisfiability Modulo Theories）求解器把 SAT 扩展到更丰富的逻辑语言中，方式是把命题 SAT 求解与特定理论的判定过程整合起来，例如线性算术、数组、位向量、未解释函数。Z3（de Moura 和 Björner，Microsoft Research，2008）以及 CVC5 成为程序验证的主力工具：当验证器把程序正确性化约为一组理论组合中的逻辑公式时，SMT 求解器判断该公式是否可满足。SAT 与 SMT 技术的结合，使自动逻辑推理在二十年前看似难以想象的尺度上变得可行。
最新发展是神经推理与符号推理的整合。语言模型在非形式数学推理中展示了令人意外的能力；形式证明助手积累了大量机器检查证明库；二者交叉处正在成为活跃研究方向：用语言模型建议证明步骤（Lean Copilot、Hypertree Proof Search），在形式证明语料上训练模型，并试图弥合论文中出现的非形式数学推理与证明助手要求的形式推理之间的差距。这种整合是否会产生能够进行真正数学发现的系统，还是只是在形式记号上进行模式匹配，仍然是开放问题——但这个问题已经进入现实议程，而且进展比预期更快。
组织这个领域的三个问题
表达力及其代价
任何逻辑系统的核心设计决策，都是它能够表达什么，因为表达力同时决定了这个系统有什么用，以及它具有什么计算性质。取舍很尖锐：表达力更强的系统能够描述更多情形，但其判定问题通常更难，甚至完全不可判定。
命题逻辑是最简单的情形。一个命题公式由原子变量和连接词 ∧、∨、¬、→ 构成。在任何把变量赋为真或假的赋值下，每个公式都有一个真值——真或假；可满足性问题问的是，是否存在某个赋值使该公式为真。可满足性是可判定的——枚举赋值即可——同时也是 NP 完全的，在最坏情况下没有已知算法优于指数时间。尽管简单，命题逻辑可以编码极大范围的问题：硬件电路可满足性、硬件和软件的有界模型检查、规划、调度、密码分析，都可以归约到 SAT。命题逻辑的实践效用之所以巨大，正是因为原本看似使它困难的 NP 完全性，后来证明与实践中高效求解真实实例并不矛盾。
一阶逻辑加入了在某个论域上取值的变量、量词 ∀ 和 ∃、谓词符号以及函数符号。这一扩展使表达大多数实际数学成为可能：算术公理、群公理、数据库查询中使用的关系性质。一阶逻辑是完备的——每个有效句子都有证明——也是可靠的——所有可证明内容都是有效的。但它是不可判定的：不存在算法能够判断任意一阶句子是否有效。这不是偶然，而是一个有具体证明的定理：停机问题可以归约到一阶句子的有效性，因此任何有效性算法都会解决停机问题。不可判定性就是表达力的代价。
一阶逻辑的片段可以恢复可判定性。全称—存在片段（Bernays-Schönfinkel-Ramsey 类）是可判定的。双变量片段是可判定的。一元一阶逻辑是可判定的。数据库查询求值——判断一个一阶查询是否被某个有限结构满足——是可判定的，而且对于受限查询类可以高效完成。描述逻辑则是专门为知识表示设计的可判定片段，其判定过程从多项式时间到双指数时间不等，取决于片段的表达力。
模态逻辑用算子 □（“必然”）和 ◇（“可能”）扩展命题逻辑，并通过可能世界语义解释：若 φ 在所有可从世界 w 到达的世界中都为真，则 □φ 在 w 为真。不同可达关系产生不同模态逻辑——主要系统（K、T、S4、S5）对应于可达性的不同约束。时序逻辑（LTL、CTL、CTL*）把模态算子限制为时间含义——“未来总是如此”“最终会如此”“直到”——并成为规定和验证并发系统的主要逻辑框架。模型检查，即判断有限状态系统是否满足时序逻辑规范的算法问题，是可判定的，并且在实践中高效：Clarke、Emerson 和 Sifakis 因其奠基性贡献获得 2007 年图灵奖。关键洞见在于，对于有限状态系统和恰当片段中的时序规范，模型检查问题具有多项式时间算法——这使真实系统的自动化验证成为现实。
高阶逻辑允许对谓词和函数本身进行量化。二阶逻辑允许对谓词量化，但不允许对谓词之上的函数量化；它远比一阶逻辑更有表达力：它可以范畴化地刻画自然数（在同构意义下），定义传递闭包，并表达许多一阶逻辑无法表达的性质。但这种表达力带来了不完备性的代价：不存在可靠且完备的二阶逻辑证明系统。高阶逻辑——HOL Light、HOL4 和 Isabelle 等证明助手的基础——在实践中通常通过限制为表现良好的类型论版本来使用，用牺牲部分表达力换取类型检查的可判定性。
证明论：证明是什么，以及它揭示什么
证明论把证明作为数学对象研究——由推理规则支配的一串句法操作——而不是把证明看作非形式论证。这门学科起源于 Gentzen 1935 年引入自然演绎和相继式演算；二者都以可分析的方式形式化了数学证明的结构。
相继式演算把证明状态表示为相继式 Γ ⊢ Δ，意思是“从假设 Γ 可以推出 Δ 中的某个公式”。推理规则操纵相继式。Gentzen 的切消定理——证明论的核心结果——指出，任何使用 cut 规则的证明，也就是允许使用中间结论的证明，都可以被转化为无 cut 证明。这个定理有两个后果。句法上，它表明每个证明都可以被规范化为一种特定结构，也就是子公式性质：证明中的每个公式都是结论或假设的子公式。语义上，它蕴含一致性：如果我们能够同时证明 φ 和 ¬φ，切消会给出任意公式的证明，而这在合理逻辑的无 cut 证明中是不可能的。切消也是一个计算过程：cut 对应函数调用，消除 cut 对应把函数调用化约为其定义——这是证明变换与计算之间对应关系的第一个例子，而 Curry-Howard 同构会把这种关系精确化。
自然演绎是 Gentzen 的另一个证明系统，它以更接近非形式数学推理的方式表示证明。每个连接词都有引入规则（用于证明它）和消去规则（用于使用它）。引入规则与消去规则之间的和谐性——大致说，消去一个你刚刚引入的公式，会把你带回起点——是每个连接词含义的证明论表达。这种和谐性是 Curry-Howard 对应的基础：在简单类型 λ 演算中，引入规则对应函数抽象，消去规则对应函数应用，而证明规范化对应 beta 归约。
当相继式演算中的结构规则——弱化（未使用假设可以丢弃）、收缩（假设可以复制）、交换（假设顺序无关）——被限制或修改时，就产生了子结构逻辑。Jean-Yves Girard 1987 年引入的线性逻辑取消了弱化和收缩，要求每个假设都恰好使用一次。这使线性逻辑成为资源逻辑：公式表示使用时会被消耗的资源。经典逻辑中的 “A 蕴含 B” 与线性逻辑中的 “A 蕴含 B（并消耗 A）” 之间的区别，就是使用一个事实和使用一种物理资源之间的区别。线性逻辑已经在类型系统中找到应用（Rust 的所有权类型是非形式的线性类型），在并发编程中找到应用（通信协议的 session types 模拟线性否定的双通道性质），也在数据库更新中找到应用（把更新视为资源消耗可以防止别名错误）。
逻辑与计算之间的关系
Curry-Howard 对应——也叫“命题即类型”对应——是连接逻辑与计算的核心洞见。它的基本形式是：命题是类型，证明是程序，证明规范化是计算。这种对应不是类比，而是同一性：同一套形式系统，只是用不同词汇描述。
在简单类型 λ 演算中，类型判断 Γ ⊢ t : τ 表示在上下文 Γ 下，项 t 具有类型 τ。在 Curry-Howard 下，这等同于逻辑判断：命题 τ 可以由假设 Γ 证明，而 t 就是这个证明。抽象（λx.t）对应蕴含引入；应用（t u）对应假言推理。λ 表达式的归约（beta 归约）对应切消。项的规范化对应证明的规范化。
这种对应扩展到更丰富的逻辑和类型系统中。System F（Girard 与 Reynolds 在 1970 年代分别独立提出）对应二阶命题逻辑。依赖类型论（Martin-Löf，1972 年起）对应直觉主义一阶逻辑。构造演算（Coquand 和 Huet，1988）对应高阶直觉主义逻辑，并成为 Coq 证明助手的基础。扩展后的 Curry-Howard 对应，使证明助手成为编程语言，也使编程语言成为证明系统：在 Agda 中写程序就是写构造性证明，在 Lean 中验证定理就是写经过认证的程序。
计算复杂性也有与 Curry-Howard 平行的逻辑刻画。带有后继函数的有序结构上的一阶逻辑，恰好刻画非确定性线性时间可计算的问题。Horn 子句逻辑刻画 P。多项式层级可以通过有限结构上一阶量词交替获得逻辑刻画。这个描述复杂性纲领（Fagin、Immerman 等）表明，通常用计算方式定义的复杂性类，也可以拥有纯逻辑定义——这是逻辑与计算之间另一种连接，关乎推理所需资源。
学习这个主题会改变什么
计算机科学中的逻辑，会产生几种没有任何单一其他主题能够提供的能力。
第一，是把形式系统作为研究对象来阅读的能力。类型系统、编程语言语义、数据库查询语言、协议规范、硬件设计——这些都是形式系统。受过逻辑训练的实践者，可以用标准逻辑工具分析它们：询问其表达力、判定问题、完备性和可靠性、元理论性质。每当遇到新的形式记号时，这都是一种可迁移的分析能力。
第二，是推理中的精确性。通过长期练习，逻辑会教会人什么叫一个论证有效：每一步为何合法，隐藏假设在哪里，什么时候看似直觉的推理实际上无效。这种精确性在一个产出形式产物的领域中具有职业用途——证明、规范、类型系统、协议——因为这些产物的正确性取决于产生它们的推理是否有效。
第三，是关于形式推理不能做什么的具体知识。一阶逻辑不可判定性、Gödel 不完备性定理、程序性质的 Rice 定理——这些不只是哲学趣味，而是实践约束。理解它们的实践者知道自己什么时候在寻找一个已经被证明不存在的东西，并能把努力转向可实现的目标。
第四，是进入工具的能力。SAT 求解器、SMT 求解器、模型检查器和证明助手，是确保软件和硬件正确性最强大的工具之一。良好使用它们，需要理解它们实现的逻辑系统：SMT 求解器支持哪些理论，为什么这些理论的组合是可判定的；模型检查器能处理哪类规范；依赖类型系统会生成什么证明义务。当理解其逻辑基础时，这些工具会更易使用，其失败也更容易诊断。
资源
书籍与文本
面向 CS 的标准入口是 Huth 和 Ryan 的 Logic in Computer Science: Modelling and Reasoning about Systems（第 2 版，2004）。它覆盖命题逻辑、一阶逻辑、模型检查、模态与时序逻辑、二叉决策图，并且全部面向 CS 应用，而不是把数理逻辑本身作为目的。模型检查章节尤其好：它比多数教材更仔细地发展了时序逻辑模型检查的理论和实践。对于多数从 CS 进入逻辑的学习者来说，Huth-Ryan 是正确起点，也是整个理论轴后续学习中值得反复回看的文本。
对于数学基础——完备性、紧致性、Löwenheim-Skolem、一阶逻辑模型论——Enderton 的 A Mathematical Introduction to Logic（第 2 版，2001）是标准严格处理。它比 Huth-Ryan 更难，并且预设较高数学成熟度，但其证明仔细而完整；对于想理解定理为什么成立，而不只是知道定理说了什么的学习者，这是合适文本。van Dalen 的 Logic and Structure（第 5 版，2013）覆盖类似材料，但更关注逻辑与计算之间的连接，是自然的配套读物。
forall x: Calgary（免费，Open Logic Project）是对形式逻辑更温和的开放入门，覆盖真值函数逻辑、带等词的一阶逻辑、自然演绎、可靠性，以及一些模态逻辑。它不像 Huth-Ryan 那样面向 CS，但适合那些在进入模型检查、SMT 或证明助手之前，需要更多练习把非形式推理翻译成形式语法和证明的读者。Peter Smith 的 Logic: A Study Guide（logicmatters.net 免费）本身不是教材，但它是一张异常有用的逻辑资源路线图；对于计划长期自学的学习者，它应当作为参考。
专门针对 证明论——自然演绎、相继式演算、Gentzen 的切消定理、证明的结构分析——Troelstra 和 Schwichtenberg 的 Basic Proof Theory（第 2 版，2000）是经典参考。它要求较高，需要熟悉一阶逻辑和 λ 演算，但它是深入理解类型论和证明助手的基础。Negri 和 von Plato 的 Structural Proof Theory（2001）是更易接近的配套读物。
对于 模态逻辑与时序逻辑，Blackburn、de Rijke 和 Venema 的 Modal Logic（2001）是当代关于模态逻辑的综合处理，并且从计算视角展开。该书以异常深度发展可能世界语义、对应理论和模态系统的算法性质。Demri、Goranko 和 Lange 的 Temporal Logics in Computer Science（2016）专门覆盖时序逻辑，包括 LTL、CTL、CTL* 以及相应模型检查算法。
对于 自动推理与 SAT/SMT，Bradley 和 Manna 的 The Calculus of Computation（2007）是对 SAT 和 SMT 求解背后判定过程最易进入的严格处理。它覆盖命题逻辑、带未解释函数的等式、算术、数组，以及理论组合（Nelson-Oppen）。Kroening 和 Strichman 的 Decision Procedures: An Algorithmic Point of View（第 2 版，2016）覆盖类似材料，但有更多算法细节。专门针对 SAT 求解，Handbook of Satisfiability（Biere 等，第 2 版，2021）是综合参考。
对于希望在技术内容之外同时获得哲学和历史语境的学习者，Smullyan 的谜题书——What Is the Name of This Book? 和 Forever Undecided——通过问题和谜题发展逻辑概念，能揭示标准教材通常不会展示的材料侧面。Hofstadter 的 Gödel, Escher, Bach（1979）通过扩展对话考察逻辑、计算、音乐和艺术之间的连接；它不正统，但对许多实践者具有形成性影响。Franzén 的 Gödel’s Theorem: An Incomplete Guide to Its Use and Abuse（2005）则是任何想理解不完备性定理到底确立了什么、没有确立什么的人所需要的关键纠偏。
| 书籍 | 作用 | 类型 |
|---|---|---|
| Huth & Ryan，Logic in Computer Science（第 2 版） | 面向 CS 的标准入口 | 入门 |
| Enderton，A Mathematical Introduction to Logic（第 2 版） | 数学基础；完备性 | 深入 |
| van Dalen，Logic and Structure（第 5 版） | 另一种数学入口 | 入门 |
| forall x: Calgary（免费） | 温和的开放形式逻辑入门 | 辅助 |
| Smith，Logic: A Study Guide（免费） | 逻辑自学路线图 | 参考 |
| Troelstra & Schwichtenberg，Basic Proof Theory（第 2 版） | 证明论经典参考 | 参考 |
| Blackburn、de Rijke & Venema，Modal Logic | 模态逻辑综合处理 | 深入 |
| Demri、Goranko & Lange，Temporal Logics in Computer Science | 面向 CS 的时序逻辑 | 深入 |
| Bradley & Manna，The Calculus of Computation | 判定过程；SAT/SMT 基础 | 深入 |
| Kroening & Strichman，Decision Procedures（第 2 版） | SAT/SMT 的算法处理 | 深入 |
| Biere 等，Handbook of Satisfiability（第 2 版） | SAT 综合参考 | 参考 |
| Smullyan，What Is the Name of This Book? | 逻辑谜题；非正统入口 | 辅助 |
| Hofstadter，Gödel, Escher, Bach | 跨学科语境 | 辅助 |
| Franzén，Gödel’s Theorem: An Incomplete Guide | 正确理解不完备性定理 | 辅助 |
课程与讲座
Stanford CS 157（Computational Logic，材料可在线获取）覆盖命题逻辑和一阶逻辑，并结合自动推理，包括 SAT 求解和归结。Genesereth 的处理比多数形式逻辑课程更直接地把逻辑连接到 AI 应用。
MIT 6.045/18.404（Theory of Computation，MIT OCW 免费）覆盖可计算性和复杂性，并包含大量逻辑内容。它与 §3.2 有显著重叠；并行学习这两个主题，会比顺序学习更好地理解二者。
Lean 4 教程（Mathematics in Lean、Theorem Proving in Lean 4，可在 leanprover-community.github.io 免费获取）提供了形式证明的动手经验，而这是教材学习无法复制的。哪怕只完成早期教程，也会以抽象描述无法做到的方式，把证明论与计算之间的联系具体化。Coq 也是类似路径，特别是 Pierce 等人的 Software Foundations（softwarefoundations.cis.upenn.edu 免费）；第一卷在介绍 Coq 的同时，也通过 Coq 教授逻辑和编程语言理论。
OPLSS（Oregon Programming Languages Summer School，YouTube 上有免费讲座）每年覆盖逻辑与编程语言交叉处的主题。Frank Pfenning 关于证明论和类型论的存档讲座尤其值得观看。
| 课程 | 平台 | 类型 |
|---|---|---|
| Stanford CS 157 Computational Logic（免费） | Stanford / 课程网站 | 入门 |
| MIT 6.045 / 18.404 Theory of Computation（免费） | MIT OCW | 入门 |
| Theorem Proving in Lean 4（免费） | leanprover-community.github.io | 实践 |
| Software Foundations Vol. 1 in Coq（免费） | softwarefoundations.cis.upenn.edu | 实践 |
| OPLSS 讲座——Pfenning 证明论系列（免费） | YouTube / OPLSS 网站 | 深入 |
实践、工具与当前来源
直接使用 SAT 求解器，是培养表达力—可处理性取舍直觉的最有效方式。MiniSat 足够小，可以阅读源码并理解 CDCL 算法。Z3（可以通过 Python API z3-solver 使用）是最广泛使用的 SMT 求解器，可以通过 Python 绑定交互式使用——把问题编码为 SMT 公式，并查询 Z3 是否可满足或是否存在反例，只需要数小时就能上手，并能立刻在验证问题中产生结果。cvc5 是另一个重要的现代 SMT 求解器，适合在 Z3 之后尝试；用同一组例子比较不同求解器，可以教会你什么属于 SMT-LIB，什么属于特定求解器的接口。SAT/SMT by Example（免费在线）是从教材中的判定过程到可执行求解器编码之间的实践桥梁。
TPTP World 是自动定理证明的标准问题库和基础设施。它不是初学者教程，但当读者想了解一阶定理证明器如何被评估、基准问题如何表示、自动推理研究如何组织共享测试用例时，它是正确参考。
Stanford Encyclopedia of Philosophy 中关于经典逻辑、模型论、证明论、模态逻辑、线性逻辑和 Gödel 不完备性定理的条目质量稳定很高，并提供了教材常常预设的定向语境。
模型检查工具——用于关系逻辑的 Alloy（Jackson，MIT）、用于并发系统时序逻辑的 SPIN、用于 CTL/LTL 模型检查的 NuSMV——使形式规约和自动验证变得可接近。Alloy 尤其学习曲线浅：Jackson 的 Software Abstractions（第 2 版）同时教授工具和底层逻辑，而 Alloy Analyzer 会对规约提供即时反馈。
| 资源 | 平台 | 类型 |
|---|---|---|
| Z3 Python API（免费） | pip install z3-solver |
实践 |
| cvc5 SMT solver（免费） | cvc5.github.io | 实践 |
| MiniSat source（免费） | GitHub | 实践 |
| SAT/SMT by Example（免费） | smt.st | 实践 |
| TPTP World（免费） | tptp.org | 参考 |
| Alloy Analyzer + Software Abstractions（免费） | alloytools.org | 实践 |
| Stanford Encyclopedia of Philosophy——逻辑条目（免费） | plato.stanford.edu | 参考 |
| SPIN model checker（免费） | spinroot.com | 实践 |
陷阱
| 陷阱 | 为什么会误导 | 更好的回应 |
|---|---|---|
| 把命题逻辑当作简单预备知识 | 命题逻辑是入口，但急着跳过它的实践者会错过相当深度：SAT 的 NP 完全性、CDCL 求解、与电路复杂性的连接、命题逻辑的证明系统，以及命题编码在形式验证中的作用。只浅层掌握命题逻辑的实践者，无法理解现代 SAT 求解器如何工作，也无法理解它们为什么如此强大。 | 认真把命题逻辑作为独立主题学习。亲自从零实现 DPLL 算法。阅读 Cook 和 Karp 的原始论文。理解为什么原本看似让 SAT 不可处理的 NP 完全性，后来证明仍然可以与实践求解能力共存。 |
| 把一阶逻辑当作万能逻辑 | 一阶逻辑是数理逻辑的主力工具，并能覆盖大多数数学，但它不能表达传递闭包，不能对谓词量化，也不能直接陈述时序性质。许多 CS 应用需要一阶之外的逻辑；只知道一阶逻辑的实践者会不恰当地使用它。 | 至少学习一种主要的非一阶逻辑：如果处理并发系统，学习时序逻辑；如果处理知识表示或协议规范，学习模态逻辑；如果处理证明助手，学习高阶逻辑。目标是养成提问习惯：“这个问题适合哪种逻辑？” |
| 混淆模型论与证明论 | 模型论视角——什么结构满足一个公式——和证明论视角——什么可以由公理通过推理规则推出——是互补但不同的。完备性定理是二者之间的连接；理解它要求同时持有这两个视角。只知道其中一个视角的学习者，在接触另一个视角时会遇到明显缺口。 | 同时学习 Huth-Ryan（偏证明论重点）和 Enderton 或 van Dalen（偏模型论重点）。阅读并理解完备性定理的陈述和证明——其陈述是模型论的，而证明是构造性的、证明论的。 |
| 误用 Gödel | 不完备性定理是数学中最常被误解的结果之一。它们并不表示“真理超越证明”“人类理性超越形式系统”，也不表示“数学在根本上是不完整的”。它们说的是，满足特定条件的特定形式系统具有特定限制。大众化解释从这些定理中推出的哲学结论，远远超出了定理实际确立的内容。 | 在学习不完备性定理时，同时阅读 Franzén 的 Gödel’s Theorem: An Incomplete Guide to Its Use and Abuse。掌握精确陈述：哪些系统、哪些条件、哪些结论成立，哪些并不成立。 |
| 学逻辑却不使用工具 | 逻辑是理论知识与工具使用之间落差最大的主题之一。一个读过 Huth-Ryan，却从未在模型检查器中编码规约、从未用 Z3 证明验证条件、从未在 Lean 中写过证明的实践者，还没有把理论连接到实践；而这种连接正是真正能力产生的地方。 | 每类工具至少实践一个：SAT/SMT 求解器（Z3）、模型检查器（Alloy 或 SPIN）、证明助手（Lean 或 Coq）。Software Foundations 系列提供了通过 Coq 学习的结构化路径；Jackson 的 Software Abstractions 提供了通过 Alloy 学习的结构化路径。 |
| 因为线性逻辑太抽象而跳过它 | 线性逻辑在你遇到 Rust 的借用检查器、通信协议的 session types，或用于资源管理的 effect systems 之前，看起来像理论奇观；但这些都可以视为线性逻辑思想的非形式实现。这个主题比其名声显示的更有实践相关性，而且随着类型系统继续吸收线性和子结构思想，它会变得更相关。 | 至少阅读一份线性逻辑入门处理——Girard 1987 年原始论文短且可读，或 Troelstra 的 Lectures on Linear Logic。然后从类型论视角阅读 Rust 的所有权和借用，以看到生产环境中的线性逻辑。 |