Where Symbolic Methods Shine

Symbolic methods shine where the rules are formal, the answers must be exact,
and the explanation matters. Concretely:

Formal reasoning — first-order logic, type theory, set theory, higher-order
logic. Used in: hardware verification, security-critical software,
mathematical proof assistants.

Type systems — Haskell, OCaml, Rust, SML. The compiler proves that
well-typed programs can't go wrong in certain ways. Types are lightweight
formal verification, automatically checked.

Automated theorem proving — Lean, Coq, Isabelle, Agda, ACL2. Used to
verify the CompCert C compiler, seL4 microkernel, four-color theorem,
Kepler's conjecture, parts of the proof of Fermat's Last Theorem.

Verified AI — combining statistical systems with symbolic verifiers.
Neural networks whose outputs are checked against formal specs. LLMs whose
code is type-checked before execution. Self-driving cars whose decision logic
is provably safe.

Knowledge graphs and ontologies — formal representations of entities and
relations, used in semantic web, biomedical informatics (Gene Ontology),
library science, enterprise search.

Mathematical software — computer algebra systems (Mathematica, Sage,
Maple), proof checkers, automated reasoning (Z3, Vampire).

The PSSH revisited. Newell and Simon claimed symbol manipulation is the
necessary and sufficient condition for intelligence. The course's
counter-perspective: symbolic methods are NECESSARY for guarantees, but not
SUFFICIENT for the perceptual richness of human intelligence. Hybrid systems
combine both.

Where to go next. If you liked this course:
- Lean theorem prover (beginner-friendly, growing community)
- Software foundations (Pierce) for type theory and verified programming
- Concrete Mathematics (Graham, Knuth, Patashnik) for the discrete math toolkit
- Elements of Discrete Mathematics (Liu) for classical problem-solving

Bibliography (key sources for this course):

• Chomsky, N. (1965). Aspects of the Theory of Syntax. MIT Press.
• Aristotle. Organon. Translated by H. Cooke (1938). Loeb Classical Library.
• Garey, M. R. & Johnson, D. S. (1979). Computers and Intractability: A Guide to the Theory of NP-Completeness. Freeman.
• Halmos, P. R. (1974). Naive Set Theory. Springer.
• Lee, L. (2002). Fast context-free grammar parsing requires fast boolean matrix multiplication. JACM 49(1).
• Lewis, H. R. & Papadimitriou, C. H. (1998). Elements of the Theory of Computation. Prentice Hall.
• Nordmann, A. et al. (2018). Lecture-capture research papers.
• Paulson, L. C. (1991). ML for the Working Programmer. Cambridge University Press.
• Ranta, A. (2017). Grammatical Framework: Programming with Multilingual Grammars. CSLI.
• Rosen, K. H. (1990). Discrete Mathematics and Its Applications. McGraw-Hill.
• Standard ML of New Jersey Basis Library (2010).
• World Wide Web Consortium. Extensible Markup Language (XML) 1.0 (Fourth Edition).
• derf.net / various. Longest palindromic substrings reference list.