<p>I briefly reviewed some areas here, trying to focus on ideas that would appeal to someone with a background in advanced mathematical logic.</p>
<h2>Finite Model Theory</h2>
<p>The simplest restriction of classical model theory from the viewpoint
of computer science is to study structures over a finite universe.
These structures occur in the form of relational databases, graphs,
and other combinatorial objects arising everywhere in computer
science. The first observation is that several fundamental theorems of
first-order model theory fail when restricted to finite models. These
include the compactness theorem, Godel's completeness theorem, and
ultraproduct constructions. Trakhtenbrot showed that unlike classical
first order logic, satisfiability over finite models is undecidable.</p>
<p>The fundamental tools in this area are Hanf locality, Gaifman
locality, and numerous variations on Ehrenfeucht-Fraisse games. The
topics studied include infinitary logics, logics with counting, fixed
point logics, etc. always with a focus on finite models. There is work
focusing on expressivity in finite-variable fragments of first-order
logic and these logics have characterisations via pebble-games. Another direction of enquiry is to identify properties of classical logics that survive the restriction to finite models. A recent result in that direction from Rossman shows that certain homomorphism preservation theorems still hold over finite models.</p>
<ol>
<li><a href="https://rads.stackoverflow.com/amzn/click/com/3540287876" rel="nofollow noreferrer" rel="nofollow noreferrer">Finite Model Theory</a>, Ebbinghaus and Flum</li>
<li><a href="https://rads.stackoverflow.com/amzn/click/com/3642059481" rel="nofollow noreferrer" rel="nofollow noreferrer">Elements of Finite Model Theory</a>, Libkin</li>
<li><a href="http://researcher.watson.ibm.com/researcher/files/us-fagin/tcs97.pdf" rel="nofollow noreferrer">On winning strategies in Ehrenfeucht-Fraisse games</a>, Arora
and Fagin, 1997.</li>
<li><a href="http://www.mit.edu/%7Ebrossman/hpt-jacm-final.pdf" rel="nofollow noreferrer">Homomorphism preservation theorems</a>, Rossman</li>
</ol>
<h2>The propositional <span class="math-container">$\mu$</span>-calculus</h2>
<p>A line of work from the late 60s showed that numerous properties of
programs could be expressed in extensions of propositional logic that
supported reasoning about fixed points. The modal-<span class="math-container">$\mu$</span> calculus is
one logic developed in this period that has found a wide range of
applications in automated formal methods. A lot of formal methods is
connected to temporal logic, or Hoare-style logics and much of this
can be viewed in terms of the <span class="math-container">$\mu$</span>-calculus. In fact, I have heard it
said that the <span class="math-container">$\mu$</span>-calculus is the assembly language of temporal
logics.</p>
<p>In his paper introducing the <span class="math-container">$\mu$</span>-calculus, Kozen gave an
axiomatization and only proved it sound and complete for a restricted
fragment of the logic. The completeness proof was one of the great
open problems in logical computer science until Walukiewicz gave a
proof (based on infinite automata). The model theory of the
<span class="math-container">$\mu$</span>-calculus has many rich results. Similar to van Benthem's theorem
for modal logic, Janin and Walukiewicz proved that the <span class="math-container">$\mu$</span>-calculus
is expressively equivalent to the bisimulation invariant fragment of
monadic second order logic. The <span class="math-container">$\mu$</span>-calculus has also been
characterised in terms of parity games and automata over infinite
trees. The satisfiability problem for this logic is EXPTIME complete
and Emerson and Jutla showed that the logic has the small model
property. Bradfield showed that the alternation hierarchy of the <span class="math-container">$\mu$</span>-calculus is strict, while Berwanger showed that the variable hierarchy is also strict. Important classical tools used in this area are Rabin's theorem and
Martin's determinacy theorem.</p>
<ol>
<li><a href="http://www.cs.cornell.edu/%7Ekozen/papers/mu.pdf" rel="nofollow noreferrer">Results on the propositional <span class="math-container">$\mu$</span>-calculus</a>, Kozen, 1983</li>
<li><a href="https://rads.stackoverflow.com/amzn/click/com/0444506209" rel="nofollow noreferrer" rel="nofollow noreferrer">Rudiments of <span class="math-container">$\mu$</span>-calculus</a> Arnold and Niwinski, 2001</li>
<li><a href="http://www.labri.fr/perso/igw/Papers/igw-kozen-compl.ps" rel="nofollow noreferrer">Completeness of Kozen's Axiomatisation of the Propositional
<span class="math-container">$\mu$</span>-Calculus</a>, Walukiewicz 1995</li>
<li><a href="http://homepages.inf.ed.ac.uk/jcb/Research/bradfield-stirling-HPA-mu-intro.ps.gz" rel="nofollow noreferrer">Modal logics and <span class="math-container">$\mu$</span>-calculi</a>, Bradfield and Stirling, 2001</li>
<li><a href="http://link.springer.com/chapter/10.1007/3-540-61604-7_58?LI=true" rel="nofollow noreferrer">The modal mu-calculus alternation hierarchy is strict</a>, Bradfield, 1996</li>
<li><a href="http://mtc.epfl.ch/%7Edwb/pub/hierarchy.pdf" rel="nofollow noreferrer">The variable hierarchy of the mu-calculus is strict</a>, Berwanger, E. Grädel, and G. Lenzi, 2005</li>
</ol>
<h2>Linear Temporal Logic</h2>
<p>Linear temporal logic was adopted from philosophical logic into
computer science for reasoning about the behaviour of computer
programs. It was considered a good logic because it could express
properties such as invariance (absence of errors) and termination. The
proof theory of temporal logic was developed by Manna and Pnueli (and
others, later) in their articles and books. The model checking and the
satisfiability problem for LTL can both be solved in terms of automata
over infinite words.</p>
<p>Pnueli also proved fundamental resuls about LTL in his original paper
introducing the logic for reasoning about programs. Vardi and Wolper
gave a much simpler compilation of LTL formulae into Buchi automata.
The connection to temporal logic has led to intense study of
algorithms for efficiently deriving automata from LTL, and for
determinization and complementation of Buchi automata. Kamp's theorem
shows that LTL with <em>since</em> and <em>until</em> modalities is expressively
equivalent to monadic first-order logic with an order relation. There
is ongoing work extending these results to logics over dense linear
orders and time intervals. Etessami and Wilke developed a variation of Ehrenfeucht-Fraisse games for LTL and used them to show that the until hierarchy is strict. Another line of work is to extend LTL to express arbitrary <span class="math-container">$\omega$</span>-regular properties. This leads to the linear-time <span class="math-container">$\mu$</span>-calculus, a linear-time counterpart of the modal <span class="math-container">$\mu$</span>-calculus. Unlike the modal counterpart, the linear-time alternation hierarchy collapses at level 2.</p>
<ol>
<li><a href="http://dl.acm.org/citation.cfm?id=1382534" rel="nofollow noreferrer">The temporal logic of programs</a>, Pnueli 1977</li>
<li><a href="http://www.cs.rice.edu/%7Evardi/papers/25mc.ps.gz" rel="nofollow noreferrer">From Church and Prior to PSL</a>, Vardi, 2008</li>
<li><a href="http://link.springer.com/chapter/10.1007/3-540-60915-6_6?LI=true" rel="nofollow noreferrer">An automata-theoretic approach to linear temporal logic</a>,
Vardi and Wolper, 1986</li>
<li><a href="https://rads.stackoverflow.com/amzn/click/com/0387976647" rel="nofollow noreferrer" rel="nofollow noreferrer">The Temporal Logic of Reactive and Concurrent Systems:
Specification</a>, Manna and Pnueli</li>
<li><a href="http://dl.acm.org/citation.cfm?id=346584" rel="nofollow noreferrer">An Until hierarchy and other applications of an Ehrenfeucht-Fraïssé game for temporal logic</a>, Etessami and Wilke, 2000</li>
</ol>
<h2>Computational-Tree Logics</h2>
<p>Instead of a linear notion of time, the behaviour of a computer
program can be understood as a tree, leading to the notion of
computational tree logics. The simplest such logic, Computational Tree
Logic can be viewed as an alternation-free fragment of the
<span class="math-container">$\mu$</span>-calculus. The difference between LTL and CTL led Emerson and
Halpern to develop CTL*, which allows reasoning about both properties
of states and traces.</p>
<p>The model checking problem for CTL over finite structures is in
polynomial time. The model checking problem for CTL* is EXPTIME
complete. The axiomatization of CTL* was a challenging open problem
that was finally resolved by Reynolds 2001. The analogue of van
Benthem's theorem for modal logic and Kamp's theorem for LTL is given
for CTL* by a theorem of Hafer and Thomas showing that CTL*
corresponds to a fragment of monadic second order logic over binary
trees. A later characterisation by Hirschfeld and Rabinovich is that
CTL* is expressively equivalent to the bisimulation-invariant fragment
of MSO with path quantification.</p>
<ol>
<li><a href="http://dl.acm.org/citation.cfm?doid=4904.4999" rel="nofollow noreferrer">&quot;Sometimes&quot; and &quot;not never&quot; revisited: on
branching versus linear time temporal logic</a>, Emerson and Halpern,
1986</li>
<li><a href="http://www.computer.org/csdl/proceedings/lics/1999/0158/00/01580360-abs.html" rel="nofollow noreferrer">On the Expressive Power of CTL</a>, Moller, Rabinovich, 1999</li>
<li><a href="http://link.springer.com/chapter/10.1007/3-540-18088-5_22" rel="nofollow noreferrer">Computation tree logic CTL* and path quantifiers in the monadic
theory of the binary tree</a>, Hafer and Thomas, 1987</li>
<li><a href="https://doi.org/10.2307/2695091" rel="nofollow noreferrer">An Axiomatization of Full Computation Tree Logic</a>, Reynolds,
2001, <a href="https://www.jstor.org/stable/269509" rel="nofollow noreferrer">JSTOR</a></li>
</ol>
<h2>Languages of Infinite Words</h2>
<p>The connection to LTL and the necessicity of modelling infinite
behaviour led to an intense study of <span class="math-container">$\omega$</span>-languages, which are languages in which words are defined as functions from natural numbers to a finite alphabet. The community has studied properties of regular languages over infinite
words and developed several results analogous to the finite-word case. There are several surprises that show up, so we cannot just lift the finite-word results to the infinite-word case.</p>
<p>Some of my favourite results are the characterisiation of <span class="math-container">$\omega$</span>-regular languages in terms of regular languages and analogues of the
Myhill-Nerode theorems. Staiger showed that you do not just get infinite word automata from an appropriately defined equivalence relation. This holds only for a specific sub-family of <span class="math-container">$\omega$</span>-regular languages. Alpern and Schneider formalised the intuitive notions of safety and liveness of computer programs in terms of  prefix-closed and limit-closed sets of <span class="math-container">$\omega$</span>-words. Moreover, using elementary topology, they showed that every linear-time property can be expressed as the intersection of a safety and a liveness property. This result has significant practical consequences because it means that rather than build complex property checkers, it suffices to build a safety and a liveness checker. A further reduction shows that it is enough to build an invariance checker and a termination checker. The safety-liveness characterisation was extended to trees by Manolios and Trefler and more recently to sets of traces, in the hyperproperties framework, by Clarkson and Schneider.</p>
<ol>
<li><a href="http://www.liafa.jussieu.fr/%7Ejep/Resumes/InfiniteWords.html" rel="nofollow noreferrer">Infinite Words: Automata, Semigroups, Logic and Games</a>, Perrin and Pin, 2004</li>
<li><a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.26.4182" rel="nofollow noreferrer"><span class="math-container">$\omega$</span>-Languages</a>, Staiger, 1997</li>
<li><a href="http://hal.archives-ouvertes.fr/docs/00/45/61/13/PDF/bojanczyk.pdf" rel="nofollow noreferrer">Beyond <span class="math-container">$\omega$</span>-Regular Languages</a>, Bojanczyk, 2010</li>
<li><a href="http://link.springer.com/chapter/10.1007/3-540-56503-5_58" rel="nofollow noreferrer">On syntactic congruences for ω—languages</a>, Maler and Staiger, 1993</li>
</ol>
<h2>Automata on Infinite Words</h2>
<p>Where there are languages, computer scientists will have automata. Enter the theory of automata over infinite words and infinite trees. It is extremely sad that although automata over infinite words appeared within two years of automata on finite words, this fundamental topic is rarely covered in standard computer science curricula. Automata over infinite words and trees provide a very robust approach to prove decidability of satisfiability for a very rich family of logics.</p>
<p>A fundamental result is that the different acceptance criteria for
infinite word automata are all equivalent. The basic problems of
union, intersection, and complement for <span class="math-container">$\omega$</span>-automata are more
involved than their finite word counterparts and the details differ
with the acceptance criterion used. Safra gave a famously complex determinization algorithm for Buchi automata and significant work has been devoted to deriving a new and simpler construction. Rabin famously proved that the monadic second order theory of the binary tree is decidable. His proof uses automata and the cornerstone result is the determinization of Rabin automata. I have heard tell that Rabin's theorem is the <em>mother of all decidability results</em> in program verification.</p>
<ol>
<li><a href="http://www.jstor.org/discover/10.2307/1995086?uid=3739560&amp;uid=2&amp;uid=4&amp;uid=3739256&amp;sid=21101657945657" rel="nofollow noreferrer">Decidability of Second-Order Theories and Automata on Infinite Trees</a>, Rabin, 1969</li>
<li><a href="http://www.automata.rwth-aachen.de/download/papers/thomas/thomas88.pdf" rel="nofollow noreferrer">Automata on infinite objects</a>, Thomas, 1988</li>
<li><a href="http://www.cs.rice.edu/%7Evardi/papers/wal07.pdf" rel="nofollow noreferrer">Automata: From Logics to Algorithms</a>, Vardi, 2007</li>
</ol>
<h2>Infinite Games</h2>
<p>Logical and infinite games are an active area of research. Games-theoretic notions show up in computer science all over the place in the duality between non-determinism and parallelism (alternation), a program and its environment, universal and existential quantification, box and diamond modalities, etc. Games turned out to be a great way to study properties of the various types of non-classical logics listed above.</p>
<p>As with acceptance criteria for automata, we have different winning conditions for games and many can be shown to be equivalent. Since you asked about classical results, the Borel Determinacy theorem and Gale-Stewart games often lie discreetly in the background of several game models we study. One pressing question of our times has been about the complexity of solving parity games. Jurdzinski gave a strategy-improvement algorithm and showed that deciding the winner was in the intersection of the complexity classes UP and coUP. The precise complexity of Jurdzinski's algorithm was open until Friedmann gave it an exponential-time lower bound in 2009.</p>
<ol>
<li><a href="https://www.sciencedirect.com/science/article/pii/S0020019098001501" rel="nofollow noreferrer">Deciding the winner in parity games is in UP ∩ co-UP</a>, Jurdzinski, 1998</li>
<li><a href="https://www.sciencedirect.com/science/article/pii/0304397595001360" rel="nofollow noreferrer">Games for the μ-calculus</a>, Niwinski and Walukiewicz, 1996</li>
<li><a href="http://files.oliverfriedmann.de/papers/strategy_improvement_lower_bound.pdf" rel="nofollow noreferrer">An Exponential Lower Bound for the Parity Game Strategy Improvement Algorithm as We Know it</a>, Friedmann, 2009</li>
</ol>

CC BY-SA 4.0
2013-01-13T23:06:30.583Z
2022-04-23T05:59:42.850Z
2022-04-23T05:59:42.850Z
Vijay D
<p><strong>Edmund M. Clarke, Orna Grumberg, Doron A. Peled:</strong> <em>Model Checking</em>. MIT Press 1999, is a nice book (for me) on model checking.</p>

<p><strong>Glynn Winskel:</strong> <em>The Formal Semantics of Programming Languages: an introduction</em>. MIT Press 1994, is one of the standard textbooks on programming languages. </p>

<p><strong>Mordechai Ben-Ari:</strong> <em>Mathematical logic for computer science</em>. Springer 2001, is perhaps what you are looking for.</p>

CC BY-SA 3.0
2013-01-13T00:05:16.743Z
2013-01-13T09:00:52.243Z
2013-01-13T09:00:52.243Z
vb le
<p>Michael Huth and Mark Ryan: <a href="http://www.cs.bham.ac.uk/research/projects/lics/">Logic in computer science</a>, Cambridge University Press, 2004.</p>

<p>I recommend this book highly as a general introduction on how logic plays a role in computer science.</p>

CC BY-SA 3.0
2013-01-13T22:09:24.703Z
2013-01-13T22:09:24.703Z
Andrej Bauer
<p>Database theory is a sprawling field providing many applications of logic.  Descriptive complexity and finite model theory are closely associated fields.  As far as I can tell, these areas all tend to use algebraic styles of logic (following in the footsteps of Birkhoff and Tarski) rather than proof-theoretic.  However, some of the work of <a href="http://dblp.uni-trier.de/pers/hd/b/Buneman%3aPeter.html">Peter Buneman</a>, <a href="http://dblp.uni-trier.de/pers/hd/l/Libkin%3aLeonid.html">Leonid Libkin</a>, <a href="http://dblp.uni-trier.de/pers/hd/f/Fan%3aWenfei.html">Wenfei Fan</a>, <a href="http://dblp.uni-trier.de/pers/hd/d/Davidson%3aSusan_B=.html">Susan Davidson</a>, <a href="http://dblp.uni-trier.de/pers/hd/w/Wong%3aLimsoon.html">Limsoon Wong</a>, <a href="http://dblp.uni-trier.de/pers/hd/o/Ohori%3aAtsushi.html">Atsushi Ohori</a>, and other researchers who were working at UPenn in the 1980s-90s, did seek to unite programming language theory and databases.  This seems to require being comfortable with both styles of logic.  The same goes for more recent work by <a href="http://dblp.uni-trier.de/pers/hd/c/Cheney%3aJames.html">James Cheney</a> and <a href="http://dblp.uni-trier.de/pers/hd/w/Wadler%3aPhilip.html">Philip Wadler</a>.</p>

<p>In terms of specific references, the standard textbook is available online for convenient reference:</p>

<ul>
<li>Serge Abiteboul, Richard Hull, Victor Vianu.  <em>Foundations of Databases</em>, 1995.  <a href="http://webdam.inria.fr/Alice/">http://webdam.inria.fr/Alice/</a></li>
</ul>

<p>Unfortunately I don't know any up to date general textbooks or surveys covering this fast-moving field.  I have found two older surveys useful.  First,</p>

<ul>
<li>Jan Van den Bussche, <em>Applications of Alfred Tarski's Ideas in Database Theory</em>, CSL 2001. <a href="http://dx.doi.org/10.1007/3-540-44802-0_2">doi:10.1007/3-540-44802-0_2</a></li>
</ul>

<p>shows how to connect the dots between Tarski and a specific subfield, constraint databases.  Second,</p>

<ul>
<li>Victor Vianu, <em>Databases and Finite-Model Theory</em>, Descriptive Complexity and Finite Models: Proceedings of a DIMACS Workshop, 1996. <a href="http://leo.saclay.inria.fr/publifiles/gemo/GemoReport-107.ps.gz">http://leo.saclay.inria.fr/publifiles/gemo/GemoReport-107.ps.gz</a></li>
</ul>

<p>pitches (1996-style) database theory to finite model theorists, and in the process highlights many interesting applications of logic in databases.  For more recent work (such as the theory of XML, provenance, streaming models, or graph databases) reading highly-cited research papers is a reasonable approach.</p>

CC BY-SA 3.0
2013-01-13T18:26:00.223Z
2013-01-13T18:26:00.223Z
András Salamon
<p>A key use of logic in CS is program logics, also called Hoare logics. </p>

<p>One good way of thinking about program logics is to see them as sub-calculi of ZFC set-theory (or whatever your preferred foundation of maths might be, e.g. second-order logic) that are just expressive enough to reason about programs in a given programming language, but not more. You can always reason about programs in ZFC set theory, but set theory has too much expressive power in the sense that it contains many formulae that are not really relevant for reasoning about programs (e.g. $2 \in \sqrt(\pi^{17})$ is a valid formula in ZFC that may or may not be true, depending on how you code up real numbers as sets). The superfluous expressive power is a disadvantage when thinking about program correctness because (simplifying a bit) it increases formula and proof size. 
So what we are looking for in the study of program logics are logics with succinct formulae and proofs. </p>

<p>A similar situation obtains in the study of modal logics which (simplfying a bit again)
 are not as expressive as first-order logic, but what they can express, they
do express with shorter formulae and proofs. </p>

<p>Identifying suitable fragments of ZFC is not hard for simple programming languages, but gets rapidly more challenging as programming languages acquire more features. The last couple of years have seen substantial progress in this endeavour.</p>

<p>The paper <a href="http://sunnyday.mit.edu/16.355/Hoare-CACM-69.pdf" rel="nofollow">An Axiomatic Basis for Computer Programming</a> by T. Hoare is often seen as founding the study of program logics in earnest, is easy to read, and probably a good way to start venturing into the field. The same logic is studied in more detail in Winskel's book "Formal Semantics of Programming Languages" menioned by @vb le.</p>

<p>Type theory can be seen in a similar light. The key selling point of type-theory is the identification of proofs with (purely functional) programs, leading to a great economy of concepts and to powerful automation (in the form of type-inference and interactive theorem provers). The price for type theory's being an elegant way of organising proofs is that it does not appear to work all that well with programming languages that are not purely functional. </p>

<p>A recent and throughly modern text that introduces program logic in a type-theoretic tinged way is <a href="http://www.cis.upenn.edu/~bcpierce/sf/index.html" rel="nofollow">Software Foundations</a> by Pierce et al. It'll lead you right near the (a) cutting edge of research in program verification and, as a textbook, probably gives a glimpse of how computer science and maths will be taught in the future.</p>

<p>Once a program logic has been developed for a language, the next
step is automation, or partial automation: constructing proofs
for non-trivial programs is labour intensive, and we would like
machines to do as much of it as possible. Much current research
in formal methods to do with such automation. </p>

CC BY-SA 3.0
2013-01-13T01:51:33.010Z
2013-01-13T08:47:28.200Z
2013-01-13T08:47:28.200Z
Martin Berger
<p>There is a very strong tradition of logic in computer science. The problems we study and the aesthetics of the computational logic community is not identical to that of the mathematical logic community. You are absolutely right that significant developments in model theory, the meta-theory of first-order logic and of set theory are not commonly used in computational logic. One can successfully research computational logi without seeing or using ultrafilters, non-standard analysis, forcing, the Paris-Harrington theorem, and a host of other fascinating concepts which are considered important in classical logic.</p>

<p>Just as one applies mathematical ideas to study logic as well as logical ideas to study mathematics, we apply logic to study computer science and as well as applying computational perspectives to study logic. This different focus has rather dramatic consequences for the types of results that are important for us.</p>

<p>Here is a quotation from John Baez about logic and computer science. I do not hold exactly the same view because I am not very familiar with advanced mathematical logic.</p>

<blockquote>
  <p>When I was an undergraduate I was quite interested in logic and the foundations of mathematics --- I was always looking for the most mind-blowing concepts I could get ahold of, and Goedel's theorem, the Loewenheim-Skolem theorem, and so on were right up there with quantum mechanics and general relativity as far as I was concerned. [...] I remember feeling at the time that logic had become less revolutionary than in it was in the early part of the century. It seemed to me that logic had become a branch of mathematics like any other, studying obscure properties of models of the Zermelo-Fraenkel axioms, rather than questioning the basic presumptions implicit in those axioms and daring to pursue new, different approaches. [...]</p>
  
  <p>Anyway, it's now quite clear to me that I just hadn't been reading the right stuff. I think Rota has said that the really interesting work in logic now goes under the name of "computer science',[...] <em>--Week 40, This Week's Find, John Baez</em></p>
</blockquote>

<p>Logic in computer science is a vast and rapidly developing field. I find that every perspective of classical logic can be modified to derive some perspective on computational logic. The Wikipedia entry on mathematical logic splits the field into set theory, model theory, proof theory and recursion theory. You can esssentially take these areas and add a computational flavour to them and obtain a sub-field of computational logic.</p>

<p><strong>Model Theory</strong> We like to study the model theory of non-classical logics and non-classical models of classical logic. By that I mean that we study modal, temporal and sub-structural logics, and that we study logics over trees, words, and finite models, as opposed to classical models like algebras. The two fundamental problems are satisfiability and model checking. Both have immense practical and theoretical significance. In contrast, these problems are less central in classical logic.</p>

<p><strong>Proof theory</strong> We study the complexity and efficiency with which we can generate proofs in classical proof systems, as well as developing new, non-classical proof systems that are sensitive to complexity and efficiency considerations. Automated deduction studies machine-supported proof generation, broad speaking. The process may involve human interaction or be completely automatic. There is a lot of work on developing decision procedures for logical theories. Proof complexity focuses on the size of proofs and the computational complexity of generating proofs. There is a fascinating line of work relating programs to proofs, which combines with work descending from linear logic to develop proof systems, and consequently programming languages, that are resource sensitive.</p>

<p><strong>Recursion theory</strong> Our recursion theory is complexity theory. Rather than studying what is computable we study how efficiently we can compute. There are many analogues of recursion theory in complexity theory, but the results and separations of recursion theory do not always hold for their complexity theoretic analogues. Instead of computable sets and an arithmetic hierarchy, we have polynomial time, the polynomial time hierarchy and polynomial space enclosing the hierarchy. Instead of bounded quantification in the arithmetic hierarchy, we have satisfiability and quantified Boolean formulae and bounded quantification of Boolean formulae.</p>

<p>The survey article</p>

<blockquote>
  <p><a href="http://www.cs.rice.edu/~vardi/papers/aaas99.jsl.pdf" rel="nofollow noreferrer">On the Unusual Effectiveness of Logic in Computer Science</a></p>
</blockquote>

<p>is a good starting point to get a very high-level view of computational logic. I am going to list several, logically oriented fields of computer science. I hope that others will edit this answer and add to that list here, and possibly add a link to an answer on this page.</p>

<ol>
<li><a href="https://cstheory.stackexchange.com/a/15081/4155">Finite model theory</a></li>
<li>Proof complexity</li>
<li>Algorithmic deduction (decision procedures for logical theories)</li>
<li><a href="https://cstheory.stackexchange.com/a/15064/4155">Logics of programs</a></li>
<li>Dynamic logic</li>
<li><a href="https://cstheory.stackexchange.com/a/15081/4155">Linear Temporal logic</a> and its variants</li>
<li>Computational Tree Logic and its variants</li>
<li>Epistemic logic</li>
<li><a href="https://cstheory.stackexchange.com/a/15070/4155">Database theory</a></li>
<li>Type theory</li>
<li><a href="https://cstheory.stackexchange.com/a/15081/4155">Automata over infinite words</a></li>
<li>Categorical logic</li>
<li>Concurrency theory and process algebra</li>
<li>Domain theory</li>
<li>Linear logic</li>
<li>Descriptive Complexity</li>
<li>Model Checking</li>
<li><a href="https://cstheory.stackexchange.com/a/15081/4155">Fixed Point calculi</a> and transitive closure logics</li>
</ol>

CC BY-SA 3.0
2013-01-18T04:21:45.223Z
2013-01-18T04:21:45.223Z
2017-04-13T12:32:28.080Z
Vijay D
<p>an area of strong overlap between logic and computer science is <a href="http://en.wikipedia.org/wiki/Automated_theorem_proving" rel="nofollow noreferrer">automated theorem proving</a>, eg [4]. also eg ref [1] is the use of the Boyer-Moore theorem prover to check/verify Godels theorem. another recent major/impressive result is the recent completion of software verification of the four color theorem (and others such as Odd Order and Feit-Thompson [3]) at Microsoft research by Gonthier.[2]</p>

<p>[1] <a href="http://rads.stackoverflow.com/amzn/click/0521585333" rel="nofollow noreferrer">Metamathematics, Machines and Gödel's Proof (Cambridge Tracts in Theoretical Computer Science</a> by Shankar</p>

<p>[2] <a href="http://research.microsoft.com/en-us/um/people/gonthier/4colproof.pdf" rel="nofollow noreferrer">A computer-checked proof of the Four Colour Theorem</a> Georges Gonthier</p>

<p>[3] <a href="https://cstheory.stackexchange.com/questions/12729/interesting-algorithms-in-the-formalization-of-the-feit-thompson-theorem">Interesting algorithms in the formalization of the Feit-Thompson theorem?</a> tcs.se</p>

<p>[4] <a href="https://cstheory.stackexchange.com/questions/82/where-and-how-did-computers-help-prove-a-theorem">Where and how did computers help prove a theorem?</a> tcs.se</p>

CC BY-SA 3.0
2013-01-17T22:25:05.057Z
2013-01-17T22:30:26.153Z
2017-04-13T12:32:28.077Z
vzn
<p>I'm a grad student in math with a solid background in logic. I've taken a year-long graduate course in logic together with graduate courses on finite model theory and another on forcing and set theory. Most CS texts seem to assume only a very modest background in logic, which mostly covers basics of propositional logic and first-order logic.</p>

<p>I'd like to get some pointers on where to go for CS applications where heavier material from logic is being used. One interest of mine would be type theory and formal methods in general. Could anyone suggest some good readings past the introductory books on model checking and programming languages?</p>

CC BY-SA 3.0
2013-01-13T18:37:39.130Z
I made this CW as the list is very long. Just have a look at 11 volumes of Handbook of Logic in Computer Science and  Handbook of Logic in AI.
Kaveh
CC BY-SA 3.0
2013-01-13T20:05:45.140Z
A good point to start is the following paper: - Samuel R. Buss, Alexander A. Kechris, Anand Pillay, and Richard A. Shore, "[Prospects for mathematical logic in the twenty-first century](http://www.math.ucsd.edu/~sbuss/ResearchWeb/FutureOfLogic/)", 2001. In particular the section by Sam Buss.
Kaveh
CC BY-SA 3.0
2013-01-14T06:52:43.757Z
This question could be expanded and answers uniformly structured so that this page eventually becomes a useful starting-point resource on computational logic. Please join the [discussion](http://meta.cstheory.stackexchange.com/questions/1639/help-answering-the-cs-applications-of-logic-question) on meta.
Vijay D
CC BY-SA 4.0
2020-04-21T03:38:24.630Z
Principles of Model Checking (Baier and Katoen) is also superb if you are interested in model-checking.  (I mention due to the reference to FM in the question.)  The book is mathematically mature, the proofs are quite good, and the references are also excellent.
Max von Hippel
<lo.logic><soft-question><big-list><books><formal-methods>
Pointers for CS applications of logic
evf
# Pointers for CS applications of logic

(Asked by: username_0 on 2013-01-12)

I'm a grad student in math with a solid background in logic. I've taken a year-long graduate course in logic together with graduate courses on finite model theory and another on forcing and set theory. Most CS texts seem to assume only a very modest background in logic, which mostly covers basics of propositional logic and first-order logic.

I'd like to get some pointers on where to go for CS applications where heavier material from logic is being used. One interest of mine would be type theory and formal methods in general. Could anyone suggest some good readings past the introductory books on model checking and programming languages?

**Tags:** lo.logic, soft-question, big-list, books, formal-methods
> **Comments:**
> **username_1**: I made this CW as the list is very long. Just have a look at 11 volumes of Handbook of Logic in Computer Science and  Handbook of Logic in AI.  
> **username_1**: A good point to start is the following paper: - Samuel R. Buss, Alexander A. Kechris, Anand Pillay, and Richard A. Shore, "[Prospects for mathematical logic in the twenty-first century](http://www.math.ucsd.edu/~sbuss/ResearchWeb/FutureOfLogic/)", 2001. In particular the section by Sam Buss.  
> **username_2**: This question could be expanded and answers uniformly structured so that this page eventually becomes a useful starting-point resource on computational logic. Please join the [discussion](http://meta.cstheory.stackexchange.com/questions/1639/help-answering-the-cs-applications-of-logic-question) on meta.  
> **username_3**: Principles of Model Checking (Baier and Katoen) is also superb if you are interested in model-checking.  (I mention due to the reference to FM in the question.)  The book is mathematically mature, the proofs are quite good, and the references are also excellent.  

---

## 7 answers

### Answer by username_2 on 2013-01-13. Score: 16

I briefly reviewed some areas here, trying to focus on ideas that would appeal to someone with a background in advanced mathematical logic.

## Finite Model Theory

The simplest restriction of classical model theory from the viewpoint
of computer science is to study structures over a finite universe.
These structures occur in the form of relational databases, graphs,
and other combinatorial objects arising everywhere in computer
science. The first observation is that several fundamental theorems of
first-order model theory fail when restricted to finite models. These
include the compactness theorem, Godel's completeness theorem, and
ultraproduct constructions. Trakhtenbrot showed that unlike classical
first order logic, satisfiability over finite models is undecidable.

The fundamental tools in this area are Hanf locality, Gaifman
locality, and numerous variations on Ehrenfeucht-Fraisse games. The
topics studied include infinitary logics, logics with counting, fixed
point logics, etc. always with a focus on finite models. There is work
focusing on expressivity in finite-variable fragments of first-order
logic and these logics have characterisations via pebble-games. Another direction of enquiry is to identify properties of classical logics that survive the restriction to finite models. A recent result in that direction from Rossman shows that certain homomorphism preservation theorems still hold over finite models.

1. [Finite Model Theory](https://rads.stackoverflow.com/amzn/click/com/3540287876), Ebbinghaus and Flum
2. [Elements of Finite Model Theory](https://rads.stackoverflow.com/amzn/click/com/3642059481), Libkin
3. [On winning strategies in Ehrenfeucht-Fraisse games](http://researcher.watson.ibm.com/researcher/files/us-fagin/tcs97.pdf), Arora
   and Fagin, 1997.
4. [Homomorphism preservation theorems](http://www.mit.edu/%7Ebrossman/hpt-jacm-final.pdf), Rossman

## The propositional $\mu$-calculus

A line of work from the late 60s showed that numerous properties of
programs could be expressed in extensions of propositional logic that
supported reasoning about fixed points. The modal-$\mu$ calculus is
one logic developed in this period that has found a wide range of
applications in automated formal methods. A lot of formal methods is
connected to temporal logic, or Hoare-style logics and much of this
can be viewed in terms of the $\mu$-calculus. In fact, I have heard it
said that the $\mu$-calculus is the assembly language of temporal
logics.

In his paper introducing the $\mu$-calculus, Kozen gave an
axiomatization and only proved it sound and complete for a restricted
fragment of the logic. The completeness proof was one of the great
open problems in logical computer science until Walukiewicz gave a
proof (based on infinite automata). The model theory of the
$\mu$-calculus has many rich results. Similar to van Benthem's theorem
for modal logic, Janin and Walukiewicz proved that the $\mu$-calculus
is expressively equivalent to the bisimulation invariant fragment of
monadic second order logic. The $\mu$-calculus has also been
characterised in terms of parity games and automata over infinite
trees. The satisfiability problem for this logic is EXPTIME complete
and Emerson and Jutla showed that the logic has the small model
property. Bradfield showed that the alternation hierarchy of the $\mu$-calculus is strict, while Berwanger showed that the variable hierarchy is also strict. Important classical tools used in this area are Rabin's theorem and
Martin's determinacy theorem.

1. [Results on the propositional $\mu$-calculus](http://www.cs.cornell.edu/%7Ekozen/papers/mu.pdf), Kozen, 1983
2. [Rudiments of $\mu$-calculus](https://rads.stackoverflow.com/amzn/click/com/0444506209) Arnold and Niwinski, 2001
3. [Completeness of Kozen's Axiomatisation of the Propositional
   $\mu$-Calculus](http://www.labri.fr/perso/igw/Papers/igw-kozen-compl.ps), Walukiewicz 1995
4. [Modal logics and $\mu$-calculi](http://homepages.inf.ed.ac.uk/jcb/Research/bradfield-stirling-HPA-mu-intro.ps.gz), Bradfield and Stirling, 2001
5. [The modal mu-calculus alternation hierarchy is strict](http://link.springer.com/chapter/10.1007/3-540-61604-7_58?LI=true), Bradfield, 1996
6. [The variable hierarchy of the mu-calculus is strict](http://mtc.epfl.ch/%7Edwb/pub/hierarchy.pdf), Berwanger, E. Grädel, and G. Lenzi, 2005

## Linear Temporal Logic

Linear temporal logic was adopted from philosophical logic into
computer science for reasoning about the behaviour of computer
programs. It was considered a good logic because it could express
properties such as invariance (absence of errors) and termination. The
proof theory of temporal logic was developed by Manna and Pnueli (and
others, later) in their articles and books. The model checking and the
satisfiability problem for LTL can both be solved in terms of automata
over infinite words.

Pnueli also proved fundamental resuls about LTL in his original paper
introducing the logic for reasoning about programs. Vardi and Wolper
gave a much simpler compilation of LTL formulae into Buchi automata.
The connection to temporal logic has led to intense study of
algorithms for efficiently deriving automata from LTL, and for
determinization and complementation of Buchi automata. Kamp's theorem
shows that LTL with *since* and *until* modalities is expressively
equivalent to monadic first-order logic with an order relation. There
is ongoing work extending these results to logics over dense linear
orders and time intervals. Etessami and Wilke developed a variation of Ehrenfeucht-Fraisse games for LTL and used them to show that the until hierarchy is strict. Another line of work is to extend LTL to express arbitrary $\omega$-regular properties. This leads to the linear-time $\mu$-calculus, a linear-time counterpart of the modal $\mu$-calculus. Unlike the modal counterpart, the linear-time alternation hierarchy collapses at level 2.

1. [The temporal logic of programs](http://dl.acm.org/citation.cfm?id=1382534), Pnueli 1977
2. [From Church and Prior to PSL](http://www.cs.rice.edu/%7Evardi/papers/25mc.ps.gz), Vardi, 2008
3. [An automata-theoretic approach to linear temporal logic](http://link.springer.com/chapter/10.1007/3-540-60915-6_6?LI=true),
   Vardi and Wolper, 1986
4. [The Temporal Logic of Reactive and Concurrent Systems:
   Specification](https://rads.stackoverflow.com/amzn/click/com/0387976647), Manna and Pnueli
5. [An Until hierarchy and other applications of an Ehrenfeucht-Fraïssé game for temporal logic](http://dl.acm.org/citation.cfm?id=346584), Etessami and Wilke, 2000

## Computational-Tree Logics

Instead of a linear notion of time, the behaviour of a computer
program can be understood as a tree, leading to the notion of
computational tree logics. The simplest such logic, Computational Tree
Logic can be viewed as an alternation-free fragment of the
$\mu$-calculus. The difference between LTL and CTL led Emerson and
Halpern to develop CTL\*, which allows reasoning about both properties
of states and traces.

The model checking problem for CTL over finite structures is in
polynomial time. The model checking problem for CTL\* is EXPTIME
complete. The axiomatization of CTL\* was a challenging open problem
that was finally resolved by Reynolds 2001. The analogue of van
Benthem's theorem for modal logic and Kamp's theorem for LTL is given
for CTL\* by a theorem of Hafer and Thomas showing that CTL\*
corresponds to a fragment of monadic second order logic over binary
trees. A later characterisation by Hirschfeld and Rabinovich is that
CTL\* is expressively equivalent to the bisimulation-invariant fragment
of MSO with path quantification.

1. ["Sometimes" and "not never" revisited: on
   branching versus linear time temporal logic](http://dl.acm.org/citation.cfm?doid=4904.4999), Emerson and Halpern,
   1986
2. [On the Expressive Power of CTL](http://www.computer.org/csdl/proceedings/lics/1999/0158/00/01580360-abs.html), Moller, Rabinovich, 1999
3. [Computation tree logic CTL\* and path quantifiers in the monadic
   theory of the binary tree](http://link.springer.com/chapter/10.1007/3-540-18088-5_22), Hafer and Thomas, 1987
4. [An Axiomatization of Full Computation Tree Logic](https://doi.org/10.2307/2695091), Reynolds,
   2001, [JSTOR](https://www.jstor.org/stable/269509)

## Languages of Infinite Words

The connection to LTL and the necessicity of modelling infinite
behaviour led to an intense study of $\omega$-languages, which are languages in which words are defined as functions from natural numbers to a finite alphabet. The community has studied properties of regular languages over infinite
words and developed several results analogous to the finite-word case. There are several surprises that show up, so we cannot just lift the finite-word results to the infinite-word case.

Some of my favourite results are the characterisiation of $\omega$-regular languages in terms of regular languages and analogues of the
Myhill-Nerode theorems. Staiger showed that you do not just get infinite word automata from an appropriately defined equivalence relation. This holds only for a specific sub-family of $\omega$-regular languages. Alpern and Schneider formalised the intuitive notions of safety and liveness of computer programs in terms of prefix-closed and limit-closed sets of $\omega$-words. Moreover, using elementary topology, they showed that every linear-time property can be expressed as the intersection of a safety and a liveness property. This result has significant practical consequences because it means that rather than build complex property checkers, it suffices to build a safety and a liveness checker. A further reduction shows that it is enough to build an invariance checker and a termination checker. The safety-liveness characterisation was extended to trees by Manolios and Trefler and more recently to sets of traces, in the hyperproperties framework, by Clarkson and Schneider.

1. [Infinite Words: Automata, Semigroups, Logic and Games](http://www.liafa.jussieu.fr/%7Ejep/Resumes/InfiniteWords.html), Perrin and Pin, 2004
2. [$\omega$-Languages](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.26.4182), Staiger, 1997
3. [Beyond $\omega$-Regular Languages](http://hal.archives-ouvertes.fr/docs/00/45/61/13/PDF/bojanczyk.pdf), Bojanczyk, 2010
4. [On syntactic congruences for ω—languages](http://link.springer.com/chapter/10.1007/3-540-56503-5_58), Maler and Staiger, 1993

## Automata on Infinite Words

Where there are languages, computer scientists will have automata. Enter the theory of automata over infinite words and infinite trees. It is extremely sad that although automata over infinite words appeared within two years of automata on finite words, this fundamental topic is rarely covered in standard computer science curricula. Automata over infinite words and trees provide a very robust approach to prove decidability of satisfiability for a very rich family of logics.

A fundamental result is that the different acceptance criteria for
infinite word automata are all equivalent. The basic problems of
union, intersection, and complement for $\omega$-automata are more
involved than their finite word counterparts and the details differ
with the acceptance criterion used. Safra gave a famously complex determinization algorithm for Buchi automata and significant work has been devoted to deriving a new and simpler construction. Rabin famously proved that the monadic second order theory of the binary tree is decidable. His proof uses automata and the cornerstone result is the determinization of Rabin automata. I have heard tell that Rabin's theorem is the *mother of all decidability results* in program verification.

1. [Decidability of Second-Order Theories and Automata on Infinite Trees](http://www.jstor.org/discover/10.2307/1995086?uid=3739560&uid=2&uid=4&uid=3739256&sid=21101657945657), Rabin, 1969
2. [Automata on infinite objects](http://www.automata.rwth-aachen.de/download/papers/thomas/thomas88.pdf), Thomas, 1988
3. [Automata: From Logics to Algorithms](http://www.cs.rice.edu/%7Evardi/papers/wal07.pdf), Vardi, 2007

## Infinite Games

Logical and infinite games are an active area of research. Games-theoretic notions show up in computer science all over the place in the duality between non-determinism and parallelism (alternation), a program and its environment, universal and existential quantification, box and diamond modalities, etc. Games turned out to be a great way to study properties of the various types of non-classical logics listed above.

As with acceptance criteria for automata, we have different winning conditions for games and many can be shown to be equivalent. Since you asked about classical results, the Borel Determinacy theorem and Gale-Stewart games often lie discreetly in the background of several game models we study. One pressing question of our times has been about the complexity of solving parity games. Jurdzinski gave a strategy-improvement algorithm and showed that deciding the winner was in the intersection of the complexity classes UP and coUP. The precise complexity of Jurdzinski's algorithm was open until Friedmann gave it an exponential-time lower bound in 2009.

1. [Deciding the winner in parity games is in UP ∩ co-UP](https://www.sciencedirect.com/science/article/pii/S0020019098001501), Jurdzinski, 1998
2. [Games for the μ-calculus](https://www.sciencedirect.com/science/article/pii/0304397595001360), Niwinski and Walukiewicz, 1996
3. [An Exponential Lower Bound for the Parity Game Strategy Improvement Algorithm as We Know it](http://files.oliverfriedmann.de/papers/strategy_improvement_lower_bound.pdf), Friedmann, 2009


---

### Answer by username_4 on 2013-01-13. Score: 10

**Edmund M. Clarke, Orna Grumberg, Doron A. Peled:** *Model Checking*. MIT Press 1999, is a nice book (for me) on model checking.

**Glynn Winskel:** *The Formal Semantics of Programming Languages: an introduction*. MIT Press 1994, is one of the standard textbooks on programming languages.

**Mordechai Ben-Ari:** *Mathematical logic for computer science*. Springer 2001, is perhaps what you are looking for.


---

### Answer by username_6 on 2013-01-13. Score: 7

Database theory is a sprawling field providing many applications of logic. Descriptive complexity and finite model theory are closely associated fields. As far as I can tell, these areas all tend to use algebraic styles of logic (following in the footsteps of Birkhoff and Tarski) rather than proof-theoretic. However, some of the work of [Peter Buneman](http://dblp.uni-trier.de/pers/hd/b/Buneman%3aPeter.html), [Leonid Libkin](http://dblp.uni-trier.de/pers/hd/l/Libkin%3aLeonid.html), [Wenfei Fan](http://dblp.uni-trier.de/pers/hd/f/Fan%3aWenfei.html), [Susan Davidson](http://dblp.uni-trier.de/pers/hd/d/Davidson%3aSusan_B=.html), [Limsoon Wong](http://dblp.uni-trier.de/pers/hd/w/Wong%3aLimsoon.html), [Atsushi Ohori](http://dblp.uni-trier.de/pers/hd/o/Ohori%3aAtsushi.html), and other researchers who were working at UPenn in the 1980s-90s, did seek to unite programming language theory and databases. This seems to require being comfortable with both styles of logic. The same goes for more recent work by [James Cheney](http://dblp.uni-trier.de/pers/hd/c/Cheney%3aJames.html) and [Philip Wadler](http://dblp.uni-trier.de/pers/hd/w/Wadler%3aPhilip.html).

In terms of specific references, the standard textbook is available online for convenient reference:

* Serge Abiteboul, Richard Hull, Victor Vianu. *Foundations of Databases*, 1995. <http://webdam.inria.fr/Alice/>

Unfortunately I don't know any up to date general textbooks or surveys covering this fast-moving field. I have found two older surveys useful. First,

* Jan Van den Bussche, *Applications of Alfred Tarski's Ideas in Database Theory*, CSL 2001. [doi:10.1007/3-540-44802-0\_2](http://dx.doi.org/10.1007/3-540-44802-0_2)

shows how to connect the dots between Tarski and a specific subfield, constraint databases. Second,

* Victor Vianu, *Databases and Finite-Model Theory*, Descriptive Complexity and Finite Models: Proceedings of a DIMACS Workshop, 1996. <http://leo.saclay.inria.fr/publifiles/gemo/GemoReport-107.ps.gz>

pitches (1996-style) database theory to finite model theorists, and in the process highlights many interesting applications of logic in databases. For more recent work (such as the theory of XML, provenance, streaming models, or graph databases) reading highly-cited research papers is a reasonable approach.


---

### Answer by username_5 on 2013-01-13. Score: 6

Michael Huth and Mark Ryan: [Logic in computer science](http://www.cs.bham.ac.uk/research/projects/lics/), Cambridge University Press, 2004.

I recommend this book highly as a general introduction on how logic plays a role in computer science.


---

### Answer by username_7 on 2013-01-13. Score: 4

A key use of logic in CS is program logics, also called Hoare logics.

One good way of thinking about program logics is to see them as sub-calculi of ZFC set-theory (or whatever your preferred foundation of maths might be, e.g. second-order logic) that are just expressive enough to reason about programs in a given programming language, but not more. You can always reason about programs in ZFC set theory, but set theory has too much expressive power in the sense that it contains many formulae that are not really relevant for reasoning about programs (e.g. $2 \in \sqrt(\pi^{17})$ is a valid formula in ZFC that may or may not be true, depending on how you code up real numbers as sets). The superfluous expressive power is a disadvantage when thinking about program correctness because (simplifying a bit) it increases formula and proof size.
So what we are looking for in the study of program logics are logics with succinct formulae and proofs.

A similar situation obtains in the study of modal logics which (simplfying a bit again)
are not as expressive as first-order logic, but what they can express, they
do express with shorter formulae and proofs.

Identifying suitable fragments of ZFC is not hard for simple programming languages, but gets rapidly more challenging as programming languages acquire more features. The last couple of years have seen substantial progress in this endeavour.

The paper [An Axiomatic Basis for Computer Programming](http://sunnyday.mit.edu/16.355/Hoare-CACM-69.pdf) by T. Hoare is often seen as founding the study of program logics in earnest, is easy to read, and probably a good way to start venturing into the field. The same logic is studied in more detail in Winskel's book "Formal Semantics of Programming Languages" menioned by @vb le.

Type theory can be seen in a similar light. The key selling point of type-theory is the identification of proofs with (purely functional) programs, leading to a great economy of concepts and to powerful automation (in the form of type-inference and interactive theorem provers). The price for type theory's being an elegant way of organising proofs is that it does not appear to work all that well with programming languages that are not purely functional.

A recent and throughly modern text that introduces program logic in a type-theoretic tinged way is [Software Foundations](http://www.cis.upenn.edu/~bcpierce/sf/index.html) by Pierce et al. It'll lead you right near the (a) cutting edge of research in program verification and, as a textbook, probably gives a glimpse of how computer science and maths will be taught in the future.

Once a program logic has been developed for a language, the next
step is automation, or partial automation: constructing proofs
for non-trivial programs is labour intensive, and we would like
machines to do as much of it as possible. Much current research
in formal methods to do with such automation.


---

### Answer by username_2 on 2013-01-18. Score: 3

There is a very strong tradition of logic in computer science. The problems we study and the aesthetics of the computational logic community is not identical to that of the mathematical logic community. You are absolutely right that significant developments in model theory, the meta-theory of first-order logic and of set theory are not commonly used in computational logic. One can successfully research computational logi without seeing or using ultrafilters, non-standard analysis, forcing, the Paris-Harrington theorem, and a host of other fascinating concepts which are considered important in classical logic.

Just as one applies mathematical ideas to study logic as well as logical ideas to study mathematics, we apply logic to study computer science and as well as applying computational perspectives to study logic. This different focus has rather dramatic consequences for the types of results that are important for us.

Here is a quotation from John Baez about logic and computer science. I do not hold exactly the same view because I am not very familiar with advanced mathematical logic.

> When I was an undergraduate I was quite interested in logic and the foundations of mathematics --- I was always looking for the most mind-blowing concepts I could get ahold of, and Goedel's theorem, the Loewenheim-Skolem theorem, and so on were right up there with quantum mechanics and general relativity as far as I was concerned. [...] I remember feeling at the time that logic had become less revolutionary than in it was in the early part of the century. It seemed to me that logic had become a branch of mathematics like any other, studying obscure properties of models of the Zermelo-Fraenkel axioms, rather than questioning the basic presumptions implicit in those axioms and daring to pursue new, different approaches. [...]
>
> Anyway, it's now quite clear to me that I just hadn't been reading the right stuff. I think Rota has said that the really interesting work in logic now goes under the name of "computer science',[...] *--Week 40, This Week's Find, John Baez*

Logic in computer science is a vast and rapidly developing field. I find that every perspective of classical logic can be modified to derive some perspective on computational logic. The Wikipedia entry on mathematical logic splits the field into set theory, model theory, proof theory and recursion theory. You can esssentially take these areas and add a computational flavour to them and obtain a sub-field of computational logic.

**Model Theory** We like to study the model theory of non-classical logics and non-classical models of classical logic. By that I mean that we study modal, temporal and sub-structural logics, and that we study logics over trees, words, and finite models, as opposed to classical models like algebras. The two fundamental problems are satisfiability and model checking. Both have immense practical and theoretical significance. In contrast, these problems are less central in classical logic.

**Proof theory** We study the complexity and efficiency with which we can generate proofs in classical proof systems, as well as developing new, non-classical proof systems that are sensitive to complexity and efficiency considerations. Automated deduction studies machine-supported proof generation, broad speaking. The process may involve human interaction or be completely automatic. There is a lot of work on developing decision procedures for logical theories. Proof complexity focuses on the size of proofs and the computational complexity of generating proofs. There is a fascinating line of work relating programs to proofs, which combines with work descending from linear logic to develop proof systems, and consequently programming languages, that are resource sensitive.

**Recursion theory** Our recursion theory is complexity theory. Rather than studying what is computable we study how efficiently we can compute. There are many analogues of recursion theory in complexity theory, but the results and separations of recursion theory do not always hold for their complexity theoretic analogues. Instead of computable sets and an arithmetic hierarchy, we have polynomial time, the polynomial time hierarchy and polynomial space enclosing the hierarchy. Instead of bounded quantification in the arithmetic hierarchy, we have satisfiability and quantified Boolean formulae and bounded quantification of Boolean formulae.

The survey article

> [On the Unusual Effectiveness of Logic in Computer Science](http://www.cs.rice.edu/~vardi/papers/aaas99.jsl.pdf)

is a good starting point to get a very high-level view of computational logic. I am going to list several, logically oriented fields of computer science. I hope that others will edit this answer and add to that list here, and possibly add a link to an answer on this page.

1. [Finite model theory](https://cstheory.stackexchange.com/a/15081/4155)
2. Proof complexity
3. Algorithmic deduction (decision procedures for logical theories)
4. [Logics of programs](https://cstheory.stackexchange.com/a/15064/4155)
5. Dynamic logic
6. [Linear Temporal logic](https://cstheory.stackexchange.com/a/15081/4155) and its variants
7. Computational Tree Logic and its variants
8. Epistemic logic
9. [Database theory](https://cstheory.stackexchange.com/a/15070/4155)
10. Type theory
11. [Automata over infinite words](https://cstheory.stackexchange.com/a/15081/4155)
12. Categorical logic
13. Concurrency theory and process algebra
14. Domain theory
15. Linear logic
16. Descriptive Complexity
17. Model Checking
18. [Fixed Point calculi](https://cstheory.stackexchange.com/a/15081/4155) and transitive closure logics


---

### Answer by username_8 on 2013-01-17. Score: 1

an area of strong overlap between logic and computer science is [automated theorem proving](http://en.wikipedia.org/wiki/Automated_theorem_proving), eg [4]. also eg ref [1] is the use of the Boyer-Moore theorem prover to check/verify Godels theorem. another recent major/impressive result is the recent completion of software verification of the four color theorem (and others such as Odd Order and Feit-Thompson [3]) at Microsoft research by Gonthier.[2]

[1] [Metamathematics, Machines and Gödel's Proof (Cambridge Tracts in Theoretical Computer Science](http://rads.stackoverflow.com/amzn/click/0521585333) by Shankar

[2] [A computer-checked proof of the Four Colour Theorem](http://research.microsoft.com/en-us/um/people/gonthier/4colproof.pdf) Georges Gonthier

[3] [Interesting algorithms in the formalization of the Feit-Thompson theorem?](https://cstheory.stackexchange.com/questions/12729/interesting-algorithms-in-the-formalization-of-the-feit-thompson-theorem) tcs.se

[4] [Where and how did computers help prove a theorem?](https://cstheory.stackexchange.com/questions/82/where-and-how-did-computers-help-prove-a-theorem) tcs.se


---

