What is symbolic AI in simple terms?

Symbolic AI is artificial intelligence that works from explicit facts and rules written in a formal language, and reaches conclusions by applying logic and search to them. Because every conclusion is derived step by step from stated facts and rules, the system can show exactly why it reached it.

GOFAI stands for Good Old-Fashioned Artificial Intelligence. The philosopher John Haugeland coined the term in his 1985 book Artificial Intelligence: The Very Idea to name classical symbolic AI: systems that represent knowledge as symbols and reason by manipulating them.

Is ChatGPT symbolic AI?

No. ChatGPT and other large language models are neural networks trained on large amounts of text; their knowledge is stored in numeric weights, not in explicit rules. They can call symbolic tools such as calculators, code interpreters, databases or solvers, and systems that combine the two are called neuro-symbolic.

Is symbolic AI still used?

Yes, widely, though often not under that name. SAT and SMT solvers, proof assistants such as Lean, Rocq and Isabelle, automated planners, compilers and type checkers, business rules engines and knowledge graphs are all symbolic AI in daily use.

What is the difference between symbolic and connectionist AI?

Symbolic AI represents knowledge as explicit symbols and rules and reasons with logic. Connectionist AI, the tradition behind today’s neural networks, represents knowledge as learned numeric connection strengths across many simple units. Symbolic systems are exact and explainable but brittle; connectionist systems learn from data and handle noisy input but offer weaker guarantees.

Is symbolic AI explainable?

Yes, by construction. A symbolic system reaches a conclusion through a chain of rule applications, and that chain is itself the explanation: it names every fact and rule used, and an independent checker can verify it. The explanation is only as good as the rules, but it is never an approximation of what the system did.

What are examples of symbolic AI?

Historical examples include the Logic Theorist, DENDRAL, MYCIN and XCON. Current examples include SAT and SMT solvers such as Z3, proof assistants such as Lean, PDDL planners, rule engines such as CLIPS and Drools, knowledge graphs such as Wikidata, and the search component of chess engines.

What are the limitations of symbolic AI?

Its main limitations are brittleness outside the knowledge it was given, the cost of acquiring and maintaining that knowledge from experts, the symbol grounding problem of connecting symbols to the world, and combinatorial explosion in search. It is also weak at perception, such as recognising images or speech.

Explainer · Definition, mechanics, examples

What is symbolic AI?

The branch of artificial intelligence that writes knowledge down as explicit symbols and rules, then reasons over them with logic and search. How it works, a worked example with the math, how it compares with machine learning, where it runs today, and where it breaks.

Perslis Research · 2026-09-26

Symbolic AI is the approach to artificial intelligence that represents knowledge as explicit, human-readable symbols (objects, relations and rules) and reaches conclusions by manipulating those symbols with logic, inference and search. Every conclusion can be traced back to the facts and rules that produced it. It is also called classical AI, rule-based AI or GOFAI.

In one paragraph

A symbolic AI system has two parts: a knowledge base of facts and rules written in a formal language, and an inference procedure that derives new facts from old ones, or searches for a sequence of steps that reaches a goal. Nothing is learned from statistics unless you add a learning component; what the system knows is what someone, or some process, wrote down. That makes symbolic AI exact, inspectable and correctable, and it is why its answers come with a proof. It also makes it brittle outside what was written, expensive to fill with knowledge, and prone to combinatorial explosion. Symbolic AI dominated the field from the 1950s to the late 1980s, never stopped running inside compilers, solvers, planners and rule engines, and is now returning as the reasoning half of neuro-symbolic systems.

1. The definition, precisely

A system is symbolic AI when its knowledge and its reasoning are both carried by symbols: tokens such as Parent, ann or Ancestor that stand for things in the world and are combined by explicit syntax into larger expressions. Four ingredients recur:

Symbols with a declared meaning. Each symbol names an object, a property or a relation. Its meaning is fixed by the people who built the system, not discovered from data.
Explicit knowledge. Facts and rules are written in a formal language: logic, production rules, frames, a graph of typed relations. Every piece of knowledge is a separate, readable, deletable item.
Inference. A general procedure derives new expressions from existing ones by rules of inference such as modus ponens or resolution. The procedure is the same whatever the domain; only the knowledge base changes.
Search. When no single inference step answers the question, the system explores a space of possible steps (proofs, plans, moves) until it finds one that works or exhausts the space.

The classic statement of the idea is Allen Newell and Herbert Simon’s physical symbol system hypothesis, from their 1975 Turing Award lecture, published in 1976: “A physical symbol system has the necessary and sufficient means for general intelligent action” [2]. The same lecture paired it with the heuristic search hypothesis: symbol systems solve problems by generating and progressively modifying symbol structures until they reach a solution. Whether the hypothesis is true of minds is still argued. As an engineering method, it produced most of the AI built before 1990.

The nickname GOFAI, “Good Old-Fashioned Artificial Intelligence”, was coined by the philosopher John Haugeland in Artificial Intelligence: The Very Idea (1985) [3]. The approach is also called classical AI, logic-based AI, knowledge-based systems or, in its most common industrial form, rule-based AI. Its historical rival is connectionism: the view that intelligence emerges from many simple units with learned, numeric connection strengths, which is the ancestor of today’s neural networks.

2. How symbolic AI works

Every symbolic system answers two design questions: how is knowledge written down (knowledge representation), and how are new conclusions produced from it (inference and search)?

2.1 Knowledge representation

Logic. Propositional logic states facts that are true or false (it is raining). First-order logic adds objects, relations and quantifiers (every parent of an ancestor is an ancestor). John McCarthy’s 1959 “Programs with Common Sense” is often described as the first proposal to represent a program’s knowledge as logical sentences and let the program reason from them [4].
Production rules. IF–THEN rules (if the organism is gram-negative and rod-shaped, then …). The workhorse of expert systems and of today’s business rules engines.
Frames. Marvin Minsky’s 1974 proposal: a structured record for a stereotyped situation, with slots for its parts and default values that can be overridden [8]. The idea anticipates objects and classes in programming.
Semantic networks. Concepts as nodes and relations as labelled links (canary —is-a→ bird), introduced for AI by M. Ross Quillian in 1968 [9].
Ontologies and description logics. Formal vocabularies with class hierarchies and constraints that a reasoner can check for consistency. The W3C’s OWL language and clinical terminologies such as SNOMED CT are built this way.
Knowledge graphs. Very large sets of subject–relation–object facts (Marie Curie —award received→ Nobel Prize in Physics), such as Wikidata. They are semantic networks at web scale, usually with lighter reasoning.

2.2 Inference

Forward chaining is data-driven: start from the known facts, fire every rule whose conditions are satisfied, add the conclusions, and repeat until nothing new appears. Production systems and business rules engines work this way.
Backward chaining is goal-driven: start from the question, find rules that could conclude it, and turn their conditions into sub-questions, recursively, until every sub-question is a known fact. Prolog and the MYCIN expert system work this way.
Unification is the matching step inside both. It finds a substitution of variables that makes two expressions identical: unifying Ancestor(ann, z) with Ancestor(x, cal) gives {x/ann, z/cal}. J. Alan Robinson gave the standard unification algorithm in 1965 [5].
Resolution, from the same 1965 paper, is a single inference rule that is refutation-complete for first-order logic: if a set of clauses is contradictory, repeated resolution will eventually derive the empty clause. To prove a statement, add its negation and search for that contradiction. Resolution underlies Prolog and many automated theorem provers.

Extensions handle what plain deduction cannot: default and non-monotonic reasoning (conclusions that can be withdrawn when new facts arrive), and uncertainty (MYCIN’s certainty factors in the 1970s, later probabilistic graphical models).

2.3 Search and planning

Many problems are not one inference but a sequence of choices. Symbolic AI frames them as search through a space of states: a proof search, a route, a chess game tree, a schedule. Heuristic search (A* is the standard example) uses an estimate of remaining cost to explore promising states first. Game-tree search with alpha–beta pruning plays two-player games. Constraint satisfaction and Boolean satisfiability (SAT) search for assignments that make every constraint true. Automated planning searches for a sequence of actions, each with explicit preconditions and effects, that turns an initial state into a goal state. STRIPS (Fikes and Nilsson, 1971) fixed the action format that most planners still use, now written in the Planning Domain Definition Language (PDDL) [10].

3. A worked example: rules, modus ponens and a fixed point

The whole method fits in a family tree. Start with two facts and two rules.

Knowledge base. Facts

F_{0} = {Parent (ann, bob), Parent (bob, cal)}

and rules

R = {R_{1}, R_{2}}

\begin{array}{l} R_{1} : & \forall x, y Parent (x, y) \to Ancestor (x, y) \\ R_{2} : & \forall x, y, z Parent (x, y) \land Ancestor (y, z) \to Ancestor (x, z) \end{array}

3.1 The one rule of inference: modus ponens

Modus ponens says: from $P$ and $P \to Q$ , conclude $Q$ . With variables, the rule needs a substitution $θ$ found by unification. This is generalized modus ponens:

\frac{p_{1}^{'}, \dots, p_{n}^{'} (p_{1} \land \dots \land p_{n} \to q)}{q θ} where p_{i}^{'} θ = p_{i} θ for every i

3.2 Forward chaining to a fixed point

Forward chaining applies every rule to every matching combination of known facts at once. Write this as an operator $T$ on sets of facts:

T (F) = F \cup {q θ : (p_{1} \land \dots \land p_{n} \to q) \in R, p_{i} θ \in F for all i}, F_{k + 1} = T (F_{k})

and stop at the first $k$ with $F_{k + 1} = F_{k}$ , a fixed point. On the family tree:

Forward chaining on the knowledge base above. Each new fact records the rule and substitution that produced it.
round	rule	substitution θ	new fact
1	R1	{x/ann, y/bob}	Ancestor(ann, bob)
1	R1	{x/bob, y/cal}	Ancestor(bob, cal)
2	R2	{x/ann, y/bob, z/cal}	Ancestor(ann, cal)
3	R1, R2	every match already known	none: fixed point, $F_{3} = F_{2}$

In round 2 the rule R2 needs Ancestor(bob, cal), which did not exist until round 1 produced it. That is the essence of chaining: conclusions become premises. In round 3 every rule still matches, but only facts already in the set come out, so the procedure stops with five facts.

Theorem (termination and completeness for Datalog). Let the rules be definite clauses with no function symbols, over

n

constants and

p

predicates of arity at most

a

. Then forward chaining reaches a fixed point

F^{*}

after at most

p \cdot n^{a}

rounds that add a fact, and a ground atom is in

F^{*}

if and only if it is logically entailed by

F_{0} \cup R

[12] [1].

Proof sketch. There are at most

p \cdot n^{a}

ground atoms, and

F_{0} \subseteq F_{1} \subseteq \dots

only grows, so it must stop growing. Soundness: each added fact follows by generalized modus ponens from facts already entailed. Completeness: the model that makes exactly the atoms of

F^{*}

true satisfies every fact and, because

F^{*}

is a fixed point, every rule; an atom outside

F^{*}

is false in that model, so it is not entailed. ∎

For the family tree, $p = 2$ , $n = 3$ , $a = 2$ : at most 18 possible facts, and the procedure stopped at 5. The theorem also says something a statistical model cannot say: Ancestor(cal, ann) is not in the fixed point, so it is not entailed by this knowledge base. The system does not rate it unlikely; it has no derivation and says so.

3.3 The same answer, backward

Backward chaining asks Ancestor(ann, cal)? R1 would need Parent(ann, cal), which is not a fact, so that branch fails. R2 unifies with $θ = {x / ann, z / cal}$ and leaves two sub-goals, Parent(ann, y) and Ancestor(y, cal). The first is satisfied by y = bob; the second, Ancestor(bob, cal), follows from R1 and Parent(bob, cal). Same conclusion, same proof, found from the other end. Backward chaining only touches facts relevant to the question, which is why Prolog and diagnostic expert systems use it.

3.4 Why the derivation is the explanation

Figure 1. The derivation of Ancestor(ann, cal). Every node is either a given fact or the conclusion of a named rule under a stated substitution.

Ask a symbolic system why it believes Ancestor(ann, cal) and the honest answer is Figure 1. The tree is not a summary produced after the fact; it is the computation itself. That has three practical consequences:

It can be checked by someone else. Each step is one application of one rule, so a small, independent checker can verify the proof without trusting the system that found it. Proof assistants are built on exactly this separation.
It can be challenged at a named point. If Parent(bob, cal) turns out to be wrong, you know precisely which conclusions depended on it. Truth maintenance systems automate this bookkeeping.
It is faithful. Attribution methods for neural networks (saliency maps, feature importances) estimate which inputs mattered to a score; they are approximations of a computation that is not itself a reason. A derivation has no gap between what the system did and what it reports.

4. Symbolic AI vs machine learning and neural networks

Typical forms of each approach. Real systems mix them; see §8.
dimension	symbolic AI	machine learning / neural networks
Representation	Explicit symbols, rules, graphs; each item readable on its own	Numeric parameters (weights) distributed across a model; no single weight means a fact
Where knowledge comes from	Written by people or compiled from structured sources	Fitted to examples by optimisation
Learning	Not built in; extensions such as inductive logic programming exist	The core mechanism
Explainability	The derivation is the explanation	Post-hoc approximation at best
Data needs	Little or none; one rule covers unboundedly many cases	Large labelled or unlabelled datasets
Messy perceptual input (images, speech, free text)	Poor: symbols must be supplied	Strong
Brittleness	Fails abruptly outside what is written	Degrades, often silently, outside the training distribution
Guarantees	Soundness, and completeness where the logic allows	Statistical: expected error on similar data
When it does not know	No derivation: it can say “not entailed”	Still outputs its most likely answer unless abstention is added
Changing behaviour	Edit a rule; effect is immediate and local	Retrain or fine-tune; effects can spread
Where it wins	Verification, planning, configuration, compliance, exact reasoning over structured data	Perception, language, prediction from patterns too complex to write down

The two are complements more than rivals. Neural networks are good at turning raw signals into categories; symbolic systems are good at doing exact, checkable work with categories once they exist. The long-running name for this split is symbolic vs connectionist AI. Most interesting systems built today use both, and the design question is which part holds authority over what counts as true.

5. Symbolic AI examples in use today

Symbolic AI never went away. It stopped being called AI once it worked, and runs inside software most people use without knowing it.

SAT and SMT solvers. Programs that decide whether a logical formula can be satisfied. They descend from the Davis–Putnam–Logemann–Loveland procedure (1962) [13]; SMT solvers such as Microsoft Research’s Z3 add arithmetic, arrays and bit-vectors [14]. They are used for hardware and software verification, test generation and scheduling.
Theorem provers and proof assistants. Lean, Rocq (named Coq until its 2025 renaming) and Isabelle check every step of a formal proof against a small trusted kernel [15]. They have been used to verify an optimising C compiler (CompCert, in Coq) and an operating-system microkernel (seL4, in Isabelle/HOL), and to formalise large parts of mathematics.
Automated planners. STRIPS-style planners written in PDDL schedule logistics, manufacturing and spacecraft operations; NASA’s Remote Agent experiment flew an onboard planner on Deep Space 1 in 1999.
Compilers and type checkers. Parsing is grammar-driven symbol manipulation, and Hindley–Milner type inference, used in languages such as OCaml and Haskell, is solved by unification, the same operation as in §2.2.
Rule engines and business rules. Production-rule engines such as CLIPS (developed at NASA) and Drools continue the expert-system tradition, and many use match algorithms derived from Charles Forgy’s Rete (1982) [11]. They are common wherever decisions must follow written policy: insurance underwriting, eligibility, tax and compliance.
Knowledge graphs and ontologies. Wikidata, search-engine knowledge graphs, and biomedical ontologies such as SNOMED CT and the Gene Ontology store facts as typed relations that programs can query and check.
Expert systems (historical). DENDRAL (Stanford, from 1965) inferred molecular structure from mass-spectrometry data. MYCIN (Stanford, 1970s) used roughly 600 backward-chaining rules to identify the bacteria behind severe infections such as bacteremia and meningitis and recommend antibiotics; in evaluations it performed comparably to specialists but was never used in clinical practice [16]. XCON, also called R1, configured DEC VAX computer orders from 1980 and grew to about 2,500 rules [17].
Chess engines. IBM’s Deep Blue beat world champion Garry Kasparov in 1997 with alpha–beta search over up to about 200 million positions per second and a hand-written evaluation function. Stockfish still searches with alpha–beta, but since 2020 evaluates positions with a small neural network (NNUE): a hybrid, with search as the symbolic half.

6. Strengths and limits

6.1 Where symbolic AI is strong

Exactness. A sound procedure never derives a conclusion its premises do not support. There is no “86% right” for a derived fact.
Transparency and auditability. Every rule can be read, and every conclusion traced (§3.4).
Data efficiency and generalisation by rule. R2 above applies to any family of any size, including ones never seen.
Editability. Correcting a rule changes behaviour immediately, only where the rule applies, without retraining.
Knowing what it does not know. No derivation means no answer, and the system can report that instead of guessing.

6.2 Where it breaks

Brittleness. A symbolic system knows exactly what it was told. A case one step outside its rules gets no answer or a wrong one, and ordinary common sense turns out to need an enormous number of rules. The frame problem (McCarthy and Hayes, 1969), stating compactly what does not change when an action happens, is one famous instance.
The knowledge-acquisition bottleneck. Experts often cannot state the rules they use. Edward Feigenbaum identified extracting knowledge from experts as the key bottleneck of expert systems in 1977 [18], and large rule bases proved costly to maintain.
Symbol grounding. Inside the system, Parent is a token related to other tokens. What connects it to actual parents? Stevan Harnad called this the symbol grounding problem (1990): meanings defined only by other symbols are like learning Chinese from a Chinese–Chinese dictionary [6]. In practice the grounding comes from people, sensors or learned perception.
Combinatorial explosion. Search spaces grow exponentially with problem size. The 1973 Lighthill report to the UK Science Research Council named combinatorial explosion as the central obstacle and contributed to deep funding cuts [19]. SAT itself is NP-complete. Heuristics, clause learning and good problem encodings make many real instances fast, but no general escape is known.
Uncertainty and noise. Classical logic is true-or-false. Real inputs are noisy, and early fixes such as certainty factors were ad hoc until probabilistic methods matured.

7. Not to be confused with

Symbolic regression. A machine-learning method that searches the space of mathematical expressions for a formula that fits data, usually by genetic programming (for example Schmidt and Lipson’s 2009 work on recovering physical laws [20], or the PySR library). Its output is a readable formula, but it is fitted to data, not deduced from knowledge. It is regression, not symbolic reasoning.
Symbolic computation (computer algebra). Software that manipulates mathematical expressions exactly: factoring, simplifying, differentiating, integrating in closed form. Macsyma (MIT, begun in the late 1960s), Mathematica (1988), Maple and the Python library SymPy are examples. It grew up alongside early AI and shares techniques such as rewriting and pattern matching, but its aim is exact mathematics, not reasoning about the world.
Symbolic execution. A program-analysis technique that runs code on symbolic inputs instead of concrete values and collects the conditions under which each path executes, often handing them to an SMT solver. It uses symbolic AI tools but is a verification method, not an AI system.

8. Symbolic AI today, and a short history

The current wave of AI is neural, and the most capable systems built on it increasingly lean on symbolic machinery for the parts that must be exact. Large language models call calculators, code interpreters, databases and solvers as tools. DeepMind’s AlphaGeometry (2024) paired a language model that suggests auxiliary constructions with a symbolic deduction engine that does the proving, and solved 25 of 30 recent olympiad geometry problems [21]. AlphaProof writes its proofs in Lean, so every accepted proof is checked by the proof assistant’s kernel. Artur d’Avila Garcez and Luís Lamb call this combination the “third wave” of AI [7]. How the pieces fit together, and what goes wrong, is the subject of our page on neuro-symbolic AI.

The history in one paragraph: the 1956 Dartmouth workshop named the field, and Newell, Shaw and Simon’s Logic Theorist, from the same period, proved theorems from Principia Mathematica by heuristic search. The 1960s and 1970s brought resolution, Prolog, frames and planners; the 1980s brought a commercial boom in expert systems, then the collapse of the specialised hardware market and the second of the “AI winters”. From the 1990s statistical machine learning took the lead, and from 2012 deep learning. The full story, with dates, is on the history of symbolic AI page. For the underlying theory of symbol systems and knowledge representation, see symbolic systems; for how symbolic steps are chained into deterministic pipelines, see symbolic flows.

9. Symbolic AI and fail-safe models

A fail-safe model is an AI model built so that when it fails, the failure drives it toward a controlled, safe state: it abstains when evidence is missing, and its learning can narrow what it does but never widen what it is authorised to do. Symbolic AI is the natural material for that safe state, for reasons already on this page:

“Not entailed” is a first-class answer. The theorem in §3 lets a symbolic layer say that a claim has no derivation, rather than attaching a probability to it. That is the abstention a fail-safe model needs.
Every admitted fact carries its reason. A derivation or a source citation makes each refusal and each acceptance accountable to a human reviewer (§3.4).
Soundness bounds the damage. If only the symbolic layer can admit a fact, a neural component that is wrong can make the system slower or less helpful, but cannot make it assert something the knowledge base does not support.

The operative word is authority. Adding a rule checker beside a language model does not make the combination fail-safe if the model’s output can still reach the user or the actuator unchecked. The property holds only when the symbolic layer is the one that decides what counts as true: a model may propose; only the floor admits a fact. This is also an honest limit. A symbolic floor is only as good as its sources and rules; it does not make a system right, it makes the system’s failures end in “unknown” instead of in a confident error. Our paper The Orchestration Gap argues why chain-level invariants need such a layer, and the Rubik’s cube comparison shows the difference in one picture: an impossible cube refused by name, which a confidence score cannot express.

Peel, by Perslis Research, is built this way. To our knowledge it is the first fail-safe model (the exact claim and the closest earlier work are on What is a fail-safe model?). There is no neural network in the loop that decides; knowledge is typed, sourced cards; and learning is readable counts. Peel is a research prototype, not a certified safety system. More on how Perslis uses a symbolic layer is on Symbolic AI at Perslis.

Every technique, explained. From A* and alpha–beta to Rete, STRIPS, description logics and CDCL: the symbolic AI techniques guide covers more than 130 methods across ten families.

10. Questions

What is symbolic AI in simple terms?: Symbolic AI is artificial intelligence that works from explicit facts and rules written in a formal language, and reaches conclusions by applying logic and search to them. Because every conclusion is derived step by step from stated facts and rules, the system can show exactly why it reached it.
What is GOFAI?: GOFAI stands for Good Old-Fashioned Artificial Intelligence. The philosopher John Haugeland coined the term in his 1985 book Artificial Intelligence: The Very Idea to name classical symbolic AI: systems that represent knowledge as symbols and reason by manipulating them.
Is ChatGPT symbolic AI?: No. ChatGPT and other large language models are neural networks trained on large amounts of text; their knowledge is stored in numeric weights, not in explicit rules. They can call symbolic tools such as calculators, code interpreters, databases or solvers, and systems that combine the two are called neuro-symbolic.
Is symbolic AI still used?: Yes, widely, though often not under that name. SAT and SMT solvers, proof assistants such as Lean, Rocq and Isabelle, automated planners, compilers and type checkers, business rules engines and knowledge graphs are all symbolic AI in daily use.
What is the difference between symbolic and connectionist AI?: Symbolic AI represents knowledge as explicit symbols and rules and reasons with logic. Connectionist AI, the tradition behind today’s neural networks, represents knowledge as learned numeric connection strengths across many simple units. Symbolic systems are exact and explainable but brittle; connectionist systems learn from data and handle noisy input but offer weaker guarantees.
Is symbolic AI explainable?: Yes, by construction. A symbolic system reaches a conclusion through a chain of rule applications, and that chain is itself the explanation: it names every fact and rule used, and an independent checker can verify it. The explanation is only as good as the rules, but it is never an approximation of what the system did.
What are examples of symbolic AI?: Historical examples include the Logic Theorist, DENDRAL, MYCIN and XCON. Current examples include SAT and SMT solvers such as Z3, proof assistants such as Lean, PDDL planners, rule engines such as CLIPS and Drools, knowledge graphs such as Wikidata, and the search component of chess engines.
What are the limitations of symbolic AI?: Its main limitations are brittleness outside the knowledge it was given, the cost of acquiring and maintaining that knowledge from experts, the symbol grounding problem of connecting symbols to the world, and combinatorial explosion in search. It is also weak at perception, such as recognising images or speech.

11. References

S. Russell, P. Norvig. Artificial Intelligence: A Modern Approach, 4th ed. Pearson, 2020.
A. Newell, H. A. Simon. Computer Science as Empirical Inquiry: Symbols and Search. Communications of the ACM 19(3):113–126, 1976. doi:10.1145/360018.360022
J. Haugeland. Artificial Intelligence: The Very Idea. MIT Press, 1985.
J. McCarthy. Programs with Common Sense. In Mechanisation of Thought Processes: Proceedings of the Symposium at the National Physical Laboratory (Teddington, 1958). HMSO, London, 1959.
J. A. Robinson. A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM 12(1):23–41, 1965. doi:10.1145/321250.321253
S. Harnad. The Symbol Grounding Problem. Physica D 42:335–346, 1990. doi:10.1016/0167-2789(90)90087-6
A. d’Avila Garcez, L. C. Lamb. Neurosymbolic AI: The 3rd Wave. Artificial Intelligence Review 56(11):12387–12406, 2023. doi:10.1007/s10462-023-10448-w. arXiv:2012.05876
M. Minsky. A Framework for Representing Knowledge. MIT AI Laboratory Memo 306, 1974.
M. R. Quillian. Semantic Memory. In M. Minsky (ed.), Semantic Information Processing. MIT Press, 1968.
R. E. Fikes, N. J. Nilsson. STRIPS: A New Approach to the Application of Theorem Proving to Problem Solving. Artificial Intelligence 2(3–4):189–208, 1971.
C. L. Forgy. Rete: A Fast Algorithm for the Many Pattern/Many Object Pattern Match Problem. Artificial Intelligence 19(1):17–37, 1982.
M. H. van Emden, R. A. Kowalski. The Semantics of Predicate Logic as a Programming Language. Journal of the ACM 23(4):733–742, 1976.
M. Davis, G. Logemann, D. Loveland. A Machine Program for Theorem-Proving. Communications of the ACM 5(7):394–397, 1962. doi:10.1145/368273.368557
L. de Moura, N. Bjørner. Z3: An Efficient SMT Solver. TACAS 2008, LNCS 4963. doi:10.1007/978-3-540-78800-3_24
L. de Moura, S. Kong, J. Avigad, F. van Doorn, J. von Raumer. The Lean Theorem Prover (System Description). CADE-25, 2015.
E. H. Shortliffe. Computer-Based Medical Consultations: MYCIN. Elsevier, 1976.
J. McDermott. R1: A Rule-Based Configurer of Computer Systems. Artificial Intelligence 19(1):39–88, 1982.
E. A. Feigenbaum. The Art of Artificial Intelligence: Themes and Case Studies of Knowledge Engineering. Proceedings of IJCAI-77, 1977.
J. Lighthill. Artificial Intelligence: A General Survey. In Artificial Intelligence: a paper symposium. Science Research Council, 1973.
M. Schmidt, H. Lipson. Distilling Free-Form Natural Laws from Experimental Data. Science 324(5923):81–85, 2009. doi:10.1126/science.1165893
T. H. Trinh, Y. Wu, Q. V. Le, H. He, T. Luong. Solving Olympiad Geometry without Human Demonstrations. Nature 625:476–482, 2024.