English
Logic studies which conclusions follow from given premises. For example, from “every administrator may edit” and “Lin is an administrator,” we can infer “Lin may edit.” The inference uses the stated policy; it does not establish whether that policy is appropriate.
Formal logic separates a statement being true in a model from being derivable in a proof system. A model supplies meanings for symbols—for example, which users count as administrators and which may edit. A proof system supplies permitted inference steps. Soundness ensures that every derivable conclusion is true in every model where its premises are true. Completeness asks whether all semantic consequences can be derived.
In computing, these distinctions appear in type checking, database queries, circuit design, and verification. A solver does not determine whether a requirement is sensible: it answers a formal question about an encoding. Learning logic helps you identify that question and judge what an answer establishes.
Begin with the proof techniques in §2.2, truth tables, and small derivations. Model theory studies interpretations, proof theory studies derivations, and computational logic studies algorithms for reasoning. These perspectives support one another; none requires treating every computation as a mathematical proof.
How Formal Reasoning Became a Branch of Computer Science
Modern mathematical logic emerged through several projects. Boole developed an algebra of logical relations; Frege’s predicate notation made quantification and nested argument structure explicit. Russell’s paradox exposed a contradiction in Frege’s later foundational system. This made restrictions on forming mathematical objects an important part of subsequent foundational work.
Hilbert sought secure foundations through formal axiomatization and finitistic consistency arguments. The intended consistency arguments had their own methodological restrictions. Gödel’s completeness theorem for first-order logic and his 1931 incompleteness theorems answer different questions. The former relates logical validity to derivability. The latter limits consistent, effectively axiomatized theories strong enough to represent arithmetic: they cannot settle every arithmetic sentence, and, under the standard hypotheses, cannot prove their own consistency.
Church and Turing connected such foundational questions to effective computation. Their negative answer to the first-order decision problem did not make mechanized reasoning useless. It distinguished a universal decision procedure, which always finishes with a correct yes or no, from methods that succeed on restricted problems or search for proofs without guaranteed termination.
AI research made proof search a practical design problem. Robinson’s resolution method combined inference with unification; logic programming connected clauses to execution. Prolog’s development involved Colmerauer, Roussel, and Kowalski, and its operational search order matters: logically equivalent descriptions can have different termination behavior. SAT and SMT solving later expanded the practical reach of automated reasoning through specialized representations and search. The development of specialized procedures shows how restrictions on a formal language can make useful reasoning tasks tractable.
Three Problems That Organize the Field
Ask three questions about any formal language: what can it say, how can a claim be justified, and what can an algorithm decide? Their answers need not coincide. A proof can be easy to check yet hard to find, and a complete proof system need not supply a terminating decision procedure.
Expressiveness and Its Costs
Propositional logic combines Boolean variables with connectives. Satisfiability asks whether some assignment makes a formula true; validity asks whether every assignment does. The formula p → q is satisfiable but not valid: p = true, q = false is a counterexample. To prove that p and p → q entail q, ask whether p ∧ (p → q) ∧ ¬q is satisfiable. No assignment can satisfy it: the premises and the negation of the conclusion conflict.
SAT is the propositional satisfiability problem. A SAT solver searches for an assignment or establishes that none exists. In scheduling, a variable can represent whether a job occupies a time slot; clauses rule out conflicting assignments. A satisfying model is then a candidate schedule. This turns a reasoning task into a concrete search with a checkable result.
First-order logic adds quantification over objects and symbols for relations and functions. ∀x (Admin(x) → MayEdit(x)) says that the implication holds for every object in the domain. Its general validity problem is undecidable, although a sound and complete calculus can enumerate proofs of valid sentences. Evaluating a formula in a given finite structure is a different, decidable task: the quantified objects can be enumerated. Asking whether there is some finite model of any size is a different problem again.
Decidable fragments impose specific restrictions. Presburger arithmetic permits addition but not unrestricted multiplication of variables. The Bernays–Schönfinkel–Ramsey fragment allows existential quantifiers followed by universal quantifiers, with relations and constants but no functions taking arguments. Such conditions restrict how formulas can generate or constrain objects. Saying only “fewer quantifiers” does not explain the result.
SMT means satisfiability modulo theories. It combines Boolean reasoning with rules for domains such as integers, arrays, or fixed-width bit vectors. Boolean variables alone treat x > 3 and x < 2 as unrelated atoms; an arithmetic theory explains why both cannot hold for the same integer. Mathematical integers and machine bit vectors differ because the latter have a fixed width and specified overflow behavior. Selecting a theory is therefore a modeling choice as well as an algorithmic one.
Modal logic evaluates statements at worlds connected by an accessibility relation: □P requires P at every accessible world, while ◇P requires it at some accessible world. Different relations can model possibilities, knowledge, or permitted transitions. Temporal logics describe behavior over time: “the lock is never held by two processes” or “a request is eventually served.” Some formulas concern one path, while others quantify over alternative future paths. Section 3.6 develops the distinction through model checking. For an explicitly represented finite transition system, CTL model checking is polynomial in model and formula size; LTL checking is PSPACE-complete in combined complexity. These different costs concern specified languages and tasks, not a general ranking of their usefulness.
Higher-order logic permits quantification over functions and predicates. Its semantic choices affect what completeness can mean: full semantics ranges over all functions of the relevant kind, while Henkin semantics permits suitably restricted function domains. The general completeness result available with Henkin semantics does not extend unchanged to full semantics. The lesson is to name the language, interpretation, and question together.
Proof Theory: What Proofs Are and What They Reveal
Proof theory treats derivations as objects that can be inspected and transformed. In natural deduction, an introduction rule tells us how to establish a connective and an elimination rule tells us how to use it. A proof of A ∧ B supplies both parts; using it to obtain A simply selects the first part. Introducing a pair and immediately selecting its first component is a small example of a removable proof detour.
In a single-conclusion sequent calculus, Γ ⊢ A records that assumptions Γ suffice for conclusion A. A cut uses an intermediate lemma: first derive B, then use B to derive A. Cut elimination shows how, in calculi with that property, the intermediate lemma can be removed by transforming the derivation. This exposes a relationship between the final statement and the formulas needed in its proof, although the transformed proof can be much larger. Gentzen’s work on natural deduction and cut elimination, followed by further normalization results, made such transformations systematic for specified calculi. They help expose which assumptions a proof uses and can support consistency arguments. They do not mean that every theory with arbitrary additional axioms automatically has the same normalization properties.
Structural rules also matter. Ordinary assumptions can typically be reused or ignored. Linear disciplines control duplication and disposal; affine disciplines allow disposal while restricting duplication. This distinction helps explain resource-sensitive programming, but Rust’s ownership and borrowing rules should not be identified wholesale with a single linear logic.
The Relationship Between Logic and Computation
Logical equivalence also supports concrete design changes. For Boolean inputs, (a ∧ b) ∨ (a ∧ c) and a ∧ (b ∨ c) agree on every assignment. If each two-input AND or OR is implemented as one gate, directly translating the first expression uses three gates; translating the second uses two. The distributive law justifies preserving the truth table, while the chosen gate model explains the smaller count. Actual delay and energy still depend on the implementation. This separates two questions that also arise in compiler and database optimization: does a transformation preserve the required result, and does it improve the relevant cost?
Curry–Howard names a family of precise correspondences between specified logics and typed calculi. In a basic constructive setting, a proof of A → B behaves as a function transforming evidence for A into evidence for B. Proof normalization corresponds to evaluating the term. Section 3.5 develops the correspondence and its conditions; an arbitrary program with unrestricted recursion is not automatically a proof of its return type as a proposition.
Automation introduces another distinction: searching for evidence and checking supplied evidence. A tactic or language model may propose a proof, while a small checker verifies the resulting derivation. An SMT solver may instead return satisfiable, unsatisfiable, or unknown for the supported input. Neither fluent text nor a solver timeout supplies a theorem. The logical foundation tells us what artifact must be checked and what assumptions remain.
Descriptive complexity connects logical expressiveness to computational resources over finite structures. Fagin’s theorem characterizes NP using existential second-order descriptions; on finite ordered structures, first-order logic with a least fixed-point operator captures P. A fixed-point construction repeatedly adds consequences until no new ones appear, as in computing graph reachability. These results, described in Immerman’s overview, relate the language used to state a property to the resources needed to decide it. They concern evaluating fixed descriptions on varying structures, a different task from deciding general logical validity.
What Studying This Changes
The practical habit is to separate the statement, its interpretation, and the evidence. Encode a small scheduling constraint as a Boolean formula, find a satisfying assignment, then add a conflicting requirement and explain the contradiction. For an implication, try constructing a countermodel before attempting a proof. These exercises make soundness, satisfiability, and validity usable concepts rather than interchangeable words.
Resources
Books and Texts
Huth and Ryan’s Logic in Computer Science: Modelling and Reasoning about Systems (2nd ed., 2004) connects propositional and first-order logic to verification, model checking, temporal logic, and binary decision diagrams. Its worked specifications make it a useful first text for readers interested in CS applications. Begin with formula translation and small proofs before the model-checking chapters.
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 a useful 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 an 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 a focused account 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, MIT OCW) supplies the computability and complexity background used in §3.2. Its decision-problem and reduction exercises help explain why complete proof systems need not provide decision procedures.
Theorem Proving in Lean 4, Mathematics in Lean, and Software Foundations provide exercises in constructing machine-checked proofs. Choose one environment initially. Follow the versions required by the material; older Coq-based exercises and the renamed Rocq distribution may require different setup instructions.
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
MiniSat provides a compact SAT implementation for studying conflict-driven clause learning. Z3 and cvc5 let you encode constraints over supported theories and inspect models or unsatisfiability results. Begin with a small scheduling problem whose answer you can check by hand, then change one constraint and explain the new result. SAT/SMT by Example provides executable examples; the SMT-LIB format helps separate a formal encoding from a particular solver interface.
The TPTP World is the standard problem library and infrastructure for automated theorem proving. It is not a beginner tutorial, but it is a useful 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.
Alloy explores relational specifications within chosen scopes; SPIN checks concurrent-system models; NuSMV supports symbolic model checking with temporal properties. Jackson’s Software Abstractions teaches Alloy through examples. Record the scope and property with every result, and distinguish the freely available analyzer from the book’s publication format.
| 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 (free) + Software Abstractions (book) | 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 |
|---|---|---|
| Confusing truth with derivability | Truth uses an interpretation; derivability uses rules and axioms. | Specify both and ask which soundness or completeness result relates them. |
| Reading completeness as decidability | Proof enumeration may run forever when no proof exists. | Distinguish checking, searching, and always-terminating decision procedures. |
| Applying incompleteness to every formal system | The theorems have effectiveness, arithmetic-strength, and consistency hypotheses. | State the theory and the precise theorem before drawing a conclusion. |
| Quoting a fragment without its restrictions | Quantifier order, function symbols, and semantics change the problem. | Write the fragment’s definition alongside the decidability claim. |
| Treating a solver answer as validation of intent | The solver reasons about the supplied encoding. | Inspect models, counterexamples, assumptions, and translation boundaries. |
| Calling every typed program a proof | Nontermination and unchecked assumptions change the correspondence. | Identify the calculus and the conditions that make its terms valid evidence. |
中文
逻辑研究给定前提能够推出哪些结论。例如，从“所有管理员都可以编辑”和“Lin 是管理员”，可以推出“Lin 可以编辑”。这个推理使用了给定的权限规则，但没有证明规则本身是否合适。
形式逻辑区分命题在模型中为真，与命题能在证明系统中推出。模型赋予符号含义，例如哪些用户是管理员，哪些用户可以编辑。证明系统规定允许的推理步骤。可靠性保证：在使前提为真的每个模型中，可推导的结论也为真；完备性则追问，所有语义上的推论是否都能被推导。
在计算中，这些区别出现在类型检查、数据库查询、电路设计和验证中。求解器不会判断需求是否合理，而是回答关于某种编码的形式问题。学习逻辑，有助于识别这个问题，并判断答案实际建立了什么。
从 §2.2 的证明技巧、真值表和小型推导开始。模型论研究解释，证明论研究推导，计算逻辑研究推理算法。这些视角相互支持，但并不要求把每一次计算都当成数学证明。
形式推理如何成为计算机科学的一支
现代数理逻辑来自多个研究方向。Boole 发展了逻辑关系的代数，Frege 的谓词记号明确表达了量化与嵌套的论证结构。Russell 悖论揭示了 Frege 后来的基础系统中的矛盾。此后，对数学对象构造规则的限制，成为基础研究的重要内容。
Hilbert 试图通过形式公理化和有穷主义的一致性论证，为数学建立可靠基础。所寻求的一致性论证本身也受到方法上的限制。Gödel 的一阶逻辑完备性定理与 1931 年的不完备性定理回答不同问题。前者连接逻辑有效性与可推导性；后者限制的是一致、可有效公理化、且足以表达算术的理论：它们不能判定每个算术命题，并且在标准前提下，不能证明自身的一致性。
Church 和 Turing 把这些基础问题连接到有效计算。他们对一阶判定问题的否定回答，并没有使机械推理失去用途。它区分了两种事物：总能终止并给出正确是非答案的通用判定程序，以及能解决受限问题、或搜索证明却不保证终止的方法。
AI 研究把证明搜索变成实际的设计问题。Robinson 的归结方法结合推理与合一；逻辑编程把子句连接到执行。Prolog 的发展涉及 Colmerauer、Roussel 和 Kowalski，而且它的操作性搜索顺序很重要：逻辑等价的描述，终止行为可能不同。SAT 与 SMT 求解随后通过专门的表示和搜索方法，扩大了自动推理的实际范围。专门推理过程的发展表明，对形式语言施加限制，可以使有用的推理任务变得可处理。
组织这个领域的三个问题
面对一种形式语言，可以问三个问题：它能表达什么，主张怎样得到论证，算法能够判定什么？答案不必一致。证明可能容易检查却难以找到；完备的证明系统，也不必提供保证终止的判定程序。
表达力及其代价
命题逻辑用连接词组合布尔变量。可满足性问是否存在使公式为真的赋值；有效性问是否每种赋值都使它为真。公式 p → q 可满足，却不是有效式：p = true, q = false 就是反例。要证明 p 和 p → q 蕴涵 q，可以问 p ∧ (p → q) ∧ ¬q 是否可满足。没有赋值能够满足它，因为前提与结论的否定相互冲突。
SAT 是命题可满足性问题。SAT 求解器搜索满足赋值，或建立不存在这种赋值的结论。在调度中，可以用变量表示某项任务是否占用某个时段，用子句排除相互冲突的安排。此时，满足模型就是一个候选时间表。这把推理任务变成了具有可检查结果的具体搜索。
一阶逻辑增加对对象的量化，以及表示关系和函数的符号。∀x (Admin(x) → MayEdit(x)) 表示：对论域中每个对象，这个蕴涵都成立。其一般有效性问题不可判定，但可靠且完备的演算可以枚举有效命题的证明。在给定有限结构中求公式的真值，是另一个可判定任务，因为可以枚举量化对象。询问是否存在某个任意大小的有限模型，又是不同的问题。
可判定片段施加具体限制。Presburger 算术允许加法，不允许变量之间不受限制的乘法。Bernays–Schönfinkel–Ramsey 片段允许先存在、后全称的量词，使用关系和常量，但没有带参数的函数。这些条件限制公式生成或约束对象的方式。只说“量词更少”，不能解释结果。
SMT 指可满足性模理论。它把布尔推理与整数、数组或固定位宽位向量等领域的规则结合起来。只使用布尔变量时，会把 x > 3 与 x < 2 当成无关原子；算术理论则解释为什么同一个整数不能同时满足二者。数学整数不同于机器位向量，后者具有固定宽度与指定的溢出行为。因此，选择理论既是建模选择，也是算法选择。
模态逻辑在通过可达关系连接的世界中评价陈述：□P 要求 P 在每个可达世界中成立，◇P 则要求它在某个可达世界中成立。不同关系可以模拟可能性、知识或允许的转移。时序逻辑描述随时间展开的行为，例如“从不同时有两个进程持有锁”或“请求最终得到处理”。有些公式描述一条路径，另一些则量化可能的未来路径。§3.6 会通过模型检查展开这个区别。对于显式表示的有限转移系统，CTL 模型检查关于模型与公式大小是多项式的；LTL 检查的组合复杂度则为 PSPACE 完全。这些不同成本针对指定语言与任务，并不是对实用性的通用排名。
高阶逻辑允许对函数和谓词量化。语义选择会影响完备性的含义：完全语义覆盖相应种类的所有函数，Henkin 语义则允许适当受限的函数论域。Henkin 语义下的一般完备性结果，不能原样扩展到完全语义。这里应养成的习惯，是同时说明语言、解释与所问问题。
证明论：证明是什么，以及它揭示什么
证明论把推导当作可以检查和变换的对象。在自然演绎中，引入规则说明如何建立某个连接词，消去规则说明如何使用它。A ∧ B 的证明提供两部分；从中得到 A，就是取出第一部分。先构造一对证明、立即取出第一部分，是一个可以消除的证明绕路。
在单结论的相继式演算中，Γ ⊢ A 记录假设 Γ 足以推出结论 A。切规则使用中间引理：先推出 B，再用 B 推出 A。对于具有消切性质的演算，可以变换推导，消去这个中间引理。这显示了最终陈述与证明中所需公式之间的关系，不过变换后的证明可能大得多。Gentzen 关于自然演绎和消切的工作，以及后续的正规化结果，在特定演算中系统化了这些变换。它们有助于看清证明用了哪些前提，也能支持一致性论证。但这不表示任意添加公理后，每一种理论都自动具有同样的正规化性质。
结构规则也很重要。普通假设通常可以重复使用或忽略。线性约束控制复制与丢弃；仿射约束允许丢弃，却限制复制。这个区别有助于理解资源敏感的编程，但不应把 Rust 的所有权和借用规则整体等同于某一种线性逻辑。
逻辑与计算之间的关系
逻辑等价也能支持具体的设计修改。对于布尔输入，(a ∧ b) ∨ (a ∧ c) 与 a ∧ (b ∨ c) 在每种赋值下都相同。若分别用一个双输入逻辑门实现一次 AND 或 OR 运算，直接翻译前式需要三个门，后式需要两个。分配律保证真值表保持不变，选定的门电路模型则解释门数为什么减少。实际延迟与能耗仍取决于实现。这区分了编译器和数据库优化中也会遇到的两个问题：变换是否保持所需结果，以及它是否改善关心的成本。
Curry–Howard 指一组指定逻辑与带类型演算之间的精确对应。在基本的构造性框架中，A → B 的证明类似一个函数：把 A 的证据变成 B 的证据。证明正规化对应项的求值。§3.5 会展开这种对应及其条件；具有不受限制递归的任意程序，并不会自动成为其返回类型所对应命题的证明。
自动化又引入另一种区分：搜索证据与检查已有证据。策略或语言模型可以提出证明，由较小的检查器核验产生的推导。SMT 求解器则可能对支持的输入返回可满足、不可满足或未知。流畅的文字和求解超时都不能提供定理。逻辑基础告诉我们需要检查什么产物，以及还保留哪些假设。
描述复杂性把有限结构上的逻辑表达力连接到计算资源。Fagin 定理用存在二阶描述刻画 NP；在有限有序结构上，带最小不动点算子的一阶逻辑刻画 P。不动点构造反复加入推论，直到不再产生新结果，例如计算图的可达关系。Immerman 的概述介绍了这些结果，它们连接了陈述性质所用的语言与判定性质所需的资源。这里讨论的是在变化的结构上评价固定描述，不同于判定一般逻辑有效性。
学习这个主题会改变什么
实际的习惯是分清陈述、解释与证据。把小型调度约束编码成布尔公式，找到满足赋值，再加入冲突要求并解释矛盾。面对蕴涵，先试着构造反模型，再尝试证明。这些练习使可靠性、可满足性和有效性成为可用的概念，而不是可以互换的词语。
资源
书籍与文本
Huth 与 Ryan 的 Logic in Computer Science: Modelling and Reasoning about Systems（第 2 版，2004）把命题逻辑、一阶逻辑连接到验证、模型检查、时序逻辑和二叉决策图。书中的规约实例使它适合关心 CS 应用的读者作为第一本教材。可以先练习公式翻译和小型证明，再进入模型检查章节。
对于数学基础——完备性、紧致性、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 所用的可计算性与复杂性背景。其中的判定问题和归约练习，有助于理解为什么完备证明系统不一定提供判定过程。
Theorem Proving in Lean 4、Mathematics in Lean 与 Software Foundations 提供构造机器检查证明的练习。起初选择一个环境即可。应采用材料要求的版本；较早的 Coq 练习与更名后的 Rocq 发行版，可能需要不同的配置说明。
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 网站 | 深入 |
实践、工具与当前来源
MiniSat 提供较小的 SAT 实现，可用于研究冲突驱动子句学习。Z3 与 cvc5 允许在所支持的理论中编码约束，并检查模型或不可满足结果。可以从一个能手工核对答案的小型调度问题开始，再改变一项约束，解释新结果。SAT/SMT by Example 提供可执行例子；SMT-LIB 格式有助于区分形式编码与具体求解器接口。
TPTP World 是自动定理证明的标准问题库和基础设施。它不是初学者教程，但当读者想了解一阶定理证明器如何被评估、基准问题如何表示、自动推理研究如何组织共享测试用例时，它是可用参考。
Stanford Encyclopedia of Philosophy 中关于经典逻辑、模型论、证明论、模态逻辑、线性逻辑和 Gödel 不完备性定理的条目质量稳定很高，并提供了教材常常预设的定向语境。
Alloy 在选定范围内探索关系规约，SPIN 检查并发系统模型，NuSMV 支持针对时序性质的符号模型检查。Jackson 的 Software Abstractions 通过例子教授 Alloy。记录结果时应同时记录范围和性质，并区分免费分析器与书籍的出版形式。
| 资源 | 平台 | 类型 |
|---|---|---|
| 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 | 实践 |
陷阱
| 陷阱 | 为什么会误导 | 更好的做法 |
|---|---|---|
| 混淆真与可推导 | 真依赖解释，可推导依赖规则和公理。 | 同时说明两者，并指出连接它们的可靠性或完备性结论。 |
| 把完备性读成可判定性 | 不存在证明时，证明枚举可能永不终止。 | 区分检查、搜索与总能终止的判定程序。 |
| 把不完备性用于所有形式系统 | 定理具有有效性、算术表达能力和一致性等前提。 | 先说明理论与具体定理，再得出结论。 |
| 引用逻辑片段却省略限制 | 量词顺序、函数符号与语义都会改变问题。 | 在可判定性主张旁写清片段定义。 |
| 把求解器答案当作意图正确的证明 | 求解器推理的是提供给它的编码。 | 检查模型、反例、假设和翻译边界。 |
| 把每个带类型程序都叫作证明 | 不终止与未经验证的假设会改变对应关系。 | 指明演算，以及使项成为有效证据的条件。 |