Nội dung được dịch bởi AI, chỉ mang tính chất tham khảo
Tìm kiếm thuật ngữ nhanh với Cây ngữ cảnh mã hóa
Tóm tắt
Cấu trúc dữ liệu chỉ mục có ảnh hưởng quan trọng đến hiệu suất của các trình chứng minh định lý tự động. Ví dụ như cây phân biệt, tương tự như cây trie, trong đó các thuật ngữ được xem như chuỗi và các tiền tố chung được chia sẻ, và cây thay thế, nơi các thuật ngữ giữ nguyên cấu trúc cây của chúng và tất cả các ngữ cảnh chung có thể được chia sẻ. Ở đây, chúng tôi mô tả một cấu trúc dữ liệu chỉ mục mới, gọi là cây ngữ cảnh, trong đó, thông qua một loại biến ngữ cảnh hạn chế, các tiểu thuật ngữ chung cũng có thể được chia sẻ, ngay cả khi chúng xuất hiện dưới các ký hiệu hàm khác nhau. Ngoài việc giới thiệu khái niệm này, chúng tôi cũng cung cấp bằng chứng về giá trị thực tiễn của nó. Chúng tôi cho thấy cách các cây ngữ cảnh có thể được triển khai bằng cách sử dụng các lệnh máy trừu tượng. Các thí nghiệm với các bài kiểm tra về khớp tiến cho thấy rằng triển khai của chúng tôi có tính cạnh tranh với các triển khai hiện tại hàng đầu khác được mã hóa chặt chẽ. Đặc biệt, mức tiêu thụ không gian của cây ngữ cảnh thấp hơn đáng kể so với các cấu trúc chỉ mục khác.
Từ khóa
#cấu trúc dữ liệu chỉ mục #cây ngữ cảnh #trình chứng minh định lý #khớp tiến #tiêu thụ không gianTài liệu tham khảo
citation_journal_title=J. Automated Reasoning; citation_title=Flatterms, discrimination nets, and fast term rewriting; citation_author=J. Christian; citation_volume=10; citation_publication_date=1993; citation_pages=95-113; citation_id=CR1
citation_title=Substitution tree indexing; citation_inbook_title=6th RTA; citation_publication_date=1995; citation_pages=117-131; citation_id=CR2; citation_author=P. Graf; citation_publisher=Springer-Verlag
citation_title=Context trees; citation_inbook_title=Proceedings of the First International Joint Conference on Automated Reasoning (IJCAR 2001); citation_publication_date=2001; citation_pages=242-256; citation_id=CR3; citation_author=H. Ganzinger; citation_author=R. Nieuwenhuis; citation_author=P. Nivela; citation_publisher=Springer-Verlag
citation_journal_title=J. Automated Reasoning; citation_title=WALDMEISTER-High-performance equational deduction; citation_author=T. Hillenbrand, A. Buch, R. Vogt, B. Löchner; citation_volume=18; citation_issue=2; citation_publication_date=1997; citation_pages=265-270; citation_id=CR4
citation_journal_title=J. Automated Reasoning; citation_title=Experiments with discrimination tree indexing and path indexing for term retrieval; citation_author=W. McCune; citation_volume=9; citation_issue=2; citation_publication_date=1992; citation_pages=147-167; citation_id=CR5
citation_title=On the evaluation of indexing techniques for theorem proving; citation_inbook_title=Proceedings of the First International Joint Conference on Automated Reasoning (IJCAR 2001); citation_publication_date=2001; citation_pages=257-271; citation_id=CR6; citation_author=R. Nieuwenhuis; citation_author=T. Hillenbrand; citation_author=A. Riazanov; citation_author=A. Voronkov; citation_publisher=Springer-Verlag
citation_title=A kernel of data structures and algorithms for automated deduction with equality clauses (system description); citation_inbook_title=14th Int. Conf. on Automated Deduction (CADE); citation_publication_date=1997; citation_pages=49-53; citation_id=CR7; citation_author=R. Nieuwenhuis; citation_author=J. M. Rivero; citation_author=M. Vallejo; citation_publisher=Springer-Verlag
Riazanov, A. and Voronkov, A. (2000) Partially adaptive code trees, in Proceedings of JELIA 2000 (Malaga, Spain).
citation_journal_title=AI Communications; citation_title=The design and implementation of VAMPIRE; citation_author=A. Riazanov, A. Voronkov; citation_volume=15; citation_publication_date=2002; citation_pages=91-110; citation_id=CR9
citation_title=The TPTP problem library; citation_inbook_title=Proceedings of the 12th International Conference on Automated Deduction; citation_publication_date=1994; citation_pages=252-266; citation_id=CR10; citation_author=G. Sutcliffe; citation_author=C. Suttner; citation_author=T. Yemenis; citation_publisher=Springer-Verlag
citation_journal_title=J. Automated Reasoning; citation_title=The anatomy of Vampire: Implementing bottom-up procedures with code trees; citation_author=A. Voronkov; citation_volume=15; citation_issue=2; citation_publication_date=1995; citation_pages=237-265; citation_id=CR11
citation_journal_title=J. Automated Reasoning; citation_title=SPASS-Version 0.49; citation_author=C. Weidenbach; citation_volume=18; citation_issue=2; citation_publication_date=1997; citation_pages=247-252; citation_id=CR12