Proof reconstruction is the operation of extracting the computed proof from the trace of a theorem proving run. In experiments with distributed theorem proving by Clause-Diffusion, we observed that proof reconstruction is far from being a trivial task in distributed theorem proving with contraction: because of the distributed nature of the derivation and especially because of backward contraction, it may happen that a deductive process generates the empty clause, but does not have all the necessary information to reconstruct the proof. We present a modified Clause-Diffusion method which guarantees that the deductive process that generates the empty clause will be able to reconstruct the distributed proof. This result is obtained without imposing a centralized control on the deductive processes and without resorting to a round of post-processing with additional, ad hoc communication. We define a set of sufficient conditions and we prove that if a distributed strategy satisfies these requirements, then proof reconstruction is guaranteed. We show how the modified Clause-Diffusion method satisfies these requirements and we compare the modified Clause-Diffusion method with previous versions of Clause-Diffusion and related approaches.
On the reconstruction of proofs in distributed theorem proving with contraction: a modified Clause-Diffusion method
BONACINA, Maria Paola
1994-01-01
Abstract
Proof reconstruction is the operation of extracting the computed proof from the trace of a theorem proving run. In experiments with distributed theorem proving by Clause-Diffusion, we observed that proof reconstruction is far from being a trivial task in distributed theorem proving with contraction: because of the distributed nature of the derivation and especially because of backward contraction, it may happen that a deductive process generates the empty clause, but does not have all the necessary information to reconstruct the proof. We present a modified Clause-Diffusion method which guarantees that the deductive process that generates the empty clause will be able to reconstruct the distributed proof. This result is obtained without imposing a centralized control on the deductive processes and without resorting to a round of post-processing with additional, ad hoc communication. We define a set of sufficient conditions and we prove that if a distributed strategy satisfies these requirements, then proof reconstruction is guaranteed. We show how the modified Clause-Diffusion method satisfies these requirements and we compare the modified Clause-Diffusion method with previous versions of Clause-Diffusion and related approaches.File | Dimensione | Formato | |
---|---|---|---|
PASCO1994dpr.pdf
accesso aperto
Descrizione: Articolo
Tipologia:
Documento in Post-print
Licenza:
Creative commons
Dimensione
176.31 kB
Formato
Adobe PDF
|
176.31 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.