| 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) |