In computability theory, an undecidable problem is a type of computational problem that requires a yes/no answer, but where there cannot possibly be any computer program that always gives the correct answer; that is, any possible program would sometimes give the wrong answer or run forever without giving any answer. More formally, an undecidable problem is a problem whose language is not a recursive set; see the article Decidable language. There are uncountably many undecidable problems, so the list below is necessarily incomplete. Though undecidable languages are not recursive languages, they may be subsets of Turing recognizable languages: i.e., such undecidable languages may be recursively enumerable. Many, if not most, undecidable problems in mathematics can be posed as word problems: determining when two distinct strings of symbols (encoding some mathematical concept or object) represent the same object or not. For undecidability in axiomatic mathematics, see List of statements undecidable in ZFC. Problems in logic Hilbert's Entscheidungsproblem. Type inference and type checking for the second-order lambda calculus (or equivalent). Determining whether a first-order sentence in the logic of graphs can be realized by a finite undirected graph. Trakhtenbrot's theorem - Finite satisfiability is undecidable. Satisfiability of first order Horn clauses. Problems about abstract machines The halting problem (determining whether a Turing machine halts on a given input) and the mortality problem (determining whether it halts for every starting configuration). Determining whether a Turing machine is a busy beaver champion (i.e., is the longest-running among halting Turing machines with the same number of states and symbols). Rice's theorem states that for all nontrivial properties of partial functions, it is undecidable whether a given machine computes a partial function with that property. The halting problem for a Minsky machine: a finite-state automaton with no inputs and two counters that can be incremented, decremented, and tested for zero. Universality of a Nondeterministic Pushdown automaton: determining whether all words are accepted. The problem whether a tag system halts. Problems about matrices The mortal matrix problem: determining, given a finite set of n × n matrices with integer entries, whether they can be multiplied in some order, possibly with repetition, to yield the zero matrix. This is known to be undecidable for a set of six or more 3 × 3 matrices, or a set of two 15 × 15 matrices. Determining whether a finite set of upper triangular 3 × 3 matrices with nonnegative integer