Loading field map
Computational logic is the study of how logical systems can be represented, manipulated, and reasoned about by computational means, and conversely, how logical concepts can be used to model and analyze computation itself. It sits at the intersection of mathematical logic and computer science, treating logic not merely as a formal language for expressing truths but as a calculational instrument: something that can be automated, implemented, and put to work in programs.
The field is defined by a double commitment. On one side, it asks what can be decided, computed, or verified about logical formulas and proofs. On the other, it asks how logical formalisms can serve as executable specifications, programming languages, or reasoning engines. This dual character means that computational logic is neither pure mathematics nor pure engineering, but a discipline in which theoretical results about expressiveness and complexity directly shape the design of practical systems, and practical implementation challenges motivate new theoretical questions.
At its core, computational logic addresses a cluster of recurring questions. The most fundamental is the decision problem: given a logical formula, is there an algorithm that determines whether it is valid, satisfiable, or entailed by a set of assumptions? For propositional logic this is decidable, though the cost of doing so in general is believed to be exponential. For first-order logic, the decision problem is undecidable in full generality, a result established by Alonzo Church and Alan Turing in the 1930s. This negative result does not end the inquiry; it reframes it. The field then asks which restricted fragments of first-order logic remain decidable, which decidable fragments are still expressive enough for practical use, and how to build algorithms that work well on the formulas that actually arise in applications.
A second central question concerns proof. Given a logical consequence, can a proof of it be found automatically? This is the theorem-proving problem. It is closely related to the decision problem—in many logics, validity and provability coincide—but it has a distinct computational character. Proof search involves exploring a space of possible derivations, and the challenge is to find strategies that are complete (they find a proof if one exists) and efficient in practice. Related to this is the question of proof representation: what is a proof as a data structure, and how can proofs be checked, stored, and communicated?
A third question concerns computation itself. How can logical systems be used to express what a program does? This leads to the logic of programs, including Hoare logic for imperative programs, and to the Curry–Howard correspondence, which reveals that proofs in certain logical systems correspond exactly to programs in certain typed lambda calculi. Under this correspondence, a proof of a proposition is a program of the corresponding type, and the normalization of a proof corresponds to the execution of a program. This insight transforms logic from a tool for reasoning about programs into a foundation for programming languages themselves.
A fourth question concerns the limits of logical method. What can be expressed in a given logical language? Model theory asks what classes of structures are definable by formulas, while finite model theory asks the same question when only finite structures are considered—a restriction that changes many answers and connects logic to complexity theory. Descriptive complexity theory, for instance, characterizes computational complexity classes in terms of the logical languages needed to express their problems, revealing deep connections between logical expressiveness and computational difficulty.
The prehistory of computational logic lies in the late nineteenth and early twentieth centuries, when mathematical logic was transformed by figures such as Gottlob Frege, Bertrand Russell, and David Hilbert. Their goal was to place mathematics on a rigorous foundation by expressing mathematical reasoning in a formal language with precise rules of inference. This project produced the logical calculi that later became the raw material for computation, but it was not itself computational in orientation. Hilbert’s program, which sought to prove the consistency of mathematics by finitary means, did raise the question of whether mathematical reasoning could be mechanized, but the tools for answering that question did not yet exist.
The decisive turn came in the 1930s, when the concept of an effective procedure was made precise. Church’s lambda calculus and Turing’s abstract machines provided two equivalent formalizations of what it means for a function to be computable. With these in hand, the undecidability of first-order logic was established, and with it the fundamental boundary of what automated reasoning can achieve. This period also saw the development of proof theory by Gerhard Gentzen, whose sequent calculus and natural deduction systems were designed to mirror actual mathematical reasoning and whose structural properties—especially the cut-elimination theorem—later became central to computational logic.
The modern field emerged in the 1950s and 1960s with the advent of digital computers. Early work on automated theorem proving, particularly by Martin Davis, Hilary Putnam, and others, produced the first algorithms for deciding propositional satisfiability. The resolution principle, introduced by John Alan Robinson in 1965, provided a single inference rule that is complete for first-order logic and is well suited to mechanical implementation. Resolution became the basis of the first generation of automated theorem provers and remains influential in logic programming.
A parallel development came from the programming language community. In the late 1960s, Robert Floyd and C. A. R. Hoare developed methods for reasoning about program correctness using logical assertions about program states. This line of work, known as program verification, treats a program as a mathematical object whose behavior can be specified and proved correct. It introduced the idea that logic could be applied not just to mathematics but to the artifacts of computer science itself.
The 1970s and 1980s saw the consolidation of several distinct research programmes. Logic programming, exemplified by Prolog, treated logical formulas as executable specifications: a program is a set of Horn clauses, and computation is proof search. The Curry–Howard correspondence, which had been noted by Haskell Curry in the 1930s and developed by William Howard in the 1960s, became the foundation of constructive type theory and of proof assistants such as Coq and Agda. Meanwhile, the development of efficient algorithms for propositional satisfiability—the DPLL algorithm and its successors—made SAT solving a practical technology with applications far beyond logic itself.
Computational logic is not a single unified method but a family of approaches that differ in their underlying logical assumptions, their computational strategies, and their intended applications. These approaches coexist and often combine, but each has a distinct character.
Automated theorem proving seeks to find proofs of logical formulas without human intervention. The classical tradition, based on first-order logic and the resolution principle, treats proof search as a combinatorial problem: given a set of clauses, derive the empty clause to refute the negation of the target theorem. The key challenge is controlling the search space, since the number of possible derivations grows explosively. Modern first-order provers use sophisticated ordering and selection strategies, redundancy elimination, and indexing techniques to make proof search tractable on problems of practical interest.
The limits of this approach are both theoretical and practical. First-order logic is undecidable, so no complete prover can terminate on all inputs. In practice, provers may run forever on difficult problems, and their performance is highly sensitive to the syntactic form of the input. Nevertheless, automated theorem provers have become reliable tools in mathematics and verification, capable of finding proofs that are short but highly non-obvious.
Propositional satisfiability (SAT) checking is the special case of theorem proving restricted to propositional logic. Although the problem is NP-complete, modern SAT solvers routinely handle formulas with millions of variables. This surprising practical success rests on the DPLL algorithm—a backtracking search that assigns truth values to variables and propagates the consequences—augmented with clause learning, which records the reasons for failures and uses them to prune later search. SAT solvers are not proof finders in the traditional sense; they decide satisfiability and can produce a satisfying assignment or a proof of unsatisfiability.
SAT solving has become a workhorse technology. It underlies hardware and software verification, where circuit equivalence and model checking problems are reduced to SAT. It is also used in planning, scheduling, and combinatorial optimization. The success of SAT solving has spawned extensions to richer logics, including satisfiability modulo theories (SMT), which combine propositional reasoning with decision procedures for specific domains such as linear arithmetic, arrays, and bit vectors.
Logic programming inverts the usual relationship between logic and computation. Instead of writing an algorithm and then proving it correct, the programmer writes a logical description of the problem, and the computer searches for a solution. In Prolog, the most influential logic programming language, a program is a set of Horn clauses—implications of a restricted form—and computation is refutation proof search using resolution. The programmer controls the search through clause ordering and the cut operator, which prunes the search space.
The appeal of logic programming is its declarative character: programs read as logical statements about the problem domain. Its limitation is that the underlying proof search is not always efficient, and the programmer must often understand the search strategy to write effective programs. Logic programming has been influential in natural language processing, database querying, and expert systems, and its ideas have been absorbed into constraint programming and answer set programming, which extend the logical core to handle constraints and non-monotonic reasoning.
The constructive tradition in computational logic treats proofs as mathematical objects in their own right. Under the Curry–Howard correspondence, a proposition is a type, and a proof of the proposition is a program of that type. This identification makes logic and computation two aspects of the same underlying structure. Type theory, particularly Martin-Löf type theory and the calculus of inductive constructions, provides a logical framework in which both mathematical theorems and programs can be expressed and verified.
Proof assistants such as Coq, Agda, and Lean implement this framework. The user constructs a proof interactively, with the system checking each step for correctness. The resulting proof object is a term in the type theory, and its correctness is guaranteed by the system’s kernel—a small, trusted core that checks the validity of the term. This approach has been used to verify substantial mathematical results, including the four-color theorem and the Kepler conjecture, and to certify the correctness of compilers and operating system kernels.
The cost of this rigor is effort. Constructing a formal proof requires making every detail explicit, and the resulting proofs are often much longer than their informal counterparts. The field has responded by developing automation: tactics that search for proofs, decision procedures for decidable fragments, and reflection, which allows the proof assistant to reason about its own computations.
Model checking addresses a different question: given a system—typically a finite-state machine representing a hardware design or a software program—does it satisfy a given logical specification? The specification is expressed in a temporal logic, such as linear temporal logic (LTL) or computation tree logic (CTL), which can describe properties of system behavior over time, such as “eventually, the system reaches a safe state” or “it is always the case that if a request is made, it is eventually granted.”
Model checking works by exhaustively exploring the state space of the system, either explicitly or symbolically using binary decision diagrams or SAT-based techniques. The central challenge is the state explosion problem: the number of states grows exponentially with the size of the system. Modern model checkers use abstraction, compositional reasoning, and bounded exploration to manage this complexity. Model checking has been remarkably successful in hardware verification, where it is now standard practice, and it has been applied to software, communication protocols, and security.
A distinct tradition treats computation as the simplification of terms according to rewrite rules. Equational logic specifies the meaning of functions by equations, and computation consists of rewriting terms until no more rules apply. Term rewriting systems have a rich theory: confluence (the property that the order of rewriting does not affect the final result), termination (the property that rewriting always ends), and completion (the process of adding rules to make a system confluent and terminating). These properties are themselves logical questions, and they have been studied both theoretically and algorithmically.
Rewriting underlies functional programming, where programs are equations and execution is evaluation. It also provides the semantic foundation for algebraic specification, in which data types are defined by equations, and for the Maude system, which uses rewriting logic to model concurrent systems. The theory of rewriting connects to computational logic through the questions it raises about decidability and complexity, and through its use in proof normalization.
These approaches are not isolated silos. They share techniques and results, and many practical systems combine them. SAT solvers are used inside SMT solvers, which in turn are used inside proof assistants to discharge routine arithmetic obligations. Model checkers use SAT and binary decision diagrams, and they can produce counterexamples that are checked by theorem provers. Logic programming has influenced constraint solving, and answer set programming shares its roots in non-monotonic reasoning.
The deeper relationships are conceptual. Automated theorem proving and proof assistants both search for proofs, but they differ in their logical frameworks: classical first-order logic versus constructive type theory. This difference reflects a fundamental choice about what counts as a proof. Classical logic accepts proof by contradiction and the law of excluded middle; constructive logic requires proofs to be effective, so that from a proof of existence one can extract a witness. The Curry–Howard correspondence only works for constructive logic, and this is why proof assistants are built on type theories rather than on classical logic.
Model checking and theorem proving are often contrasted as exhaustive search versus deductive reasoning. Model checking is automatic but limited to finite-state systems; theorem proving is more general but requires human guidance. In practice, the two are complementary: model checking finds bugs in designs, while theorem proving establishes general correctness. Modern verification often uses both, with model checking exploring the state space and theorem proving providing the inductive arguments that cover unbounded cases.
Contemporary computational logic is characterized by the convergence of previously separate traditions and by the increasing scale of what can be verified. SAT and SMT solving have matured into industrial technologies, with competitions that drive steady improvements in performance. Proof assistants have grown powerful enough to formalize substantial mathematics and to verify realistic software, and the libraries of formalized mathematics have reached the point where new results can build on thousands of previously verified theorems.
The field has also expanded into new logical territory. Separation logic extends Hoare logic to reason about programs that manipulate pointers and mutable data structures. Homotopy type theory offers a new foundation for mathematics that unifies type theory with higher-dimensional structures. Probabilistic programming and differential dynamic logic extend logical methods to systems with uncertainty and continuous dynamics. These developments share the core commitment of computational logic: that logical formalism, made precise enough to be executed or checked by machine, is a powerful tool for understanding both mathematics and computation.
The enduring questions remain the ones that defined the field. What can be decided, and at what cost? What can be proved, and by what means? How can logical descriptions be turned into running systems, and how can running systems be shown to satisfy their logical descriptions? Computational logic answers these questions not once but continuously, as new logical systems are invented, new algorithms are developed, and new applications demand new forms of reasoning.