Mechanising a Proof of Craig s Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle

Peter Chapman, James McKinna, Christian Urban. Mechanising a Proof of Craig s Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle. In Serge Autexier, John Campbell, Julio Rubio, Volker Sorge, Masakazu Suzuki, Freek Wiedijk, editors, Intelligent Computer Mathematics, 9th International Conference, AISC 2008, 15th Symposium, Calculemus 2008, 7th International Conference, MKM 2008, Birmingham, UK, July 28 - August 1, 2008. Proceedings. Volume 5144 of Lecture Notes in Computer Science, pages 38-52, Springer, 2008. [doi]

Authors

Peter Chapman

This author has not been identified. Look up 'Peter Chapman' in Google

James McKinna

This author has not been identified. Look up 'James McKinna' in Google

Christian Urban

This author has not been identified. Look up 'Christian Urban' in Google