English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Tools annual

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

This work provides both a speciication and a proof of correctness for the system PDP (Prolog Distributed Processor) which make use of Abstract State Machines (ASMs). PDP is a recomputation-based model for parallel execution of Prolog on distributed memory. The system exploits OR parallelism, Independent AND parallelism as well as the combination of both. The veriication process starts from the SLD trees, which deene the execution of a Prolog program, and going through the parallel model, it arrives to the abstract machine designed for PDP, an extension of the WAM (War-ren Abstract Machine), the most common sequential implementation of Prolog. The rst step of this process consists in deening parallel SLD subtrees, which are a kind of partition of the SLD tree for programs whose clauses are annotated with parallelism. In a subsequent step the parallel execution approach of PDP is modeled by means of an OR TASK ASM. In this ASM each task is associated with the execution of a parallel SLD subtree. The execution of the parallel SLD subtree corresponding to each task is modeled by a NODE submachine which is an extension of the one proposed by BB orger and Rosenzweig to verify the sequential execution of Prolog. Accordingly, the veriication leans on the results of this work in order to avoid the veriication of the common points with the sequential execution. The new elements of the execution due to parallelism exploitation are modeled at successive steps of the veriication process, nally leading to the extended WAM which implements PDP. The PDP veriication proves correctness for this particular system but it can readily be adapted to prove it in other related parallel systems exploiting AND, OR or both kinds of parallelism.

Correctness Proof of a Distributed Implementation of Prolog by Means of Abstract State Machines