zbMATH — the first resource for mathematics

Pervasive parallelism in highly-trustable interactive theorem proving systems. (English) Zbl 1390.68571
Carette, Jacques (ed.) et al., Intelligent computer mathematics. MKM, Calculemus, DML, and systems and projects 2013, held as part of CICM 2013, Bath, UK, July 8–12, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-39319-8/pbk). Lecture Notes in Computer Science 7961. Lecture Notes in Artificial Intelligence, 359-363 (2013).
Summary: Interactive theorem proving is a technology of fundamental importance for mathematics and computer-science. It is based on expressive logical foundations and implemented in a highly trustable way. Applications include huge mathematical proofs and semi-automated verifications of complex software systems. Interactive development of larger and larger proofs increases the demand for computing power, which means explicit parallelism on current multicore hardware.
For the entire collection see [Zbl 1268.68008].
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI