Christian Urban, Xingyuan Zhang Interactive Theorem Proving - Springer 2015 - Lecture Notes in Computer Science . ISBN: 9783319221021 Subjects--Index Terms: Mathematical Logic and Formal Languages; Artificial Intelligence (incl. Robotics); Logics and Meanings of Programs; Software Engineering; Systems and Data Security; Algorithm Analysis and Problem Complexity