| A* algorithm | add list | admissible |
| algebraic simplification | alpha/beta search | AND node |
| AND/OR graph | answer extraction | answer literal |
| antecedent | arc consistent | assert |
| atom or atomic formula | ||
| average branching factor | axiom | backed-up value |
| backward chaining | backward search | beam search |
| best-first search | bidirectional search | blind search |
| Boolean satisfiability (SAT) | ||
| bound occurrence of variable | bounded depth-first | box |
| branching factor | breadth-first | canonical form |
| chronological backtracking | clause | closed list |
| closed world assumption (CWA) | combinatoric explosion | complete |
| conjunctive normal form (CNF) | consequent | consistent |
| constant | constraint network | constraint propagation |
| constraint satisfaction problem (CSP) | credit assignment problem | |
| decidable | deduction | deduction tree |
| delete list | dependency-directed backtracking | depth bound |
| depth-first | diameter | difference |
| effective branching factor | entail | evaluation function |
| expand a node | extension | false under an interpretation |
| first-order logic | fluent | forward chaining |
| forward search | frame problem | free occurrence of variable |
| function | game tree | genetic algorithm |
| goal state | GPS | ground instance |
| Herbrand base or atom set | Herbrand universe | heuristic function |
| heuristic search | hierarchical planning | hill climbing |
| Horn clause | horizon effect | IDA* |
| inconsistent | instantiate | intension |
| interpretation | invalid | iterative deepening |
| level-saturation method | linear resolution | literal |
| local maxima | logical consequence | means/ends analysis |
| minimax | model | model checking |
| modus ponens | most general unifier (MGU) | negation as failure |
| non-monotonic logic | open list | open world assumption |
| operator | OR node | parent clauses |
| pattern matching | plan monitoring | ply |
| precondition | predicate | predicate calculus |
| prefix | premise | prenex normal form |
| primitive subproblem | problem reduction search | propositional logic |
| quantifier | representation hypothesis | resolvent |
| retract | rewrite rule | satisfiable |
| set of support | simulated annealing | situation calculus |
| Skolem constant | Skolem function | Skolemization |
| sound | splitting | start state |
| state space | state variable | static evaluation function |
| steepest ascent | STRIPS operator | subproblem |
| substitution | successor operator | symbolic manipulation |
| table of connections | tautology | term |
| true under an interpretation | truth maintenance system (TMS) | truth table |
| Turing test | two-pointer method | unification algorithm |
| unifier | uniform cost search | unit clause |
| unit preference | unsatisfiable | valid |
| variable | Waltz filtering | well-formed formula (wff) |