Managing Proof Documents for Asynchronous Processing | Zendy

Holger Gast | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Managing Proof Documents for Asynchronous Processing

Author(s) -

Holger Gast

Publication year - 2009

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2008.12.097

Subject(s) - computer science , gas meter prover , asynchronous communication , automated theorem proving , protocol (science) , programming language , usability , consistency (knowledge bases) , proof of concept , simple (philosophy) , state (computer science) , theoretical computer science , distributed computing , mathematical proof , operating system , artificial intelligence , computer network , medicine , philosophy , geometry , mathematics , alternative medicine , epistemology , pathology

Asynchronous proof processing is a recent approach at improving the usability and performance of interactive theorem provers. It builds on a simple metaphor: the user edits a proof document while the prover checks its consistency in the background without explicit requests from the user. This paper presents a software architecture for asynchronous proof processing. Its foundation is a novel state model for commands that synchronizes the possibly parallel accesses of the user interface and prover. The state model is complemented by a communication protocol that places minimal requirements on the prover. The model also allows asynchronous processing to be emulated by existing linear-processing proof engines, such that the migration to the new communication protocol is simplified. A prototype implementation that works with the current development version of Isabelle is presented

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research