This series follows the development of modern mathematical logic: how reasoning acquired precise languages, how proofs and their limits became mathematical subjects, and how those ideas shaped computation and formalized mathematics.
Part 0 is this guide. Parts 1–27 form the main sequence. Six companion notes examine earlier logical traditions separately, giving their questions and achievements space in their own historical settings.
Explore the series in two other ways: find your reasoning companions or follow the interactive timeline.
Where to begin
For a first reading, begin with Part 1: Boole and the Algebraic Tradition and follow the Previous note and Next note controls. The sequence introduces ideas before returning to their later developments.
If you have a particular interest, use these starting points:
- Foundations and the limits of proof. Read Parts 1–12 in order, from logical algebra to set-theoretic independence.
- Proofs, types, and programs. Begin with intuitionism and Gentzen's proof theory, then read Parts 15–18. These notes develop the relationship between constructive evidence, typed programs, and semantics.
- Automation and formalization. Begin with syntax and completeness and computability, then read Parts 19–25 and 27. Dependent type theory supplies background for assistants based on that foundation.
- Earlier history. Choose a note from the earlier traditions. These companions can be read independently; their order does not imply a single line of historical transmission.
How to read the notes
Each note develops a historical problem through the people and texts involved, a worked example, and an explanation of what the resulting ideas establish. Technical terms are introduced as they arise. Familiarity with elementary algebra, sets, and functions will help with the examples.
Three distinctions recur throughout the series: a formal proof and truth in a model; the existence of an algorithm and the resources it requires; and a checked statement and its intended interpretation. Keeping these distinctions in view makes the transitions between foundations, computation, and verification easier to follow.
The reading order is organized around these connections. Historical developments often overlap, and modern notation used in an example may reconstruct an earlier argument rather than reproduce its original presentation.
Interactive labs
The labs connect a worked example with an experiment. Begin with the supplied problem, predict its result, then change an input and compare. Hints and variations help explain what the computation establishes.
Begin with the foundations, or choose a lab beside the subject you are reading:
- Test a class argument — Part 1. Edit memberships, find counterexamples, and test the role of existence assumptions.
- See how quantifiers change a claim — Part 2. Build a relation, inspect witnesses, and compare safe substitution with variable capture.
- Construct a set missing from the list — Part 3. Try to find a missing subset, then reveal a construction that works for every proposed list.
- Work through Russell’s paradox — Part 4. Test both self-membership assumptions and see how separation changes the defining condition.
- Run a Turing machine — Part 9. Edit the tape and transitions; inspect halting, cycles, and bounded runs.
- Construct a proof, one inference at a time — Part 10. Build a Gentzen-style tree, discharge assumptions, and remove a proof detour.
- Change the frame, test the formula — Part 13. Change accessibility and valuations to inspect modal truth and countermodels.
- Check a term, then watch its proof normalize — Part 15. Edit typed terms, follow reductions, and compare untyped evaluation strategies.
- Follow a conflict to its explanation — Part 20. Step through Boolean decisions, propagation, clause learning, and backtracking.
- Find a model—or explain a conflict — Part 20. Run Z3 on editable constraints involving arithmetic, equality, bit-vectors, and scheduling.
- Possible eventually, or inevitable eventually? — Part 24. Compare EF and AF with exact fixed points, witness paths, and counterexample cycles.
Further labs will be added to this directory as they become available. Each lab states its mathematical scope, and the surrounding worked example remains readable without running it.
Main reading order
1–6 · Languages and foundations
The series begins with changes in logical expression and the mathematical questions that made explicit foundations necessary.
- Boole and the Algebraic Tradition — Classes, relations, and the development of logical calculation.
- Frege, Quantifiers, and Logical Form — Variables, scope, and the expression of mathematical arguments.
- Rigor, Infinity, and Axioms — Analysis, infinite sets, and explicit axiomatic methods.
- Paradoxes and Competing Foundations — Logicism, types, predicativity, and axiomatic set theory.
- Hilbert's Program — The attempt to justify mathematics through the study of finite proofs.
- Intuitionism and Construction — Constructive evidence and the meaning of mathematical existence.
7–14 · Proof, truth, and their limits
Once formal systems were precisely defined, logicians could investigate their expressive power, their models, and the questions they could not decide.
- Syntax, Truth, and Completeness — Derivability, satisfaction, and the completeness of first-order logic.
- Gödel and Incompleteness — Arithmetic coding, undecidable sentences, and consistency statements.
- Computability — Effective procedures and the limits of algorithmic decision.
- Gentzen and Proof Theory — Deduction, proof transformations, and consistency analysis.
- Model Theory — Definability, mathematical structures, and classification.
- Set Theory and Independence — Constructibility, forcing, and the choice of additional axioms.
- Modal Logic — Necessity, possibility, time, knowledge, and relational semantics.
- Alternative Logics — Truth values, relevance, inconsistency, and the use of assumptions.
15–18 · Types, programs, and semantics
The next group develops precise connections between proofs and programs, then examines the mathematical structures used to interpret them.
- Lambda Calculus and Curry–Howard — Typed terms, proofs, substitution, and normalization.
- Dependent Type Theory — Types that express properties of values, equality, and universes.
- Categorical Logic — Structural interpretations of logic and quantification.
- Functional Programming and Semantics — Recursion, polymorphism, evaluation, and models of computation.
19–24 · Automation and verification
These connections support several distinct uses of machines: searching for proofs, checking derivations, executing logical programs, and verifying systems.
- Automated Theorem Proving — Resolution, unification, equality reasoning, and proof search.
- Complexity, SAT, and SMT — Computational cost, satisfiability, and cooperating decision procedures.
- Logic Programming — Clauses as programs and the relationship between deduction and execution.
- Proof Assistants — Interactive proving, checking architectures, and formal assumptions.
- Program Verification — Invariants, termination, specifications, and local reasoning.
- Model Checking and Abstraction — Temporal properties, state spaces, and counterexamples.
25–27 · Formalized mathematics and new methods
The final group considers how formal methods change mathematical practice, from shared libraries to alternative foundations and learned proof search.
- Formalized Mathematics — Large proofs, reusable libraries, and mathematical collaboration.
- Homotopy Type Theory and Univalence — Identity, equivalence, and new foundations for formal mathematics.
- Learned Theorem Proving — Learning-guided search, formalization, and the evidence behind recent results.
Earlier traditions
These six notes form a separate companion series. They examine inference, demonstration, language, and knowledge in traditions whose aims cannot be reduced to preparing the way for modern symbolic logic.
- Greek and Late-Antique Logic — Aristotle, the Stoics, demonstration, and commentary.
- Arabic, Islamic, and Jewish Logical Traditions — Translation, Avicenna, later developments, and reception.
- Medieval Latin Logic — Supposition, consequence, semantic paradoxes, and disputation.
- Indian Logic — Nyāya, Buddhist inference, evidence, and Navya-Nyāya.
- Chinese Traditions of Argument — Mohist reasoning, names and kinds, and standards of argument.
- Before Boole: Reform, Leibniz, and Bolzano — Early-modern projects for method, calculation, and logical consequence.
The final companion connects naturally with Part 1 of the main sequence. Earlier traditions also remain relevant when later notes return to demonstration, modal reasoning, or the interpretation of language.
Sources and editorial approach
Each subject note ends with sources and further reading. Original works establish what was proposed or proved; scholarly histories help explain terminology, influence, reception, and disputed attribution. Recent formalization results are discussed with their dates, assumptions, and documented scope.
A meeting of minds
Your reasoning portrait
Twelve small thought experiments. Discover historical thinkers whose questions you might enjoy exploring.
A playful reading guide, not a psychological test or an assessment of ability. The matches interpret published work; they do not describe the thinkers’ personalities. There are no correct answers.
Question 1 of 12 · 0 answered
Your reading companions
These are affinities with research questions, not identities. A different set of choices can suggest a different route through the series.
Aristotle (384–322 BCE)
The classification of statements and patterns of inference is central to the logical works associated with Aristotle.
Begin with syllogistic, demonstration, and what the form of an argument contributes. Explore the note →
Image and biographical sources
Later likeness: a Roman copy after a Greek portrait; the mantle is a modern addition. After Lysippos. Via Wikimedia Commons. Image source · Public domain · Biographical dates
Dignāga (c. 480–c. 540 CE)
Dignāga’s analysis asks when an inferential sign supplies warranted evidence. The connection here is an interest in evidence and interpretation, not an attribution of modern verification theory.
Read the conditions of an inferential reason and the distinction between perception and inference. Explore the note →
Image and biographical sources
Later depiction: a modern Buddhavanam relief showing Dignāga teaching Buddhist logic. Anandajoti. Via Wikimedia Commons. Image source · CC BY-SA 4.0 · Biographical dates
Mozi (c. 470–c. 391 BCE)
Mohist arguments appeal to public standards and comparisons. This profile uses that emphasis on assessable reasons as a reading connection.
Explore standards of argument, names, kinds, and the limits of analogical extension. Explore the note →
Image and biographical sources
Later depiction: an imagined portrait, not a contemporary record of his appearance. Vjacheslav Rublevskiy. Via Wikimedia Commons. Image source · CC0 · Biographical dates
George Boole (1815–1864)
Boole turned conditions of inference into objects of algebraic calculation.
Try the class-algebra lab and examine what an equation does—and does not—say about existence. Explore the note →
Image and biographical sources
Algebraic methods for class and propositional reasoning. Unknown artist, The Illustrated London News, 21 January 1865, public domain, via Wikimedia Commons Image source · Public domain · Biographical dates
Gottlob Frege (1848–1925)
Frege’s work makes logical form, variables, and quantifier scope explicit.
Compare separate witnesses with a common witness in the quantifier lab. Explore the note →
Image and biographical sources
Quantification, function–argument analysis, and formal derivations. Unknown photographer, circa 1879, public domain, via Wikimedia Commons Image source · Public domain · Biographical dates
David Hilbert (1862–1943)
Hilbert’s foundational program made formal proofs and their justification mathematical objects.
Ask which methods a consistency argument itself is allowed to use. Explore the note →
Image and biographical sources
Axiomatization and the metamathematical study of consistency. Unknown photographer, before 1912, public domain, via Wikimedia Commons Image source · Public domain · Biographical dates
L. E. J. Brouwer (1881–1966)
Brouwer’s intuitionism puts mathematical construction at the center of claims of existence.
Compare a witness-producing proof with a classical existence argument. Explore the note →
Image and biographical sources
Intuitionistic foundations and mathematical construction. Unknown photographer, 1937 or earlier, public domain, via Wikimedia Commons Image source · Public domain · Biographical dates
Kurt Gödel (1906–1978)
Gödel’s completeness and incompleteness results expose different relationships between proof, truth, and formal expressive power.
Read why completeness of a logic and incompleteness of arithmetic are compatible. Explore the note →
Image and biographical sources
Completeness, incompleteness, and effective axiomatization. Unknown photographer, circa 1926, public domain, via Wikimedia Commons Image source · Public domain · Biographical dates
Alan Turing (1912–1954)
Turing’s analysis pairs an exact account of effective computation with a proof of its limits.
Run a small machine, then distinguish a long run from a proof of nontermination. Explore the note →
Image and biographical sources
Machine computation, effective procedures, and undecidability. Elliott and Fry, 1951, public domain in its source country, via Wikimedia Commons Image source · Public domain · Biographical dates
Alfred Tarski (1901–1983)
Tarski’s semantic work separates formal expressions from the structures and metalanguage used to interpret them.
Follow satisfaction through a model and examine the scope of a truth definition. Explore the note →
Image and biographical sources
Truth, satisfaction, and the semantics of formal languages. George M. Bergman, 1968; cropped by Off-shell. Oberwolfach Photo Collection via Wikimedia Commons. Image source · GFDL 1.2 or later · Biographical dates
.jpeg){kind=link}
Gerhard Gentzen (1909–1945)
Gentzen studied the structure of deductions and transformations that remove unnecessary detours.
Construct a natural-deduction tree and inspect how assumptions are discharged. Explore the note →
Image and biographical sources
Natural deduction, cut elimination, and ordinal analysis. Prague, 1945. Image credited to Eckart Menzler-Trott in the Oberwolfach Photo Collection, via Wikimedia Commons. Image source · CC BY-SA 2.0 de · Biographical dates
Julia Robinson (1919–1985)
Julia Robinson’s work on Diophantine definability helped connect equations with the limits of algorithmic decision.
Follow the collaborative solution of Hilbert’s tenth problem. Explore the note →
Image and biographical sources
George Bergman. Via Wikimedia Commons. Image source · GFDL 1.2 · Biographical dates
Alonzo Church (1903–1995)
Church’s lambda calculus and logical calculi connect formal expression, functions, and effective procedures.
Compare typed terms with untyped computation in the reduction lab. Explore the note →
Image and biographical sources
Princeton graduation portrait, published in 1924. Photographer not identified. Nassau Herald, 1924, p. 101; Princeton University Library. Portrait extracted from the page; no retouching. Image source · Public domain (published before 1931) · Biographical dates
Per Martin-Löf (b. 1942)
Martin-Löf’s type theories organize constructive proofs through judgments, dependent types, and computation.
Study how a dependent pair packages a value together with evidence about it. Explore the note →
Image and biographical sources
Creator not identified in the source record. Via Wikimedia Commons. Image source · Public domain · Biographical dates
C. A. R. Hoare (1934–2026)
Hoare’s program logic relates specified assumptions, execution, and guarantees.
Separate partial correctness, termination, and the adequacy of a specification. Explore the note →
Image and biographical sources
Rules connecting commands with preconditions and postconditions. Nano412, released into the public domain, via Wikimedia Commons Image source · Public domain · Biographical dates
Vladimir Voevodsky (1966–2017)
Voevodsky’s univalent foundations connect mathematical structure with a project of formal verification.
Explore why identity, equivalence, and computation raise new foundational questions. Explore the note →
Image and biographical sources
Schmid, Renate. Via Wikimedia Commons. Image source · CC BY-SA 2.0 de · Biographical dates
How your choices shaped the result
Each answer contributes to one or more of six interests. The bars show points earned relative to the points available for that interest. They are not population percentiles or probabilities. Matches compare the pattern with editorial profiles of sixteen thinkers; close results are best read together.
Definitions, scope, and the form of an argument.
Witnesses, constructions, and the steps of a proof.
Counterexamples, paradoxes, and boundaries of a method.
Rules, algorithms, and the process of computation.
Models, relations, and what a statement means.
Evidence, assumptions, and independently checkable claims.
The weights and historical profiles are interpretive, not scientifically validated. Equal matching scores are ordered alphabetically. No personality type is assigned.
Review or change an answer
Answers stay in this page and are cleared when you reload.
Ideas across time
The series timeline
Follow 107 milestones across thirteen streams, from earlier traditions to modern formalization.
Years run horizontally; streams run vertically. Every subject note is represented. This is a map of the series, not an exhaustive history. Streams overlap intellectually; their position does not imply a hierarchy or a line of influence.
107 milestones · 33 subject notes · compiled 5 September 2026
Scroll, swipe, or drag through years and streams. Select a milestone to read it. Zoom changes the date spacing while keeping text readable.
Mouse and keyboard controls
Drag with the mouse to pan, or hold Alt while scrolling over the map to zoom around the pointer. With the map focused, use + / − to zoom, 0 for 100%, and F to fit the period. With a milestone focused, use ← / → to move chronologically, Home / End for the first or last, and Enter to read it. The sliders also support arrow keys. Browser zoom and touch gestures retain their usual behavior.
Overview: dots mark individual milestones. Select a dot for its title and sources, or zoom in to show full cards.
No milestones match these filters. Try another period or reset the map.
The chronological index below includes dates, source records, and links to the corresponding notes. Enable JavaScript to use the map and filters.
c. 450–350 BCEDialectic and paradox
Greek and late antique
Socratic questioning, Platonic dialectic, and early paradoxes make argument itself an object of inquiry. The period is approximate.
c. 4th–3rd centuries BCELater Mohist analysis
Chinese traditions
The Mohist Canons and explanations investigate distinctions, names, knowledge, and argument. Their composition belongs to a developing textual tradition.
Earlier traditions, part 5: Chinese Traditions of Argument: Names, Kinds, and Distinctions →
4th century BCEAristotle: syllogistic
Greek and late antique
The Analytics investigate valid syllogisms and demonstrative knowledge. This interval locates the work within Aristotle’s period; it does not date each treatise.
3rd century BCEXunzi: rectifying names
Chinese traditions
Xunzi connects the use of names with distinctions and shared practices. The bar locates his work within a century; it does not give a composition date or a lifespan. His precise dates are uncertain, and he was still alive in 238 BCE.
Earlier traditions, part 5: Chinese Traditions of Argument: Names, Kinds, and Distinctions →
3rd century BCEStoic propositional inference
Greek and late antique
Chrysippus and the Stoic tradition develop inference patterns organized around propositions. Surviving reports require historical reconstruction.
c. 2nd–5th centuries CENyāya text and commentary
Indian traditions
The Nyāya-sūtra and Vātsyāyana’s commentary organize inquiry into knowledge and inference. Formation and dating are disputed; this is a broad orientation.
Earlier traditions, part 4: Indian Logic: Inference, Evidence, and Analysis →
Logic in Classical Indian Philosophy · Stanford Encyclopedia of Philosophy
c. 480–540Dignāga: inferential signs
Indian traditions
Dignāga analyzes the conditions under which a sign warrants inference. The interval indicates his approximate lifetime, not a precise publication date.
Earlier traditions, part 4: Indian Logic: Inference, Evidence, and Analysis →
Logic in Classical Indian Philosophy · Stanford Encyclopedia of Philosophy
Early 6th centuryBoethius and transmission
Greek and late antique
Boethius’s translations and logical writings become important resources for later Latin readers. Transmission involved many intermediaries.
c. 7th centuryDharmakīrti: grounds of inference
Indian traditions
Dharmakīrti investigates why an inferential connection is warranted, including relations of identity and causal dependence. Chronology remains approximate.
Earlier traditions, part 4: Indian Logic: Inference, Evidence, and Analysis →
Logic in Classical Indian Philosophy · Stanford Encyclopedia of Philosophy
9th–10th centuriesTranslation and interpretation
Arabic and Jewish traditions
Greek logical writings circulate through Syriac and Arabic scholarship. Translators and commentators also develop terminology and interpretations.
Earlier traditions, part 2: Arabic, Islamic, and Jewish Logical Traditions →
Early 10th centuryAl-Fārābī: organizing logic
Arabic and Jewish traditions
Al-Fārābī treats logic as a systematic discipline and examines its relation to language and demonstrative science.
Earlier traditions, part 2: Arabic, Islamic, and Jewish Logical Traditions →
Early 11th centuryIbn Sīnā’s logical project
Arabic and Jewish traditions
Ibn Sīnā develops an independent account of syllogistic and modality. The interval locates major work, rather than dating every logical text.
Earlier traditions, part 2: Arabic, Islamic, and Jewish Logical Traditions →
Early 12th centuryAbelard: language and consequence
Latin and early modern
Abelard’s logical works examine signification and consequence within a changing textual and institutional setting.
Earlier traditions, part 3: Medieval Latin Logic: Reference, Consequence, and Paradox →
13th–14th centuriesSupposition and consequence
Latin and early modern
Latin logicians develop theories of reference, consequence, and semantic paradox. Ockham and Buridan belong to a diverse tradition.
Earlier traditions, part 3: Medieval Latin Logic: Reference, Consequence, and Paradox →
13th–14th centuriesPost-Avicennan developments
Arabic and Jewish traditions
Authors including al-Rāzī, al-Ṭūsī, and al-Kātibī reshape the inherited discussions. Jewish logical writing participates in several linguistic settings.
Earlier traditions, part 2: Arabic, Islamic, and Jewish Logical Traditions →
c. 14th centuryGaṅgeśa and Navya-Nyāya
Indian traditions
The Tattvacintāmaṇi helps establish a highly technical analysis of cognition, inference, and language. Dating is approximate.
Earlier traditions, part 4: Indian Logic: Inference, Evidence, and Analysis →
1620Bacon: Novum Organum
Latin and early modern
Bacon proposes a reform of inquiry centered on the disciplined investigation of nature.
Earlier traditions, part 6: Before Boole: Reform, Leibniz, and Bolzano →
1662The Port-Royal Logic
Latin and early modern
Arnauld and Nicole organize logic around conceiving, judging, reasoning, and method.
Earlier traditions, part 6: Before Boole: Reform, Leibniz, and Bolzano →
1666–1686 · selected writingsLeibniz: symbolic projects
Latin and early modern
Leibniz pursues connected projects for a characteristic language and calculation of reasoning. Much logical work remained unpublished during his lifetime.
Earlier traditions, part 6: Before Boole: Reform, Leibniz, and Bolzano →
1837Bolzano: Wissenschaftslehre
Latin and early modern
Bolzano studies propositions, consequence, and variation of ideas independently of a modern symbolic calculus.
Earlier traditions, part 6: Before Boole: Reform, Leibniz, and Bolzano →
1847Boole’s logical algebra
Algebra and logical language
The Mathematical Analysis of Logic presents an algebraic treatment of inference. Its operations require historical care when compared with modern Boolean algebra.
1854The Laws of Thought
Algebra and logical language
Boole develops his treatment of logical calculation, including probability and the interpretation of algebraic expressions.
1870–1885 · selected papersPeirce: relations and quantifiers
Algebra and logical language
Peirce develops an algebra of relatives and quantification; Oscar Howard Mitchell contributes to the notation and treatment of quantifiers.
1872Constructions of the reals
Foundations and set theory
Dedekind’s cuts and contemporary approaches to real numbers make continuity an explicit mathematical problem.
1874Cantor: unequal infinities
Foundations and set theory
Cantor proves that real numbers cannot all be enumerated. His 1874 argument should be distinguished from the later diagonal presentation.
1879Frege’s Begriffsschrift
Algebra and logical language
Frege introduces a formal language with explicit quantification and the analysis of mathematical inference.
1888Dedekind on numbers
Foundations and set theory
Was sind und was sollen die Zahlen? develops a structural account of the natural numbers.
1889Peano’s arithmetic
Foundations and set theory
Peano presents arithmetic using explicit axioms and symbolic notation.
1890–1895Schröder’s lectures
Algebra and logical language
Schröder’s Vorlesungen organize and extend algebraic logic, including relations.
1891The diagonal argument
Foundations and set theory
Cantor gives a diagonal method for showing that a proposed enumeration misses an object.
1899Hilbert’s geometry
Foundations and set theory
Grundlagen der Geometrie clarifies the organization and independence of geometric axioms.
1901 discovery · 1902 letterRussell’s paradox
Foundations and set theory
Russell discovers the paradox and communicates it to Frege in 1902. Unrestricted comprehension requires revision.
1907Brouwer’s dissertation
Foundations and set theory
Brouwer’s foundational work helps establish the constructive orientation later associated with intuitionism.
1908Zermelo’s axiomatization
Foundations and set theory
Zermelo proposes axioms for set theory, restricting subset formation to an already given set.
1910–1913Principia Mathematica
Foundations and set theory
Whitehead and Russell publish the three volumes of a logicist development using ramified type theory.
1918Lewis and strict implication
Proof, models, and logics
C. I. Lewis’s Survey of Symbolic Logic develops an alternative to treating material implication as every form of implication.
Part 13: Modal Logic: Necessity, Time, Knowledge, and Provability →
1920Łukasiewicz: three values
Proof, models, and logics
Łukasiewicz presents a three-valued logic, opening a different semantic treatment of logical connectives.
Part 14: Alternative Logics: Truth, Relevance, Inconsistency, and Resources →
1920s · representative periodHilbert’s proof-theoretic program
Foundations and set theory
Hilbert, Bernays, Ackermann, and collaborators investigate formal mathematics using restricted metamathematical methods.
1924Schönfinkel’s combinators
Types, programs, and categories
Combinators express combinations of functions without bound variables; Curry subsequently develops the subject.
Part 15: Lambda Calculus and the Curry–Howard Correspondence →
1929 dissertation · 1930 publicationFirst-order completeness
Proof, models, and logics
Gödel proves that semantic validity in first-order logic entails formal derivability.
1930Heyting’s formal calculus
Proof, models, and logics
Heyting formulates intuitionistic logic, making its rules available for mathematical study.
1931Gödel’s incompleteness theorems
Proof, models, and logics
Sufficiently strong, effectively axiomatized arithmetic theories face limits on completeness and internal consistency proofs under the relevant hypotheses.
1932–1933Church’s lambda calculus
Types, programs, and categories
Church develops lambda calculus within a larger foundational project. The calculus outlives defects in that initial logical system.
Part 15: Lambda Calculus and the Curry–Howard Correspondence →
1933 Polish · 1935 GermanTarski on truth
Proof, models, and logics
Tarski defines truth for formalized languages with an explicit distinction between object language and metalanguage.
1934–1935Natural deduction and sequents
Proof, models, and logics
Gentzen develops proof calculi and cut elimination, making the structure of derivations central.
1936Church’s undecidability result
Computability and complexity
Church uses lambda-definability and recursive functions to establish an unsolvable problem and a negative decision result.
1936Gentzen’s consistency proof
Proof, models, and logics
Gentzen’s analysis of arithmetic uses transfinite induction up to ε₀. The metatheoretic assumptions matter.
1936Rosser’s refinement
Proof, models, and logics
Rosser weakens the consistency hypothesis needed for an incompleteness result.
1936–1937 publicationTuring’s computable numbers
Computability and complexity
Turing gives a machine account of computation and proves a negative answer to the Entscheidungsproblem.
Part 9: The Emergence of Computability →
On Computable Numbers, with an Application to the Entscheidungsproblem
1938 announcement · 1940 monographGödel’s constructible universe
Foundations and set theory
Constructibility establishes relative consistency results for choice and the generalized continuum hypothesis.
1940Church’s simple type theory
Types, programs, and categories
Church presents a typed logical calculus that becomes an important ancestor of higher-order systems.
Part 15: Lambda Calculus and the Curry–Howard Correspondence →
1944Post: degrees of unsolvability
Computability and complexity
Post’s work organizes questions about recursively enumerable sets and relative computability.
1945Eilenberg and Mac Lane
Types, programs, and categories
General Theory of Natural Equivalences introduces the categorical language developed to study mathematical transformations.
Part 17: Categorical Logic: Structure, Quantification, and Internal Languages →
Eilenberg and Mac Lane, General Theory of Natural Equivalences (1945)
1946Barcan: quantified modality
Proof, models, and logics
Ruth Barcan Marcus’s early work combines quantification and modal reasoning.
Part 13: Modal Logic: Necessity, Time, Knowledge, and Provability →
1949Henkin’s completeness method
Proof, models, and logics
Henkin’s construction builds a model from a suitably expanded consistent theory.
1955Łoś’s theorem
Proof, models, and logics
Łoś’s theorem relates first-order truth in an ultraproduct to truth in its component structures.
1956The Logic Theory Machine
Automated reasoning
Newell, Shaw, and Simon present an early program for searching for proofs.
Part 19: Automated Theorem Proving: Clauses, Unification, Equality, and Search →
The Logic Theory Machine: A Complex Information Processing System (1956)
1960Davis–Putnam procedure
Automated reasoning
Davis and Putnam present a clause-based procedure for quantification theory.
1960McCarthy’s symbolic functions
Types, programs, and categories
McCarthy’s account of recursive symbolic expressions connects computation with an executable functional language.
Part 18: Functional Programming and Programming-Language Semantics →
1962DPLL backtracking
Automated reasoning
Davis, Logemann, and Loveland develop a search procedure using case splitting and propagation.
Part 20: Complexity, SAT, and SMT →
Davis, Logemann, and Loveland, A Machine Program for Theorem-Proving (1962)
1963Cohen introduces forcing
Foundations and set theory
Forcing establishes independence results for set theory, relative to appropriate consistency assumptions.
1963 · influential publicationRelational modal semantics
Proof, models, and logics
Kripke’s semantic work is a major stage in the development of relational semantics, alongside earlier contributions by others.
Part 13: Modal Logic: Necessity, Time, Knowledge, and Provability →
1964Landin’s mechanical evaluation
Types, programs, and categories
Landin analyzes evaluation through a lambda-based abstract machine.
Part 18: Functional Programming and Programming-Language Semantics →
Peter Landin, The Mechanical Evaluation of Expressions (1964)
1964–1971 · selected worksCategorical logic develops
Types, programs, and categories
Lawvere, Lambek, Tierney, and others connect categories with foundations, deduction, quantification, and internal logic.
Part 17: Categorical Logic: Structure, Quantification, and Internal Languages →
F. William Lawvere, Adjointness in Foundations (1969), reprint
1965Morley’s categoricity theorem
Proof, models, and logics
Morley’s theorem connects categoricity in uncountable cardinalities and helps orient later classification theory.
1965Robinson’s resolution
Automated reasoning
Resolution and unification supply a general method for clause-based automated deduction.
Part 19: Automated Theorem Proving: Clauses, Unification, Equality, and Search →
A Machine-Oriented Logic Based on the Resolution Principle (1965)
1967De Bruijn’s Automath
Assistants and formal mathematics
Automath provides a language for representing mathematics with mechanically checkable reasoning.
1967Floyd assigns meanings to programs
Program and system verification
Floyd uses assertions at program points to reason about program behavior.
Part 23: Program Verification: Invariants, Semantics, and Local Reasoning →
1969Hoare’s axiomatic basis
Program and system verification
Hoare formalizes reasoning about programs through preconditions, commands, and postconditions.
Part 23: Program Verification: Invariants, Semantics, and Local Reasoning →
1969 manuscriptHoward: formulas as types
Types, programs, and categories
Howard’s manuscript relates formulas and proofs to types and terms. Its publication follows in 1980.
Part 15: Lambda Calculus and the Curry–Howard Correspondence →
1970Hilbert’s tenth problem
Computability and complexity
Matiyasevich completes a line of work by Davis, Putnam, and Julia Robinson, establishing the algorithmic unsolvability of the general problem.
1971Cook: NP-completeness
Computability and complexity
Cook establishes a foundational completeness result connecting nondeterministic computation with satisfiability.
1971 · joint reportScott–Strachey semantics
Types, programs, and categories
Scott and Strachey develop a mathematical account of programming-language meaning using domains and denotations.
Part 18: Functional Programming and Programming-Language Semantics →
Scott and Strachey, Toward a Mathematical Semantics for Computer Languages (1971)
1972Karp’s reductions
Computability and complexity
Karp exhibits reductions linking a broad family of combinatorial decision problems.
1972 · first implementationProlog emerges
Automated reasoning
Colmerauer, Roussel, and collaborators develop Prolog in dialogue with work on deduction and the procedural interpretation of clauses.
1972–1984 · successive formulationsMartin-Löf’s type theories
Types, programs, and categories
Successive constructive type theories develop judgments, dependent types, equality, and universes. The 1984 book records lectures from 1980.
Part 16: Dependent Type Theory: Proofs, Data, and Universes →
1973Levin’s independent work
Computability and complexity
Levin’s publication develops an independent formulation of universal search problems.
1973 · project beginsMizar’s development begins
Assistants and formal mathematics
Trybulec’s Mizar project pursues readable formal mathematical language and sustained library development.
1970s · early developmentML and inferred types
Types, programs, and categories
ML grows around LCF; work on polymorphic type inference helps shape functional programming.
Part 18: Functional Programming and Programming-Language Semantics →
1974Logic as a programming language
Automated reasoning
Kowalski presents the procedural interpretation of predicate logic, separating logical content from control.
1975Guarded commands and derivation
Program and system verification
Dijkstra develops guarded commands and a calculus for deriving programs from specifications.
Part 23: Program Verification: Invariants, Semantics, and Local Reasoning →
Guarded Commands, Nondeterminacy and a Calculus for the Derivation of Programs (1975)
1977Abstract interpretation
Program and system verification
Patrick and Radhia Cousot establish a framework relating concrete program behaviors to sound abstract analyses.
Part 24: Temporal Verification, Model Checking, and Abstraction →
1977 dissertationLandau’s analysis in Automath
Assistants and formal mathematics
Van Benthem Jutting formalizes Landau’s Grundlagen der Analysis, an early substantial mathematical development.
Part 25: Formalized Mathematics: Proofs and Reusable Libraries →
1977Pnueli: temporal program reasoning
Program and system verification
Pnueli brings temporal logic to the specification and reasoning of program behavior.
Part 24: Temporal Verification, Model Checking, and Abstraction →
1979 · Edinburgh LCF accountLCF’s theorem architecture
Assistants and formal mathematics
The Edinburgh LCF account develops an architecture in which an abstract theorem type protects checked inference.
1979Combining decision procedures
Automated reasoning
Nelson and Oppen analyze how suitable theories can cooperate through shared equalities.
Part 20: Complexity, SAT, and SMT →
Nelson and Oppen, Simplification by Cooperating Decision Procedures (1979)
1980 publicationHoward’s manuscript published
Types, programs, and categories
The Formulae-as-Types Notion of Construction appears in the Curry festschrift, after circulating as a 1969 manuscript.
Part 15: Lambda Calculus and the Curry–Howard Correspondence →
1981–1982Model checking emerges
Program and system verification
Clarke and Emerson, and independently Queille and Sifakis, develop automatic finite-state checking of temporal properties.
Part 24: Temporal Verification, Model Checking, and Abstraction →
Mid-to-late 1980sHOL develops
Assistants and formal mathematics
Gordon’s HOL work adapts the LCF approach to classical higher-order logic and verification.
1986 · initial developmentIsabelle begins
Assistants and formal mathematics
Paulson’s Isabelle develops a generic framework for implementing logical formalisms.
1987Girard’s linear logic
Proof, models, and logics
Linear logic makes the use of assumptions explicit by controlling structural rules.
Part 14: Alternative Logics: Truth, Relevance, Inconsistency, and Resources →
1988 journal publicationCalculus of Constructions
Types, programs, and categories
Coquand and Huet’s calculus combines dependent types and polymorphism; later inductive extensions support the Coq lineage.
Part 16: Dependent Type Theory: Proofs, Data, and Universes →
1996GRASP and conflict analysis
Automated reasoning
Marques-Silva and Sakallah’s work develops conflict analysis and nonchronological search in SAT solving.
Part 20: Complexity, SAT, and SMT →
Marques-Silva and Sakallah, GRASP—A New Search Algorithm for Satisfiability (1996)
10 October 1996EQP resolves the Robbins problem
Automated reasoning
McCune’s EQP finds an equational proof that Robbins algebras are Boolean; subsequent checking is distinct from the search.
Part 19: Automated Theorem Proving: Clauses, Unification, Equality, and Search →
2001Chaff: solver engineering
Automated reasoning
Chaff demonstrates how propagation, branching, and implementation choices can dramatically affect SAT performance.
2002 · Reynolds’s surveySeparation logic
Program and system verification
Separation logic organizes local reasoning about disjoint portions of mutable memory, following work by several contributors.
Part 23: Program Verification: Invariants, Semantics, and Local Reasoning →
Separation Logic: A Logic for Shared Mutable Data Structures (2002)
2005 completionA formal Four Color proof
Assistants and formal mathematics
Gonthier, building on work with Werner, completes a Coq formalization. His explanatory article appears in 2008.
Part 25: Formalized Mathematics: Proofs and Reusable Libraries →
2006–2009 · early accountsCompCert’s verified compilation
Program and system verification
Leroy and collaborators develop compiler correctness proofs connecting source and target program behavior.
Part 23: Program Verification: Invariants, Semantics, and Local Reasoning →
2008Z3’s system paper
Automated reasoning
De Moura and Bjørner present Z3, an SMT solver combining Boolean search with theory reasoning.
2009seL4’s verification result
Program and system verification
The seL4 team reports functional-correctness verification of an operating-system kernel, under explicitly stated assumptions.
Part 23: Program Verification: Invariants, Semantics, and Local Reasoning →
2012 completion · 2013 paperThe Odd Order Theorem
Assistants and formal mathematics
A large team led by Gonthier formalizes the theorem in Coq, with extensive reusable algebraic infrastructure.
Part 25: Formalized Mathematics: Proofs and Reusable Libraries →
2013The HoTT book
Types, programs, and categories
The collaborative book synthesizes work on identity, equivalence, and univalent foundations during the IAS program.
2013 · project beginsLean’s development begins
Assistants and formal mathematics
De Moura initiates Lean; later versions develop integrated elaboration, automation, and mathematical libraries.
2014 completionFlyspeck completed
Assistants and formal mathematics
The Flyspeck collaboration completes formal verification of the Kepler conjecture proof using HOL Light and Isabelle.
Part 25: Formalized Mathematics: Proofs and Reusable Libraries →
July 2024 reportAlphaProof and AlphaGeometry 2
Automated reasoning
DeepMind reports a combined silver-medal-level IMO score. The problems were manually formalized, and some computations took days.
Part 27: Learned Theorem Proving: Search, Formalization, and Discovery →
AI Achieves Silver-Medal Standard at the International Mathematical Olympiad
November 2025 publicationAlphaProof methodology
Automated reasoning
A research paper describes reinforcement learning with formal proof feedback. The publication date differs from the 2024 demonstration.
Part 27: Learned Theorem Proving: Search, Formalization, and Discovery →
2026 · versioned case studyPrimeGapsLib’s conditional theorem
Assistants and formal mathematics
The series examines a versioned Lean theorem on infinitely many prime gaps at most 246. Bombieri–Vinogradov is an explicit hypothesis of that theorem.
Part 27: Learned Theorem Proving: Search, Formalization, and Discovery →
Dates and editorial choices
The map distinguishes publication, completion, announcement, and approximate periods in its labels. Bars may represent successive works or an approximate lifetime; read each description before treating a range as a continuous project. The axis uses a linear scale with BCE/CE years and no year zero.
The stream assignments and “read alongside” links are editorial navigation aids. They do not establish historical influence. Consult each source and the fuller account in its note. Recent cases are dated snapshots, not a claim to cover every development through the present.
Further exploration
Use these references to explore the series by period, person, or source.
People
These profiles link to the relevant notes. The essays also examine the wider communities and collaborators behind each development.
Algebraic methods for class and propositional reasoning.
Unknown artist, The Illustrated London News, 21 January 1865, public domain, via Wikimedia Commons Image record · Public domain · Biographical dates
Quantification, function–argument analysis, and formal derivations.
Unknown photographer, circa 1879, public domain, via Wikimedia Commons Image record · Public domain · Biographical dates
The paradox of unrestricted formation and type-theoretic responses.
Unknown photographer, 1907, public domain, via Wikimedia Commons Image record · Public domain · Biographical dates
Axiomatization and the metamathematical study of consistency.
Unknown photographer, before 1912, public domain, via Wikimedia Commons Image record · Public domain · Biographical dates
Intuitionistic foundations and mathematical construction.
Unknown photographer, 1937 or earlier, public domain, via Wikimedia Commons Image record · Public domain · Biographical dates
Truth, satisfaction, and the semantics of formal languages.
George M. Bergman, 1968; cropped by Off-shell. Oberwolfach Photo Collection via Wikimedia Commons. Image record · GFDL 1.2 or later · Biographical dates
Completeness, incompleteness, and effective axiomatization.
Unknown photographer, circa 1926, public domain, via Wikimedia Commons Image record · Public domain · Biographical dates
Machine computation, effective procedures, and undecidability.
Elliott and Fry, 1951, public domain in its source country, via Wikimedia Commons Image record · Public domain · Biographical dates
Natural deduction, cut elimination, and ordinal analysis.
Prague, 1945. Image credited to Eckart Menzler-Trott in the Oberwolfach Photo Collection, via Wikimedia Commons. Image record · CC BY-SA 2.0 de · Biographical dates
Constructive derivations and typed terms.
Andrej Bauer, 22 May 2004, CC BY-SA 2.5 Slovenia, via Wikimedia Commons Image record · CC BY-SA 2.5 si · Biographical dates
Recursive symbolic computation and Lisp.
Tom Varco, 21 April 2006, CC BY-SA 3.0, via Wikimedia Commons Image record · CC BY-SA 3.0 · Biographical dates
With J. C. Shaw, heuristic proof search in the Logic Theorist.
Circa 1958. The Commons record credits Paolo Massa; the original photographer is not identified. J. C. Shaw is not pictured. Image record · Public domain · Herbert A. Simon: dates · Allen Newell: dates
The procedural interpretation of clauses, logic, and control.
Yongyuth Permpoontanalarp, 9 November 2009, CC BY 3.0, via Wikimedia Commons Image record · CC BY 3.0 · Biographical dates
With Philippe Roussel and collaborators, the development of Prolog.
Alaindavid2, 5 July 1988, CC BY-SA 4.0, via Wikimedia Commons Image record · CC BY-SA 4.0 · Biographical dates
Automath and the formal representation of mathematical texts.
Konrad Jacobs, 1960s, CC BY-SA 2.0 DE, Oberwolfach Photo Collection via Wikimedia Commons Image record · CC BY-SA 2.0 de · Biographical dates
Rules connecting commands with preconditions and postconditions.
Nano412, released into the public domain, via Wikimedia Commons Image record · Public domain · Biographical dates
Polynomial reductions and the complexity of propositional reasoning.
Jiří Janíček, 24 September 2008, via Wikimedia Commons. Image record · CC BY-SA 3.0 · Biographical dates
Universal search problems and independent work on computational complexity.
Sergio01, 22 September 2010, via Wikimedia Commons. Image record · CC BY-SA 3.0 · Biographical dates
Detail from a group photograph at the 1932 International Congress of Mathematicians. The available crop has limited resolution.
Johannes Meiner. Via Wikimedia Commons. Image record · Public domain · Biographical dates
.jpg){kind=link}
.jpg){kind=link}
.jpg){kind=link}
.jpg){kind=link}
.jpg){kind=link}
.jpg){kind=link}
.png){kind=link}
Photograph from around 1922; his death is generally dated to 1942.
Open Logic. Via Wikimedia Commons. Image record · CC BY-SA 4.0 · Biographical dates.jpg){kind=link}
.jpg){kind=link}
.jpg){kind=link}
.jpg){kind=link}
.jpg){kind=link}
Later depiction: a seventeenth-century print by Jan de Bisschop.
Jan de Bisschop. Via Wikimedia Commons. Image record · CC0 · Biographical dates,_RP-P-1907-4495.jpg){kind=link}
Later likeness: a Roman marble portrait, possibly copied from a lost Greek bronze.
Copy of Lysippos (?). Via Wikimedia Commons. Image record · Public domain · Biographical dates
Later likeness: a marble copy of the portrait attributed to Silanion.
© Marie-Lan Nguyen / Wikimedia Commons. Via Wikimedia Commons. Image record · Public domain · Biographical dates
Later likeness: a Roman copy after a Greek portrait; the mantle is a modern addition.
After Lysippos. Via Wikimedia Commons. Image record · Public domain · Biographical dates
Later depiction: a bust in the Palermo Botanical Garden.
Teofrasto_Orto_botanico_PA.jpg : tato grasso derivative work: Singinglemon ( talk ). Via Wikimedia Commons. Image record · CC BY-SA 2.5 · Biographical dates
Later likeness: a Roman marble copy after a lost Hellenistic original.
Unknown artist Unknown artist. Via Wikimedia Commons. Image record · Public domain · Biographical dates
Later depiction: an engraving by Georg Paul Busch.
Georg Paul Busch (engraver). Via Wikimedia Commons. Image record · Public domain · Biographical dates
Later depiction: an illustration in André Thevet's collection of portraits, 1584.
Unknown photographer or artist. Via Wikimedia Commons. Image record · Public domain · Biographical dates
Later depiction from the Bibliothèque nationale de France portrait collection.
Creator not identified in the source record. Via Wikimedia Commons. Image record · Public domain · Biographical dates
Later depiction: a medieval illustration of the late-antique author.
Unknown photographer or artist. Via Wikimedia Commons. Image record · Public domain · Biographical dates
Later depiction: an imagined portrait in the Nuremberg Chronicle, 1493.
Mr.Nostalgic. Via Wikimedia Commons. Image record · Public domain · Biographical dates
Later depiction: a reproduction of a bust held in the National Library of Medicine collection.
National Library of Medicine. Via Wikimedia Commons. Image record · No restrictions · Biographical dates.jpg){kind=link}
Later depiction: a detail of Andrea di Bonaiuto's fourteenth-century fresco in Florence.
Sailko. Via Wikimedia Commons. Image record · CC BY 3.0 · Biographical dates
Later depiction: an Iranian commemorative stamp issued in 1976.
Creator not identified in the source record. Via Wikimedia Commons. Image record · Public domain · Biographical dates
Later depiction: a portrait published in the eighteenth-century Thesaurus antiquitatum sacrarum.
Blaisio Ugolino. Via Wikimedia Commons. Image record · Public domain · Biographical dates
Later depiction: an engraving by Antoni Oleszczyński.
Antoni Oleszczyński. Via Wikimedia Commons. Image record · Public domain · Biographical dates.jpg){kind=link}
Later depiction: stained glass in a church in Surrey.
self-created (Moscarlop). Via Wikimedia Commons. Image record · CC BY-SA 3.0 · Biographical dates
Later depiction: a manuscript illustration from around 1370, now in the Jagiellonian Library.
Unknown photographer or artist. Via Wikimedia Commons. Image record · Public domain · Biographical dates.jpg){kind=link}
Later depiction: a commemorative statue at Udayanacharya Sanskrit Vidyalaya.
pravendrakt. Via Wikimedia Commons. Image record · CC BY-SA 3.0 · Biographical dates
Later depiction: a modern Buddhavanam relief showing Dignāga teaching Buddhist logic.
Anandajoti. Via Wikimedia Commons. Image record · CC BY-SA 4.0 · Biographical dates
Later depiction: a Tibetan portrait from the fifteenth or sixteenth century, Cleveland Museum of Art.
Creator not identified in the source record. Via Wikimedia Commons. Image record · CC0 · Biographical dates
Later depiction: an imagined portrait, not a contemporary record of his appearance.
Vjacheslav Rublevskiy. Via Wikimedia Commons. Image record · CC0 · Biographical dates
Later depiction: a modern commemorative sculpture in Xiamen Garden Expo Park.
向史公哲曰. Via Wikimedia Commons. Image record · CC BY-SA 4.0 · Biographical dates
Later depiction: a traditional portrait, not a contemporary record of his appearance.
Unknown photographer or artist. Via Wikimedia Commons. Image record · Public domain · Biographical dates
Later depiction: a Japanese religious portrait; not a contemporary likeness.
Unknown photographer or artist. Via Wikimedia Commons. Image record · Public domain · Biographical dates
Later depiction: a Japanese religious portrait; not a contemporary likeness.
Unknown photographer or artist. Via Wikimedia Commons. Image record · Public domain · Biographical dates
.jpg){kind=link}
Harvard graduation portrait, published in 1920.
Photographer not identified. Harvard Class Album, 1920, p. 173; Allen County Public Library via Internet Archive. Portrait extracted from the page; no retouching. Image record · Public domain (published before 1931) · Biographical dates
Princeton graduation portrait, published in 1924.
Photographer not identified. Nassau Herald, 1924, p. 101; Princeton University Library. Portrait extracted from the page; no retouching. Image record · Public domain (published before 1931) · Biographical datesReference index
A consolidated selection of sources. Consult each note's bibliography for reading specific to its subject.
- The Emergence of First-Order Logic
- Begriffsschrift (1879)
- Mathematical Problems (1900)
- Principia Mathematica
- Zermelo's Axiomatization of Set Theory
- Intuitionism in the Philosophy of Mathematics
- Hilbert's Program
- Kurt Gödel
- Gödel's Incompleteness Theorems
- Tarski's Truth Definitions
- An Unsolvable Problem of Elementary Number Theory (1936)
- On Computable Numbers, with an Application to the Entscheidungsproblem
- The Development of Proof Theory
- Propositions as Types
- An Intuitionistic Theory of Types (1972)
- The Logic Theory Machine: A Complex Information Processing System (1956)
- A Computing Procedure for Quantification Theory (1960)
- A Machine-Oriented Logic Based on the Resolution Principle (1965)
- Predicate Logic as Programming Language (1974)
- An Axiomatic Basis for Computer Programming (1969)
- Description of the Language Automath (1967)
- History of Interactive Theorem Proving
- About the Rocq Prover
- Isabelle Overview
- A History of Haskell
- Formal Proof, The Four-Color Theorem
- A Machine-Checked Proof of the Odd Order Theorem
- The Flyspeck Project
- CompCert Bibliography
- Lean Language Reference: Introduction and History
- Mathlib
- Recursive Functions of Symbolic Expressions (1960)
- A Note on the Entscheidungsproblem (1936)
- Church's Type Theory
- Assigning Meanings to Programs (1967)
- seL4: Formal Verification of an OS Kernel (2009)
- Homotopy Type Theory: Univalent Foundations of Mathematics
- Hilbert's Tenth Problem
- The Continuum Hypothesis
- Aristotle's Logic
- Leibniz's Influence on 19th Century Logic
- The Early Development of Set Theory
- Continuity and Infinitesimals
- AI Achieves Silver-Medal Standard at the International Mathematical Olympiad
- PrimeGapsLib
- Skolem's Paradox
- Computational Complexity Theory
- Chaff: Engineering an Efficient SAT Solver (2001)
- Temporal Logic
- Social Processes and Proofs of Theorems and Programs (1979)
- The Development of Intuitionistic Logic
- Intuitionistic Logic
- Recursive Functions
- Second-order and Higher-order Logic
- Generalized Quantifiers
- Modal Logic
- Provability Logic
- Guarded Commands, Nondeterminacy and a Calculus for the Derivation of Programs (1975)
- Separation Logic: A Logic for Shared Mutable Data Structures (2002)
- Robbins Algebras Are Boolean (1996)
- Ibn Sina's Logic
- Gaṅgeśa
- Mohism