Automated Theorem Proving in a Chat Environment

Simple item page
dc.contributor.authorZhumagambetov, Rustam
dc.contributor.authorSterling, Mark
dc.date.accessioned2020-09-21T09:06:29Z
dc.date.available2020-09-21T09:06:29Z
dc.date.issued2018
dc.description.abstractWe 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.identifier.urihttps://doi.org/10.29007/m9ms
dc.identifier.urihttp://nur.nu.edu.kz/handle/123456789/4966
dc.language.isoenen_US
dc.publisherNazarbayev University School of Science and Technologyen_US
dc.subjectChat boten_US
dc.subjectCoq proof assistanten_US
dc.subjectinteractive theorem proveren_US
dc.subjectproof assistanten_US
dc.subjecttheorem provingen_US
dc.subjectuser interfaceen_US
dc.subjectResearch Subject Categories::TECHNOLOGYen_US
dc.titleAutomated Theorem Proving in a Chat Environmenten_US
dc.typePreprinten_US
workflow.import.sourcescience

Files

Original bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
proceedings_paper_325.pdf
Size:
763.65 KB
Format:
Adobe Portable Document Format
Description:
Download
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
6.28 KB
Format:
Item-specific license agreed upon to submission
Description:
Download

Collections

Articles