Automated Theorem Proving in a Chat Environment

dc.contributor.author	Zhumagambetov, Rustam
dc.contributor.author	Sterling, Mark
dc.date.accessioned	2020-09-21T09:06:29Z
dc.date.available	2020-09-21T09:06:29Z
dc.date.issued	2018
dc.identifier.uri	https://doi.org/10.29007/m9ms
dc.identifier.uri	http://nur.nu.edu.kz/handle/123456789/4966
dc.description.abstract	We present a chat bot interface for the Coq proof assistant system. The bot provides a new modality of interaction with Coq that functions across multiple devices and platforms. Our system is particularly suitable for mobile platforms, Android and iOS. The basic architecture of the bot software is reviewed as are the outcomes of several rounds of beta-testing. Potential implications of the system are discussed, such as the possibility of a seamless collaborative proof environment.	en_US
dc.language.iso	en	en_US
dc.publisher	Nazarbayev University School of Science and Technology	en_US
dc.subject	Chat bot	en_US
dc.subject	Coq proof assistant	en_US
dc.subject	interactive theorem prover	en_US
dc.subject	proof assistant	en_US
dc.subject	theorem proving	en_US
dc.subject	user interface	en_US
dc.subject	Research Subject Categories::TECHNOLOGY	en_US
dc.title	Automated Theorem Proving in a Chat Environment	en_US
dc.type	Preprint	en_US
workflow.import.source	science