PL EN


2009 | 18(31) | 79-88
Article title

THE INFLUENCE OF DELOCALIZATION ON THE RESULTS OF ELIMINATING REPETITIONS OF SEMANTICALLY EQUIVALENT SENTENCES IN THE MML DATABASE

Authors
Selected contents from this journal
Title variants
Languages of publication
EN
Abstracts
EN
Detecting and removing repetitions of semantically equivalent sentences improves the quality of the MML database, but it is also an important factor in evaluating the robustness of the Mizar system. However, the complicated structure of proofs in the MML database makes it very difficult to automatically discover and remove such repetitions. One possible solution to this problem may be to apply the delocalization process, i.e. moving some sentences to outer levels of a proof where the elimination of repetitions becomes possible.
Year
Issue
Pages
79-88
Physical description
Document type
ARTICLE
Contributors
  • Robert Milewski, Institute of Computer Science, University of Bialystok, Sosnowa 64, Bialystok, Poland
References
Document Type
Publication order reference
Identifiers
CEJSH db identifier
11PLAAAA10166
YADDA identifier
bwmeta1.element.7b6b9135-5c47-3280-ae22-e84263091416
JavaScript is turned off in your web browser. Turn it on to take full advantage of this site, then refresh the page.