Editing List of undecidable problems (section)

==Problems in logic==
* Hilbert's [[Entscheidungsproblem]].
* [[Type inference]] and [[type checking]] for the [[second-order lambda calculus]] (or equivalent).<ref>{{cite journal | first = J. B. | last = Wells | title = Typability and type checking in the second-order lambda-calculus are equivalent and undecidable | citeseerx = 10.1.1.31.3590 | journal = Tech. Rep. 93-011 | publisher = Comput. Sci. Dept., Boston Univ. | year = 1993 | pages = 176–185 }}</ref>
* Determining whether a first-order sentence in the [[logic of graphs]] can be realized by a finite undirected graph.<ref>{{cite journal | last = Trahtenbrot | first = B. A. | author-link = Boris Trakhtenbrot | journal = Doklady Akademii Nauk SSSR |series=New Series | mr = 0033784 | pages = 569–572 | title = The impossibility of an algorithm for the decision problem for finite domains | volume = 70 | year = 1950}}</ref>
* [[Trakhtenbrot's theorem]] - Finite satisfiability is undecidable.
* Satisfiability of first order [[Horn clause]]s.