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.
1994
981-02-2040-5
Automated theorem proving, distributed deduction, contraction
File in questo prodotto:
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/16052
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact