Interactive theorem proving

From Wikipedia, the free encyclopedia

You have new messages (last change).

Interactive theorem proving is the field of computer science and mathematical logic concerned with tools to develop formal proofs by man-machine collaboration. This involves some sort of proof assistant: an interactive proof editor, or other interface, with which a human can guide the search for proofs, the details of which are stored in, and some steps provided by, a computer.

 This mathematics-related article is a stub. You can help Wikipedia by expanding it.
Retrieved from "http://en.wikipedia.org../../../i/n/t/Interactive_theorem_proving.html"